Наименьший общий унификатор, Prolog Опции

[Altair]

Если кто-то знает, что это такое пожалуйста напишите
(Prolog)

[AlaRic]

Только теория:

Пусть {E1,…,Ek} – множество литералов или множество термов. Подстановка s называется унификатором этого множества, если s(E1)=s(E2)=…=s(Ek). Множество унифицируемо, если существует унификатор этого множества.

Например, множество атомарных формул


{Q(a,x,f(x)), Q(u,у,z)}

унифицируемо подстановкой {u=a, x=у,z=f(у)}, а множество


{R(x,f(x)), R(u,u)}

неунифицируемо. Действительно, если заменить х на u, то получим множество


{R(u,f(u), R(u,u)}.


Проводить же замену u=f(u) запрещено определением подстановки, да и бесполезно, т.к. она приводит к формулам R(f(u), f(f(u))) и R(f(u), f(u)), которые тоже различны.


Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют так называемый наиболее общий унификатор.

[Altair]

спасибо!