SHPORA.net :: PDA

[ Back ]

Пусть С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.