Унификация предикатов при выводе из гипотез

Определение. Унификация — процедура сравнения предикатов и поиск подстановки-интерпретации, при которой предикаты совпадают.

Предикаты P (t_v …, t_n) и Р (1_и …, /") (?, и /, — термы) сравнимы, если существует унифицирующая подстановка для всех пар аргументов (?, ^ /,).

Алгоритм унификации^[1]

Для выбранных пар дизъюнктов формируется множество согласования: сопоставляются пары термов и решаются уравнения.

Для пары предикатов P (t_v …, t") и P (l_l9 …, 1_п) множество согласования задается в форме уравнения {t_x = /_t,…, t_n = /"}.

• 1. В машинном алгоритме выполняется посимвольное сравнение и выписываются пары символьных строк-термов с первым различимым символом. Для каждой пары t_x — (подстановка возможна, если один из термов — переменная и ее можно заменить частично или полностью другим термом.
• 2. Если х — у — переменные, то заменяем х/у для всех х в уравнениях множества согласования; уравнение х = у исключается в множестве согласования.
• 3. Если х = а и а — константа, то заменяем х/а для всех вхождений х в уравнения согласования.
• 4. Если х = /(г/), х не принадлежит t, то применяем x/t = x/f (y) ко всем уравнениям.

Допустимые пары согласования и соответствующие подстановки^[1]:

Рассмотрим пример унификации предикатов при сравнении Р (х, f (x)),

p (yjm-

• • согласование подстановок для хг. {(х/у), (х/у/b)} выбрано х/Ь;
• • согласование подстановок для f (x): {f (b), f (y)/f (b)}, выбрано (y/b);
• • P (b, f (b)) — унифицированный предикат;
• • две последовательные подстановки {х/у, у/b} и итоговая замена х/Ь — наибольший общий унификатор.

Пример унификации Р (а, x, f (g (y)) и P (z, f (z), f (u)):

• • выбрано для (a, z): z/a
• • для (х, /(г)): {x/z, x/z/a, x/f (a)};
• • для (g (y), и): {u/g (y)}
• • наибольший общий унификатор {z/a, x/f (a), u/g (y)}, после унификации Р (а, f (g (y))).

Формула при унификации может содержать предикаты, имеющие одинаковые предикатные символы. Применение унификации к таким предикатам возможно, если выбранная подстановка применима или терм t свободен для замещения.

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

• [1] Гринчеиков Д. ВПотоцкий С. И. Математическая логика и теория алгоритмов для программистов.
• [2] Гринчеиков Д. ВПотоцкий С. И. Математическая логика и теория алгоритмов для программистов.