Задача унификации: различия между версиями

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

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

Если термы унифицируемы, то у них может быть много унификаторов, но всегда существует и единствен

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