Унификатор двух термов.
Унификатором двух термов называется подстановка, которая делает термы одинаковыми.
Терм1 f(x) Терм2 у
а) унификатор {х = а; у = f(a)} – подстановка
f(a) f(a)
б) унификатор {x = z; y = f(z)} - подстановка
f(z) f(z)
Если существует унификатор двух термов, то они называются унифицируемыми.
Легко видеть, что любой унификатор определяет общий пример, и обратно: любой общий пример определяет унификатор.
- в случае а) общим примером для f(x) и у является f(a)
- в случае б) общим примером для f(x) и у является f(z)
наиболее общим унификатором двух термов называется унификатор, соответствующий наиболее общему примеру:
для f(x) и у унификатор примера б), то есть {x = z; y = f(z)} является наиболее общим унификатором.
Если два терма унифицируемы, то существует единственный наиболее общий унификатор. Единственность определена с точностью до
переименования переменных (например, f(z) и f(t)).
Определим основные компоненты алгоритма унификации (нахождения наиболее общего унификатора) двух термов. Если термы не
унифицируемы, алгоритм должен сообщить об отказе.
1. Константы унифицируемы, когда они совпадают
2. Переменные унифицируемы со всеми (константы, переменные, термы)
3. Термы унифицируемы тогда и только тогда, когда их названия совпадают и унифицируемы между собой соответствующие аргументы.
Теперь мы в состоянии обобщить понятие резольвента двух дизъюнктов и правило резолюций для исчисления предикатов.
Пусть дизъюнкты С1 и С2 исчисления предикатов имеют вид: и L1 и L2 имеют наибольший общий унификатор q (т.е. L1q и L2q
совпадают, а L1q и L2q - контрарная пара), тогда С1 и С2 называется дизъюнктор q q, а правило резолюций .
Заметим, что в С1 и С2 все переменные связаны, а значит, в L1 и L2 нет одинаковых переменных, что упрощает поиск унификатора.
Теорема: резольвента является логическим следствием резольвируемых дизъюнктив (т.к. контрарные пары не могут дать истинность,
а истинность заключена либо в либо в, а значит в