Tekst źródłowy strony Rezolucja (matematyka)

{{dopracować|źródła=2021-06}}
{{spis treści}}
'''Rezolucja''' – metoda [[automatyczne dowodzenie twierdzeń|automatycznego dowodzenia twierdzeń]] oparta na generowaniu nowych [[klauzula (matematyka)|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 [[Tautologia (logika)|tautologią]].

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

== Zasady generowania nowych klauzul ==
Zasady generowania nowych klauzul to:
* z klauzuli <math>[\alpha \land \beta, \Gamma]</math> można utworzyć <math>[\alpha, \Gamma]</math> i <math>[\beta, \Gamma],</math>
* z klauzuli <math>[\alpha \lor \beta, \Gamma]</math> można utworzyć <math>[\alpha, \beta, \Gamma],</math>
* z pary klauzul <math>[\alpha, \Gamma]</math> i <math>[\lnot \beta, \Delta],</math> gdzie <math>\alpha</math> i <math>\beta</math> się [[unifikacja (logika)|unifikują]], <math>\sigma</math> zaś jest ich ''najmniejszym unifikatorem'' – <math>[\sigma(\Gamma); \sigma(\Delta)]</math> (zasada rezolucji),

gdzie <math>\alpha, \beta</math> to formuły, <math>\Gamma, \Delta</math> – zbiory formuł.

W [[rachunek zdań|rachunku zdań]] reguła rezolucji upraszcza się do:
* Z pary klauzul <math>[\alpha, \Gamma]</math> i <math>[\lnot \alpha, \Delta]</math> można utworzyć <math>[\Gamma, \Delta].</math>

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 <math>\mathrm{p \to (p \lor q)}{:}</math>

Sprowadźmy najpierw <math>\mathrm{\lnot (p \to (p \lor q))}</math> do postaci z [[negacja]]mi 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):
* <math>\mathrm{\lnot (p \to (p \lor q))}</math>
* <math>\mathrm{\lnot ((\lnot p) \lor (p \lor q))}</math>
* <math>\mathrm{p \land (\lnot (p \lor q))}</math>
* <math>\mathrm{p \land ((\lnot p) \land (\lnot q))}</math>

Rezolucja w działaniu:
# <math>\mathrm{[p \land ((\lnot p) \land (\lnot q))]}</math>
# <math>\mathrm{[p] - z\ 1}</math>
# <math>\mathrm{[(\lnot p) \land (\lnot q)] - z\ 1}</math>
# <math>\mathrm{[\lnot p] - z\ 3}</math>
# <math>\mathrm{[] - z\ 2,4}</math> 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 [[Rozkład na czynniki|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 <math>\land</math> i <math>\lor</math> są trywialne, zajmijmy się więc tylko zasadą rezolucji.

Jeśli istnieje podstawienie, które jest spełnialne zarówno przez <math>[\alpha, \Gamma],</math> jak i przez <math>[\lnot \alpha, \Delta],</math> i dokonujemy na tych klauzulach rezolucji, są dwie możliwości:
* <math>\alpha</math> jest w tym podstawieniu prawdziwe. Wtedy wartość <math>[\lnot \alpha, \Delta]</math> jest równa wartości <math>[\Delta],</math> a skoro <math>[\Delta]</math> jest prawdziwe to osłabiona klauzula <math>[\Gamma, \Delta]</math> też jest prawdziwa
* <math>\alpha</math> jest w tym podstawieniu fałszywe. Wtedy wartość <math>[\alpha, \Gamma]</math> jest równa wartości <math>[\Gamma],</math> a skoro <math>[\Gamma]</math> jest prawdziwe to osłabiona klauzula <math>[\Gamma, \Delta]</math> 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 <math>[\Gamma]</math> jest spełnialne, to spełnialne jest też dowolne podstawienie <math>[\Gamma]\sigma.</math> W szczególności jeśli rezolwujemy <math>[\alpha, \Gamma]</math> z <math>[\lnot \beta, \Delta],</math> a \sigma jest unifikatorem <math>\alpha</math> i <math>\beta,</math> to <math>[\alpha\sigma, \Gamma\sigma]</math> oraz <math>[\lnot \beta\sigma, \Delta\sigma] (\alpha\sigma\beta\sigma)</math> są spełnialne. Dalej prowadzi to do przypadku analogicznego do rachunku zdań:
* jeśli są spełnialne przez model gdzie <math>\alpha\sigma</math> jest prawdziwe, to <math>[\lnot \beta\sigma, \Delta\sigma] = [\lnot \alpha\sigma, \Delta\sigma] = [\Delta\sigma]</math> jest spełnialne, a więc również osłabione <math>[\Gamma\sigma, \Delta\sigma]</math>
* jeśli są spełnialne przez model, gdzie <math>\alpha\sigma</math> jest faszywe, to <math>[\alpha\sigma, \Gamma\sigma] = [\Gamma\sigma]</math> jest spełnialne, a więc również osłabione <math>[\Gamma\sigma, \Delta\sigma].</math>

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

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

Teraz udowodnijmy, że sprzeczny jest zbiór <math>[\Gamma_i, \Delta_j], [\Psi_k].</math>

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

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

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

Tak więc z każdego zbioru klauzul sprzecznych o <math>n</math> zmiennych możemy stworzyć zbiór klauzul sprzecznych o <math>n-1</math> 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, [[skolemizacja|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 [[Struktura matematyczna|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 [[twierdzenie o zwartości|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):
* <math>A</math> przez substytucję przechodzi w <math>B,</math>
* <math>B</math> rezolwuje się z <math>C</math> dając <math>D.</math>

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:
* <math>A = [\alpha,\Delta],</math>
* <math>B = [\alpha\sigma,\Delta\sigma],</math> <math>\sigma</math> – użyta substytucja,
* <math>C = [\neg\beta,\Gamma],</math>
* <math>D = [\Delta\sigma\tau, \Gamma\tau]</math> – <math>\tau</math> – najmniejszy unifikator <math>\alpha\sigma</math> i <math>\beta,</math>

lub też negacja będzie w <math>A</math> zamiast w <math>C,</math> co nie zmienia dowodu.

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

Tak więc możemy zmienić ten dowód na:
* <math>A</math> rezolwuje się z <math>C</math> dając <math>E,</math>
* <math>E</math> przez substytucję przechodzi w <math>D.</math>

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 ==
* {{MathWorld|adres=ResolutionPrinciple |tytuł=Resolution Principle |data dostępu=12 grudnia 2020}}

{{Kontrola autorytatywna}}

[[Kategoria:Logika matematyczna]]