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

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

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

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