Dowód niesprzeczności rezolucji

Jeśli dany skończony zbiór klauzul jest spełnialny, nie uda nam się udowodnić jego fałszywości przez rezolucję. Zasady pozbywania się spójników ${\displaystyle \land }$ i ${\displaystyle \lor }$ są trywialne, zajmijmy się więc tylko zasadą rezolucji.

Jeśli istnieje podstawienie, które jest spełnialne zarówno przez ${\displaystyle [\alpha ,\Gamma ],}$ jak i przez ${\displaystyle [\lnot \alpha ,\Delta ],}$ i dokonujemy na tych klauzulach rezolucji, są dwie możliwości:

• ${\displaystyle \alpha }$ jest w tym podstawieniu prawdziwe. Wtedy wartość ${\displaystyle [\lnot \alpha ,\Delta ]}$ jest równa wartości ${\displaystyle [\Delta ],}$ a skoro ${\displaystyle [\Delta ]}$ jest prawdziwe to osłabiona klauzula ${\displaystyle [\Gamma ,\Delta ]}$ też jest prawdziwa
• ${\displaystyle \alpha }$ jest w tym podstawieniu fałszywe. Wtedy wartość ${\displaystyle [\alpha ,\Gamma ]}$ jest równa wartości ${\displaystyle [\Gamma ],}$ a skoro ${\displaystyle [\Gamma ]}$ jest prawdziwe to osłabiona klauzula ${\displaystyle [\Gamma ,\Delta ]}$ też jest prawdziwa,

czyli rezolucja dwóch klauzul spełnialnych nie może dać klauzuli niespełnialnej.

W rachunku predykatów pierwszego rzędu, niech jeśli ${\displaystyle [\Gamma ]}$ jest spełnialne, to spełnialne jest też dowolne podstawienie ${\displaystyle [\Gamma ]\sigma .}$ W szczególności jeśli rezolwujemy ${\displaystyle [\alpha ,\Gamma ]}$ z ${\displaystyle [\lnot \beta ,\Delta ],}$ a \sigma jest unifikatorem ${\displaystyle \alpha }$ i ${\displaystyle \beta ,}$ to ${\displaystyle [\alpha \sigma ,\Gamma \sigma ]}$ oraz ${\displaystyle [\lnot \beta \sigma ,\Delta \sigma ](\alpha \sigma \beta \sigma )}$ są spełnialne. Dalej prowadzi to do przypadku analogicznego do rachunku zdań:

• jeśli są spełnialne przez model gdzie ${\displaystyle \alpha \sigma }$ jest prawdziwe, to ${\displaystyle [\lnot \beta \sigma ,\Delta \sigma ]=[\lnot \alpha \sigma ,\Delta \sigma ]=[\Delta \sigma ]}$ jest spełnialne, a więc również osłabione ${\displaystyle [\Gamma \sigma ,\Delta \sigma ]}$
• jeśli są spełnialne przez model, gdzie ${\displaystyle \alpha \sigma }$ jest faszywe, to ${\displaystyle [\alpha \sigma ,\Gamma \sigma ]=[\Gamma \sigma ]}$ jest spełnialne, a więc również osłabione ${\displaystyle [\Gamma \sigma ,\Delta \sigma ].}$

Dowód zupełności rezolucji w rachunku zdań

Udowodnijmy, że jeśli dany zbiór klauzul (po zastosowaniu wszystkich reguł dla eliminacji spójników) jest sprzeczny, dojdziemy za pomocą rezolucji do klauzuli pustej.

Weźmy dowolną zmienną ${\displaystyle p.}$ Są trzy grupy klauzul: zawierające ${\displaystyle p,}$ zawierające ${\displaystyle \neg p,}$ oraz nie zawierające ani jednego ani drugiego. Klauzule zawierające zarówno ${\displaystyle p,}$ jak i ${\displaystyle \neg p}$ są oczywiście spełnialne i nie będziemy się nimi zajmować:

• ${\displaystyle [p,\Gamma _{i}],\;[\neg p,\Delta _{j}],\;[\Psi _{k}].}$

Dla każdego wartościowania sprzeczne jest albo któreś ${\displaystyle [\Psi _{k}],}$ albo któreś ${\displaystyle [p,\Gamma _{i}],}$ albo też któreś ${\displaystyle [\neg p,\Delta _{j}].}$ Utwórzmy wszystkie klauzule przez rezolucje względem ${\displaystyle p{:}}$ ${\displaystyle [\Gamma _{i},\Delta _{j}].}$

Teraz udowodnijmy, że sprzeczny jest zbiór ${\displaystyle [\Gamma _{i},\Delta _{j}],[\Psi _{k}].}$

Jeśli w wartościowaniu któreś ${\displaystyle [\Psi _{k}]}$ nie było spełnione, to nowy zbiór – ponieważ też zawiera tę klauzulę – też nie spełnia tego wartościowania.

Rozpatrzmy więc przypadek kiedy tak nie jest. Ponieważ żadne wartościowanie nie spełnia tego zbioru, to nie spełnia go też żadne wartościowanie z pozytywnym ${\displaystyle p,}$ a jako że wszystkie ${\displaystyle [p,\Gamma _{i}]}$ są w takich wartościowaniach spełnione, a ${\displaystyle [\neg p,\Delta _{j}]=[\Delta _{j}],}$ to jest przynajmniej jedno niespełnione ${\displaystyle [\Delta _{j}].}$

Weźmy też identyczne wartościowanie tyle że z negatywnym ${\displaystyle p.}$ Wszystkie ${\displaystyle [\neg p,\Delta _{j}]}$ są w tym wartościowaniu spełnione, a ${\displaystyle [p,\Gamma _{i}]=[\Gamma _{i}].}$ Tak więc jest przynajmniej jedno niespełnione ${\displaystyle [\Gamma _{i}].}$

Ponieważ istnieją niespełnione ${\displaystyle [\Gamma _{i}]}$ i ${\displaystyle [\Delta _{j}],}$ a wszystkie pary utworzyliśmy przez rezolucje, to istnieje przynajmniej jedna para ${\displaystyle [\Gamma _{i},\Delta _{j}]}$ która nie jest spełniona.

Tak więc z każdego zbioru klauzul sprzecznych o ${\displaystyle n}$ zmiennych możemy stworzyć zbiór klauzul sprzecznych o ${\displaystyle n-1}$ zmiennych, dochodząc w ten sposób w końcu do klauzuli pustej (przy okazji zwiększając liczbę klauzul wykładniczo).

Dowód zupełności rezolucji w rachunku predykatów pierwszego rzędu

Przypadek bez zmiennych jest trywialny – każdemu termowi przyporządkowujemy pewną zmienną zdaniową i dowód postępuje identycznie jak dla rachunku zdań.

Skończony, skolemizowany zbiór klauzul rachunku predykatów pierwszego rzędu odpowiada nieskończonemu zbiorowi wynikłemu z wszystkich możliwych podstawień zmiennych. „Dowolne” modele są jednak zbyt trudne – mogą one np. być nieprzeliczalne. Na szczęście zachodzi twierdzenie:

Jeśli istnieje model dla danego zbioru formuł rachunku predykatów pierwszego rzędu, to istnieje taki model Herbranda.

Modele Herbranda są przeliczalne i składają się z termów. Tak więc nieskończony zbiór klauzul będzie przeliczalnym zbiorem klauzul rachunku zdań.

Dodajmy do rezolucji dodatkową zasadę – zasadę substytucji – mówiącą, że możemy podstawić dowolne wyrażenie za daną zmienną – i będziemy podstawiać w taki sposób że kiedyś podstawimy wszystko co podstawić można w każde możliwe miejsce (czyli nałożymy na podstawienia jakiś porządek i będziemy podstawiać w końcu do każdej klauzuli którą mamy). Zgodnie z twierdzeniem o zwartości każdy sprzeczny zbiór formuł rachunku zdań ma sprzeczny podzbiór skończony. Tak więc odpowiednio podstawiając w końcu uzyskamy taki podzbiór, a że dla rachunku zdań rezolucja jest zupełna, razem z taką regułą dostajemy system zupełny.

Teraz wystarczy dowód korzystający z zasady substytucji przekształcić na dowód nie korzystający z tej zasady. Dowód składa się z kroków substytucji i rezolucji oraz klauzul powstałych w ich wyniku. Jeśli pewna klauzula została uzyskana w drodze substytucji, i wykorzystaliśmy ją również jedynie do substytucji, może by zastąpić tę parę jedną substytucją.

Ponieważ w końcu uzyskujemy klauzulę pustą ostatnim krokiem dowodu musi być rezolucja – substytucja nie może prowadzić do zmniejszenia liczby elementów klauzuli.

Teraz wyeliminujmy pozostałe substytucje – jedyne substytucje jakie mamy w dowodzie to substytucje klauzul, które potem będą wykorzystywane do rezolucji – ponieważ w przeciwnym wypadku ich wykluczenie nie psuje dowodu. Tak więc weźmy dowolny fragment dowodu postaci (nie muszą być one jedno po drugim w liniowej reprezentacji dowodu):

• ${\displaystyle A}$ przez substytucję przechodzi w ${\displaystyle B,}$
• ${\displaystyle B}$ rezolwuje się z ${\displaystyle C}$ dając ${\displaystyle D.}$

Ponieważ mamy przynajmniej jedną rezolucję, przynajmniej jedną substytucję (w przeciwnym wypadku dowód jest skończony), a każda substytucja jest użyta w rezolucji, zawsze będzie taki fragment. Rozpisując te wyrażenia będzie to:

• ${\displaystyle A=[\alpha ,\Delta ],}$
• ${\displaystyle B=[\alpha \sigma ,\Delta \sigma ],}$ ${\displaystyle \sigma }$ – użyta substytucja,
• ${\displaystyle C=[\neg \beta ,\Gamma ],}$
• ${\displaystyle D=[\Delta \sigma \tau ,\Gamma \tau ]}$ – ${\displaystyle \tau }$ – najmniejszy unifikator ${\displaystyle \alpha \sigma }$ i ${\displaystyle \beta ,}$

lub też negacja będzie w ${\displaystyle A}$ zamiast w ${\displaystyle C,}$ co nie zmienia dowodu.

Ponieważ ${\displaystyle A}$ i ${\displaystyle C}$ mają z definicji rozłączne zmienne ${\displaystyle C\sigma \tau =C\tau .}$ Tak więc ${\displaystyle A}$ i ${\displaystyle C}$ można zunifikować w ${\displaystyle D}$ za pomocą ${\displaystyle C\sigma \tau .}$ Każdy unifikator można rozbić na najmniejszy wspólny unifikator i jakieś podstawienie – niech ${\displaystyle \tau _{1}}$ będzie najmniejszym wspólnym unifikatorem, a ${\displaystyle \sigma _{1}}$ takim podstawieniem, że ${\displaystyle A\sigma \tau =A\tau _{1}\sigma _{1},}$ ${\displaystyle C\sigma \tau =C\tau =C\tau _{1}\sigma _{1}.}$

Tak więc możemy zmienić ten dowód na:

• ${\displaystyle A}$ rezolwuje się z ${\displaystyle C}$ dając ${\displaystyle E,}$
• ${\displaystyle E}$ przez substytucję przechodzi w ${\displaystyle D.}$

Teraz (pamiętając o składaniu substytucji) dojdziemy w końcu do sytuacji gdzie przenosimy substytucję (która mogła już osiągnąć gigantyczne rozmiary) przez ostatnią rezolucje. Ponieważ jednak podstawienie to zachodzi dla klauzuli pustej – w rzeczywistości możemy je zupełnie odrzucić.

Tak więc rezolucja bez dodatkowych zasad jest zupełna.