Rezolucja (matematyka)
![]() | Ten artykuł od 2021-06 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary) Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu. Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu. |
Rezolucja – 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
Sprowadźmy najpierw 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):
Rezolucja w działaniu:
- 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 \sigma 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ą Są trzy grupy klauzul: zawierające zawierające oraz nie zawierające ani jednego ani drugiego. Klauzule zawierające zarówno jak i są oczywiście spełnialne i nie będziemy się nimi zajmować:
Dla każdego wartościowania sprzeczne jest albo któreś albo któreś albo też któreś Utwórzmy wszystkie klauzule przez rezolucje względem
Teraz udowodnijmy, że sprzeczny jest zbiór
Jeśli w wartościowaniu któreś 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 a jako że wszystkie są w takich wartościowaniach spełnione, a to jest przynajmniej jedno niespełnione
Weźmy też identyczne wartościowanie tyle że z negatywnym Wszystkie są w tym wartościowaniu spełnione, a Tak więc jest przynajmniej jedno niespełnione
Ponieważ istnieją niespełnione i a wszystkie pary utworzyliśmy przez rezolucje, to istnieje przynajmniej jedna para która nie jest spełniona.
Tak więc z każdego zbioru klauzul sprzecznych o zmiennych możemy stworzyć zbiór klauzul sprzecznych o 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):
- przez substytucję przechodzi w
- rezolwuje się z dając
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:
- – użyta substytucja,
- – – najmniejszy unifikator i
lub też negacja będzie w zamiast w co nie zmienia dowodu.
Ponieważ i mają z definicji rozłączne zmienne Tak więc i można zunifikować w za pomocą Każdy unifikator można rozbić na najmniejszy wspólny unifikator i jakieś podstawienie – niech będzie najmniejszym wspólnym unifikatorem, a takim podstawieniem, że
Tak więc możemy zmienić ten dowód na:
- rezolwuje się z dając
- przez substytucję przechodzi w
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
- Eric W.E.W. Weisstein Eric W.E.W., Resolution Principle, [w:] MathWorld, Wolfram Research [dostęp 2020-12-12] (ang.).
- Britannica: topic/resolution-computer-logic