Правило резолюций предполагает нахождение в дизъюнкте литерала, контрарного литералу в другом дизъюнкте. Для дизъюнктов логики высказываний это очень просто. Для дизъюнктов логики предикатов процесс усложняется, так как дизъюнкты могут содержать функции, переменные и константы.
Пример 12. Рассмотрим дизъюнкты:
C1: P(y)Ъ Q(y),
C2: ШP(f(x))Ъ R(x).
Не существует никакого литерала в C1, контрарного какому-либо литералу в C2. Однако, если подставить f(a) вместо y в C1 и a вместо x в C2, то исходные дизъюнкты примут вид:
C1’: P(f(a))Ъ Q(f(a)),
C2’: ШP(f(a))Ъ R(a).
Так как P(f(a)) контрарен ШP(f(a)), то можно получить резольвенту
C3’: Q(f(a))Ъ R(a).
В общем случае, подставив f(x) вместо y в C1, получим
C1’’: P(f(x))Ъ Q(f(x)).
Литерал P(f(x)) в C1’’ контрарен литералу ШP(f(x)) в C2. Следовательно, можно получить резольвенту
C3: Q(f(x))Ъ R(x).
Таким образом, если подставлять подходящие термы вместо переменных в исходные дизъюнкты, можно порождать новые дизъюнкты. Отметим, что дизъюнкт C3из примера 13 является наиболее общим дизъюнктом в том смысле, что все другие дизъюнкты, порожденные правилом резолюции будут частным случаем данного дизъюнкта.
Определение 29: Подстановка q– это конечное множество вида {t1/v1,…,tn/vn}, где каждая vi – переменная, каждый ti – терм, отличный от vi, все vi различны.
Определение 30: Подстановка q называется унификатором для множества {E1,…, Ek} тогда и только тогда, когда E1q=E2q=… Ekq. Множество {E1,…, Ek} унифицируемо, если для него существует унификатор.
Прежде чем применить правило резолюции в исчислении предикатов переменные в литералах необходимо унифицировать.
Унификация производится при следующих условиях:
1. Если термы константы, то они унифицируемы тогда и только тогда, когда они совпадают.
2. Если в первом дизъюнкте терм переменная, а во втором константа, то они унифицируемы, при этом вместо переменной подставляется константа.
3. Если терм в первом дизъюнкте переменная и во втором дизъюнкте терм тоже переменная, то они унифицируемы.
4. Если в первом дизъюнкте терм переменная, а во втором - употребление функции, то они унифицируемы, при этом вместо переменной подставляется употребление функции.
5. Унифицируются между собой термы, стоящие на одинаковых местах в одинаковых предикатах.
Пример 13. Рассмотрим дизъюнкты:
1. Q(a, b, c) и Q(a, d, l). Дизъюнкты не унифицируемы.
2. Q(a, b, c) и Q(x, y, z). Дизъюнкты унифицируемы. Унификатор - Q(a, b, c).
Определение 31: Унификатор s для множества {E1,…, Ek} будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора q для этого множества существует такая подстановка l, что q=s ° l, то есть q является композицией подстановок s и l.
Определение 32: Композицией подстановок s и l есть функция s ° l, определяемая следующим образом (s ° l) [t]=s[ l[t]], где t – терм, s и l - подстановки, а l[t] – терм, который получается из t путем применения к нему подстановки l.
Определение 33: Множество рассогласований непустого множества дизъюнктов {E1,…, Ek} получается путем выявления первой (слева) позиции, на которой не для всех дизъюнктов из E стоит один и тот же символ, и выписывания из каждого дизъюнкта терма, который начинается с символа, занимающего данную позицию. Множество термов и есть множество рассогласований в E.
Пример 14. Рассмотрим дизъюнкты:
{P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}.
Множество рассогласований состоит из термов, которые начинаются с пятой позиции и представляет собой множество {f(x, y), a, g(h(k(x)))}.
Алгоритм унификации для нахождения наиболее общего унификатора.
Пусть E – множество дизъюнктов, D – множество рассогласований, k – номер итерации, sk наиболее общий унификатор на k-ой итерации.
Шаг 2. Если для Ek не существует множества рассогласований Dk, то остановка: sk – наиболее общий унификатор для E. Иначе найдем множество рассогласований Dk.
Шаг 3. Если существуют такие элементы vk и tk в Dk, что vk переменная, не входящая в терм tk, то перейдем к шагу 4. В противном случае остановка: E не унифицируемо.
Шаг 4. Пусть sk+1=sk { tk / vk}, заменим во всех дизъюнктах Ek tk на vk.
