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

Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество дизъюнктов пустой дизъюнкт. Если множество содержит пустой дизъюнкт, то оно противоречиво (невыполнимо). Если множество не содержит пустой дизъюнкт, то проверяется следующий факт: может ли пустой дизъюнкт быть получен из данного множества. Множество содержит пустой дизъюнкт, тогда и только тогда, когда оно пустое. Если множество можно свести к пустому, то тем самым можно доказать его противоречивость. В этом и состоит метод резолюций, который часто рассматривают как специальное правило вывода, используемое для порождения новых дизъюнктов из данного множества.

Определение 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.

Пример 11. Рассмотрим множество 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

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