Метод Дэвиса и Патнема

По этому методу задача формулируется также в виде формулы F₁&F₂&…&F_n&ùB. Формулируется несколько правил, которые позволяют ответить на вопрос: «Выводима ли формула?», «Выполнима ли формула?» Формула невыводима, если она выполнима (существует такая интерпретация, при которой формула истинна).

Правила:

1)Правило тавтологии

Исходное рассуждение приводится к КНФ и представляет собой множество дизъюнктов S. Вычеркиваются все тавтологические дизъюнкты: (aÚùaºистина)

S^¢=c S^¢¹c

(S^¢ выполнимо и (S^¢ выполнимо или невы-

вывод опровергается) полнимо, когда S выпол

нимо или невыполнимо)

2)Правило однолитерных дизъюнктов:

а)можно вычеркнуть все однолитерные дизъюнкты, т.к. выполнимость зависит от истинности (однолитерный дизъюнкт). И оставшееся множество S^¢ выполнимо (невыполнимо) тогда и только тогда, когда S выполнимо (невыполнимо)

S^¢=c S^¢¹c

(S выполнимо) (S^¢~S)

б) если присутствуют однолитерные дизъюнкты L, и есть ещё один дизъюнкт, который содержит L, то (LÚA) тоже вычеркивается;

L&(LÚA)=L - вычёркивается

S’=c S’¹c

S – выполнимо, S’~S

В – опровергается

в) если есть однолитерные дизъюнкты L и если найдем дизъюнкту, которая содержит ùL (ùLÚA), то в дизъюнктах можно вычеркнуть ùL

L&(ùLÚA)~L&(L®A)aA

A=S’=c A=S’¹c

Множество S невы- S’~S

полнимо

Пример:

AÚB AÚB AÚB правило AÚB правило

A®C - гипотезы ùAÚC ùAÚC однолитерных ùA однолитерных c

B®D ùBÚD ùBÚD дизъюнктов ùB дизъюнктов

CÚB - доказать ù(CÚD) ùC ùC,ùD

отрицание вывода ùD

Доказано, что CÚD - теорема.

Пример:

pÚq pÚq правило p это является опровержением

ùpÚqÚùr ùpÚqÚùr однолитерных ùpÚùr ùr®c теоремы

q ùq дизъюнктов

3) Правило Дэвиса-Патнема

Правило чистых литер:

Литера L – чистая, если в множестве дизъюнктов S не существует ни одной дизъюнкты с отрицанием L (ùL). По правилу вычеркиваются все дизъюнкты, содержащие L

(LÚA₁)&(LÚA₂)

S’=S’\(LÚS)

S’=c S’¹ c

S выполнимо при L=Æ S’~S

Пример:

PÚQ PÚQ PÚQ правило

PÚùQ PÚùQ PÚùQ чистых =>c (S – выполнимо,

RÚQ RÚQ RÚQ литер ùR&Q

ùR&Q ù(ùR&Q) RÚùQ P,R

4) Правило расщепления

Множество дизъюнктов S – непустое и не применимы правила 1),2),3).

S=(LÚA₁)&(LÚA₂)&…(ùLÚB₁)&(ùLÚB₂)&…&R

R –не содержит ни L и ниùL

S₁={A₁,A₂…} – встречаются с L

S₂={B₁,B₂…} – встречаются с ùL

Утверждается, что S – выполнимо (невыполнимо) тогда и только тогда, когда S₁ÚS₂ выполнимо (невыполнимо). Можем записать

S=(LÚS₁)&(ùLÚS₂)&R

(LÚA₁)&(LÚA₂)=LÚA₁&A₂

произвольная интерпретация I

L ùL

Выполнение зависит от S₂ S₁

выполняется (не выполняется) S₁ÚS₂

Не выполняется (º c), если S₁ÚS₂ º c. Дизъюнкция S₁ÚS₂ должна быть преобразована в конъюнктивную форму:

(S₁ÚS₂) ® A₁&A₂&…&A_nÚB₁&B₂&…&B_n=(A₁ÚB₁)&(A₂ÚB₂)&…&(A_nÚB_n)

содержит n*m дизъюнктов