Если кто-то знает, что это такое пожалуйста напишите
(Prolog)
Только теория:
Пусть {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)), которые тоже различны.
Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют так называемый наиболее общий унификатор.