Правило резолюции для исчисления высказывания
Пусть С1 и С2 два предложения в исчислении высказываний и С1=Р -дизъ- С’1, C2= -дизъ- C’2, Р – пропозициональная переменная,
а С’1, C’2,предложения.
Правило вывода
С1, С2 R - называется правилом резолюций.
С’1 -дизъ- C’2
Предложения С1 и С2 называются резольвирующими (родительскими).
Многие ранее рассмотренные правила являются частным случаем правила резолюции.
Теорема :Правило резолюции дает резольвенту, которая является логическим следствием резольвируемых предложений.
Доказательство.
Если C1(I)=C2(I)=И<*>либо P(I)=И, тогда C’2(I)=И, то есть (С’1 -дизъ- C’2)(I)=И, либо P(I)=Л, тогда С’1(I)=И, то есть (С’1
-дизъ- C’2)(I)=И.
Пусть S – множество дизъюнктов. Резолютивный вывод С из S есть такая конечная последовательность С1, С2,…, Сk дизъюнктов, что
каждый Сi принадлежит S, или является резольвентой дизъюнктов, предшествующих Сi, и Ск=C.
Вывод пустого дизъюнкта <*> из S называется опровержением S (или доказательством невыполнимости (противоречивости) S).
Теорема. (полнота резолюций): Множество S дизъюнктов невыполнимо (противоречиво) тогда и только тогда, когда существует
резолютивный вывод пустого дизъюнкта <*> из S.