Задача унификации

Задача унификации (Unification problem) - По двум описаниям [math]\displaystyle{ X }[/math] и [math]\displaystyle{ Y }[/math] определить, можно ли найти объект [math]\displaystyle{ Z }[/math], который удовлетворяет обоим описаниям.

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

Литература

[Евстигнеев-Касьянов/94]