Преобразования

C=c,CÎS’ S’¹ c S=S₁ÚS₂

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

Алгоритм конечный, хотя количество промежуточных дизъюнктов может возрастать.

Пример:

PÚùQ 1)PÚùQ

ùPÚQ 2)ùPÚQ Расщепление по P

QÚùT 3)QÚùT

Q&T 4)ùQÚùT

5)S₁=ùQ

S₂=Q

R=(QÚùT)&(ùQÚùT)

S=S₁ÚS₂=QÚùQ - тавтология

6) QÚùT ùT – чистая литера

ùQÚùT

7) c (S выполнимо)

Теорема 4: Пусть L₁,L₂…,L_k- последовательность вычеркнутых литер по правилам 2),3) и L_k - последняя вычеркнутая литера, после которой S’= c => S – выполнима. Тогда условие L₁&L₂&…&L_k - это условие выполнимости и,соответственно, условие ù(L₁&L₂&…&L_k) – условие невыполнимости, которое можно добавить в множество гипотез для коррекции вывода.

Правило резолюций (предложено Робинсом)

Для любых дизъюнктов C₁ и C₂, для которых существует литера L в C_­1 и контрарная литера ùL в C_­2­ вычеркиваются литеры L и ùL и формируется дизъюнкция из оставшихся дизъюнктов C_­1­ и C_­2­.

C_­1­=LÚa

C_­2­=ùLÚb ®C=aÚb

Построенный дизъюнкт С называется резольвентой С_­1­ и С_­2­.

Теорема 5: Для дизъюнктов С_­1­ и С_­2­ с контрарными литерами C_­1­=LÚa и C_­2­=ùLÚb резольвента C=aÚb является логическим следствием C_­1­ и C_­2­.

Пример:

LÚa LÚa 1) LÚa 1)L =>c S невыполнимо и доказана выводимость

ùLÚb ùLÚb 2)ùLÚb 2)ùL aÚb

aÚb ù(aÚb) 3)ùa

4)ùb