Rezolucja (matematyka)

Rezolucja to metoda automatycznego dowodzenia twierdzeń oparta na generowaniu nowych klauzul, aż dojdzie się do sprzeczności. W ten sposób można udowodnić, że dane twierdzenie nie jest spełnialne, lub też, co jest równoważne, że jego zaprzeczenie jest tautologią.

Rezolucja jest podstawą wielu praktycznych systemów dowodzenia twierdzeń rachunku predykatów pierwszego rzędu.

Zasady generowania nowych klauzul

Zasady generowania nowych klauzul to:

• Z klauzuli [ α ∧ β, Γ ] można utworzyć [ α, Γ ] i [ β, Γ ]
• Z klauzuli [ α ∨ β, Γ ] można utworzyć [ α, β, Γ ]
• Z pary klauzul [ α, Γ ] i [ ¬ β, Δ ], gdzie α i β się unifikują, σ zaś jest ich najmniejszym unifikatorem – [ σ(Γ); σ(Δ) ] (zasada rezolucji)

Gdzie α, β to formuły, Γ, Δ – zbiory formuł.

W rachunku zdań reguła rezolucji upraszcza się do:

• Z pary klauzul [ α, Γ ] i [ ¬ α, Δ ] można utworzyć [ Γ, Δ ]

Jeśli potrafimy dojść do klauzuli pustej rezolucja jest zakończona, i twierdzenie jest sprzeczne (a więc jego zaprzeczenie jest tautologią).

Przykład działania.

Udowodnimy że p → (p ∨ q):

Sprowadźmy najpierw ¬ (p → (p ∨ q)) do postaci z negacjami na liściach (nie jest to konieczne, ale potrzebne by były wtedy reguły usuwania każdego ze spójników oraz podwójnej negacji):

• ¬ (p → (p ∨ q))
• ¬ ((¬ p) ∨ (p ∨ q))
• p ∧ (¬ (p ∨ q))
• p ∧ ((¬ p) ∧ (¬ q))

Rezolucja w działaniu:

1. [p ∧ ((¬ p) ∧ (¬ q))]
2. [p] – z 1
3. [(¬ p) ∧ (¬ q)] – z 1
4. [¬ p] – z 3
5. [] – z 2,4 i reguły rezolucji

Istnieje wiele wersji pochodnych rezolucji, polegających na ograniczeniu możliwości stosowania reguły rezolucji w prowadzaniu dodatkowych reguł (takich jak faktoryzacja czy kondensacja), co daje lepsze praktyczne rezultaty.

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 ∧ i ∨ są trywialne, zajmijmy się więc tylko zasadą rezolucji.

Jeśli istnieje podstawienie, które jest spełnialne zarówno przez [ α, Γ ] jak i przez [ ¬ α, Δ ], i dokonujemy na tych klauzulach rezolucji, są dwie możliwości:

• α jest w tym podstawieniu prawdziwe. Wtedy wartość [ ¬ α, Δ ] jest równa wartości [ Δ ], a skoro [ Δ ] jest prawdziwe to osłabiona klauzula [Γ , Δ] też jest prawdziwa
• α jest w tym podstawieniu fałszywe. Wtedy wartość [ α, Γ ] jest równa wartości [ Γ ], a skoro [ Γ ] jest prawdziwe to osłabiona klauzula [Γ , Δ] 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 [Γ] jest spełnialne, to spełnialne jest też dowolne podstawienie [Γ]σ. W szczególności jeśli rezolwujemy [ α, Γ ] z [ ¬ β, Δ ], a σ jest unifikatorem α i β, to [ ασ, Γσ ] oraz [ ¬ βσ, Δσ ] (ασβσ) są spełnialne. Dalej prowadzi to do przypadku analogicznego do rachunku zdań:

• jeśli są spełnialne przez model gdzie ασ jest prawdziwe, to [ ¬ βσ, Δσ ] = [ ¬ ασ, Δσ ] = [ Δσ ] jest spełnialne, a więc również osłabione [ Γσ, Δσ ]
• jeśli są spełnialne przez model gdzie ασ jest faszywe, to [ ασ, Γσ ] = [ Γσ ] jest spełnialne, a więc również osłabione [ Γσ, Δσ ]

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ą $p$. Są trzy grupy klauzul: zawierające $p$, zawierające $\neg p$, oraz nie zawierające ani jednego ani drugiego. Klauzule zawierające zarówno $p$ jak i $\neg p$ są oczywiście spełnialne i nie będziemy się nimi zajmować:

• $\; [p,\Gamma_i],\; [\neg p,\Delta_j],\; [\Psi_k]$

Dla każdego wartościowania sprzeczne jest albo któreś $[\Psi_k]$, albo któreś $[p,\Gamma_i]$, albo też któreś $[\neg p,\Delta_j]$. Utwórzmy wszystkie klauzule przez rezolucje względem $p$: $[\Gamma_i, \Delta_j]$.

Teraz udowodnijmy że sprzeczny jest zbiór $[\Gamma_i, \Delta_j], [\Psi_k]$. Jeśli w wartościowaniu któreś $[\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 $p$, a jako że wszystkie $[p,\Gamma_i]$ są w takich wartościowaniach spełnione, a $[\neg p,\Delta_j] = [\Delta_j]$, to jest przynajmniej jedno niespełnione $[\Delta_j]$.

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

Ponieważ istnieją niespełnione $[\Gamma_i]$ i $[\Delta_j]$, a wszystkie pary utworzyliśmy przez rezolucje, to istnieje przynajmniej jedna para $[\Gamma_i, \Delta_j]$ która nie jest spełniona.

Tak więc z każdego zbioru klauzul sprzecznych o $n$ zmiennych możemy stworzyć zbiór klauzul sprzecznych o $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żeby 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):

• A przez substytucję przechodzi w B
• B rezolwuje się z C dając 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:

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

Lub też negacja będzie w A zamiast w C, co nie zmienia dowodu. Ponieważ $A$ i $C$ mają z definicji rozłączne zmienne $C\sigma\tau = C\tau$. Tak więc $A$ i $C$ można zunifikować w D za pomocą $C\sigma\tau$. Każdy unifikator można rozbić na najmniejszy wspólny unifikator i jakieś podstawienie – niech $\tau_1$ będzie najmniejszym wspólnym unifikatorem, a $\sigma_1$ takim podstawieniem, że $A\sigma\tau = A\tau_1\sigma_1$, $C\sigma\tau = C\tau = C\tau_1\sigma_1$.

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

• A rezolwuje się z C dając E
• E przez substytucję przechodzi w 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.

Linki zewnętrzne

• Zasada rezolucji na MathWorld (en)