Правило унификации в логике предикатов

Метод резолюций в исчислении предикатов.

Правило резолюций предполагает нахождение в дизъюнкте литерала, контрарного литералу в другом дизъюнкте. Для дизъюнктов логики высказываний это очень просто. Для дизъюнктов логики предикатов процесс усложняется, так как дизъюнкты могут содержать функции, переменные и константы.

Пример 13. Рассмотрим дизъюнкты:

C₁: P(x)Ъ Q(x),

C₂: ШP(f(x))Ъ R(x).

Не существует никакого литерала в C₁, контрарного какому-либо литералу в C₂. Однако, если подставить f(a) вместо x в C₁ и a вместо x в C₂, то исходные дизъюнкты примут вид:

C₁^’: P(f(a))Ъ Q(f(a)),

C₂^’: ШP(f(a))Ъ R(a).

Так как P(f(a)) контрарен ШP(f(a)), то можно получить резольвенту

C₃^’: Q(f(a))Ъ R(a).

В общем случае, подставив f(x) вместо x в C₁, получим

C₁^’’: P(f(x))Ъ Q(f(x)).

Литерал P(f(x)) в C₁^’’ контрарен литералу ШP(f(x)) в C₂. Следовательно, можно получить резольвенту

C₃: Q(f(x))Ъ R(x).

Таким образом, если подставлять подходящие термы вместо переменных в исходные дизъюнкты, можно порождать новые дизъюнкты. Отметим, что дизъюнкт C₃ из примера 13 является наиболее общим дизъюнктом в том смысле, что все другие дизъюнкты, порожденные правилом резолюции будут частным случаем данного дизъюнкта.

Определение 29: Подстановка q– это конечное множество вида {t₁/v₁,…,t_n/v_n}, где каждая v_i – переменная, каждый t_i – терм, отличный от v_i, все v_i различны.

Определение 30: Подстановка q называется унификатором для множества {E₁,…, E_k} тогда и только тогда, когда E₁q=E₂q=… E_kq. Множество {E₁,…, E_k} унифицируемо, если для него существует унификатор.

Прежде чем применить правило резолюции в исчислении предикатов переменные в литералах необходимо унифицировать.

Унификация производится при следующих условиях:

1. Если термы константы, то они унифицируемы тогда и только тогда, когда они совпадают.

2. Если в первом дизъюнкте терм переменная, а во втором константа, то они унифицируемы, при этом вместо переменной подставляется константа.

3. Если терм в первом дизъюнкте переменная и во втором дизъюнкте терм тоже переменная, то они унифицируемы.

4. Если в первом дизъюнкте терм переменная, а во втором - употребление функции, то они унифицируемы, при этом вместо переменной подставляется употребление функции.

5. Унифицируются между собой термы, стоящие на одинаковых местах в одинаковых предикатах.

Пример 14. Рассмотрим дизъюнкты:

1. Q(a, b, c) и Q(a, d, l). Дизъюнкты не унифицируемы.

2. Q(a, b, c) и Q(x, y, z). Дизъюнкты унифицируемы. Унификатор - Q(a, b, c).

Определение 31: Унификатор s для множества {E₁,…, E_k} будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора 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: Множество рассогласований непустого множества дизъюнктов {E₁,…, E_k} получается путем выявления первой (слева) позиции, на которой не для всех дизъюнктов из E стоит один и тот же символ, и выписывания из каждого дизъюнкта терма, который начинается с счимвола, занимающего данную позицию. Множество термов и есть множество рассогласований в E.

Пример 15. Рассмотрим дизъюнкты:

{P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}.

Множество рассогласований состоит из термов, которые начинаются с пятой позиции и представляет собой множество {f(x, y), a, g(h(k(x)))}.

Дата добавления: 2015-06-27