Procedura Davisa-Putnama
Procedura Davisa-Putnama to efektywny system dowodzenia twierdzeń w rachunku zdań. Choć istnieją modyfikacje dla rachunku predykatów pierwszego rzędu, zazwyczaj są one mniej wydajne niż rezolucja.
Podstawowa idea polega na zamianie negacji formuły, którą chcemy udowodnić, na alternatywę koniunkcji alternatyw literałów, określaną jako zbiór klauzul. Alternatywę tych zbiorów nazywamy blokiem.
Reguły systemu
- Subsumpcja: Jeśli klauzula C subsumuje klauzulę D (wszystkie literały C są także w D), usuwamy D.
- Usuwanie klauzul: Jeśli literał występuje tylko pozytywnie lub negatywnie, usuwamy wszystkie klauzule, które go zawierają.
- Usuwanie pojedynczych literałów: Jeśli klauzula to pojedynczy literał, usuwamy wszystkie klauzule zawierające ten literał oraz jego negację z innych klauzul.
- Splitting: Jeśli literał występuje zarówno pozytywnie, jak i negatywnie, dzielimy zbiór na dwa:
- Jeden zbiór, w którym usunięto klauzule zawierające literał oraz jego negację.
- Drugi zbiór, w którym usunięto wszystkie wystąpienia literału oraz klauzule zawierające jego negację.
- Usuwanie klauzuli pustej: Klauzula pusta, mająca wartość fałsz, eliminuje inne klauzule przez subsumpcję. Taki zbiór klauzul jest nieistotny dla bloku.
Jeśli blok nie zawiera już zbiorów klauzul, twierdzenie zostało udowodnione, co oznacza, że jego negacja jest fałszywa. W przeciwnym przypadku, jeśli pozostał pusty zbiór klauzul, twierdzenie jest fałszywe, a jego zaprzeczenie jest spełnialne.
Kategoria: Automatyczne dowodzenie twierdzeń
