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

Определение 24:Если A атом, то литералы A и ØA контрарны друг другу, и множество { A, ØA } называется контрарной парой.

Отметим, что дизъюнкт есть тавтология, если он содержит контрарную пару.

Определение 25: Правило резолюций состоит в следующем:

Для любых двух дизъюнктов C₁ и C₂, если существует литерал L₁ в C₁, который контрарен литералу L₂ в C₂, то вычеркнув L₁ и L₂ из C₁ и C₂ соответственно и построив дизъюнкцию оставшихся дизъюнктов, получим резолюцию (резольвенту) C₁ и C₂.

Пример 9: рассмотрим следующие дизъюнкты:

C₁: PÚ R,

C₂: ØPÚ Q.

Дизъюнкт C₁ имеет литерал P, который контрарен литералу ØP в C₂. Следовательно, вычеркивая P и ØP из C₁ и C₂ соответственно, построим дизъюнкцию оставшихся дизъюнктов R и Q и получим резольвенту RÚ Q.

Важным своством резольвенты является то, что любая резольвента двух дизъюнктов C₁ и C₂ есть логическое следствие C₁ и C₂. Это устанавлисвается в следующей теореме.

Теорема 4. Пусть даны два дизъюнкта C₁ и C₂. Тогда резольвента C дизъюнктов C₁ и C₂ есть логическое следствие C₁ и C₂.

Если есть два единичных дизъюнкта, то их резольвента, если она существует, есть пустой дизъюнкт ÿ. Более существенно, что для невыполнимого множества дизъюнктов многократным применением правила резолюций можно породить ÿ.

Определение 26: Пусть S – множество дизъюнктов. Резолютивный вывод C из S есть такая конечная последовательность С₁, C₂,…, C_k дизъюнктов, что каждый C_i или принадлежит S или является резольвентой дизъюнктов, предшествующих C_i, и C_k=C. Вывод ÿ из S называется опровержением (или доказательством невыполнимости ) S.

Пример 10. Рассмотрим множество S:

1. ØPÚ Q,

2. Ø Q,

3. P.

Из 1 и 2 получим резольвенту

4. ØP.

Из 4 и 3 получим резольвенту

5. ÿ.

Так как ÿ получается из S применениями правила резолюций , то согласно теореме 4 ÿ есть логическое следствие S, следовательно S невыполнимо.

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

Определение 27: Фразой называется дизъюнкт, у которого негативные литералы размещаются после позитивных литералов в конце дизъюнкта.

Пример 11: Р₁ ÚР₂ Ú…Р_n Ú ØN₁ Ú ØN₂…Ú ØN_m

Определение 28: Фраза Хорна это фраза, содержащая только один позитивный литерал.

Пример 12: преобразовать фразу Хорна в обратную импликацию.

Р Ú ØN₁ Ú ØN₂…Ú ØN_m

ØN₁ Ú ØN₂…Ú ØN_m =Ø (N₁ Ù N₂ Ù…ÙN_m)

P¬ (N₁ Ù N₂ Ù…ÙN_m)

P¬ N₁, N₂,…N_m

При представлении дизъюнктов фразами Хорна негативные литералы соответствуют гипотезам, а позитивный литерал представляет заключение. Единичный позитивный дизъюнкт представляет некоторый факт, то есть заключение, не зависящее ни от каких гипотез. Часто задача состоит в том, что надо проверить некоторую формулу, называемую целью, логически выведенную из множества правил и фактов. Резолюция является методом доказательства от противного: исходя из фактов, правил и отрицания цели, приходим к противоречию (пустому дизъюнкту).

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

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

Пример 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)))}.