Rezolucja (matematyka)

Z Wikipedii

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ą.

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:

[p ∧ ((¬ p) ∧ (¬ q))]
[p] - z 1
[(¬ p) ∧ (¬ q)] - z 1
[¬ p] - z 3
[] - z 1,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.

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

Spis treści

1 Dowód niesprzeczności rezolucji
2 Dowód zupełności rezolucji w rachunku zdań
3 Dowód zupełności rezolucji w rachunku predykatów pierwszego rzędu
4 Zobacz też

[edytuj] 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 [ Γσ, Δσ ]

[edytuj] 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,Γ i]$
$[\neg p,\Delta_j]$
$[Ψ k]$

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

Teraz udowodnijmy że sprzeczny jest zbiór $[Γ i,Δ j],[Ψ k]$ . Jeśli w wartościowaniu któreś $[Ψ 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,Γ i]$ są w takich wartościowaniach spełnione, a $[\neg p,\Delta_j] = [\Delta_j]$ , to jest przynajmniej jedno niespełnione $[Δ 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,Γ i] = [Γ i]$ . Tak więc jest przynajmniej jedno niespełnione $[Γ i]$ .

Ponieważ istnieją niespełnione $[Γ i]$ i $[Δ j]$ , a wszystkie pary utworzyliśmy przez rezolucje, to istnieje przynajmniej jedna para $[Γ i,Δ 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).

[edytuj] 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 zeskolemizowany 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 = [α,Δ]$
$B = [ασ,Δσ]$ , $σ$ - użyta substytucja
$C = [\neg\beta,\Gamma]$
$D = [Δστ,Γτ]$ - $τ$ - najmniejszy unifikator $ασ$ i $β$

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 στ = C τ$ . Tak więc $A$ i $C$ można zunifikować w D za pomocą $C στ$ . Każdy unifikator można rozbić na najmniejszy wspólny unifikator i jakieś podstawienie - niech $τ 1$ będzie najmniejszym wspólnym unifikatorem, a $σ 1$ takim podstawieniem, że $A στ = A τ 1 σ 1$ , $C στ = C τ = C τ 1 σ 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.