Procedura Davisa-Putnama

Z Wikipedii

Procedura Davisa-Putnama to bardzo efektywny system dowodzenia twierdzeń dla rachunku zdań. Istnieją też jego modyfikacje dla rachunku predykatów pierwszego rzędu, jednak są one zwykle mniej wydajne od rezolucji.

Idea jest następująca: negację formuły którą zamierzamy udowodnić zamieniamy na alternatywę koniunkcji alternatyw literałów, czyli alternatywę CNFów. Taki CNF nazywa się tu zbiorem klauzul, natomiast alternatywa CNFów blokiem.

Następnie usuwamy wszystkie powtórzenia literałów i fałsze, oraz wszystkie klauzule zawierające jednocześnie literał i jego negację lub też prawdę.

Teraz mamy następujące reguły:

subsumpcja - jeśli w pewnym zbiorze klauzul klauzula C subsumuje klauzulę D, czyli wszystkie literały C występują też w D, to usuwamy D.
jeśli w pewnym zbiorze klauzul jakiś literał występuje tylko pozytywnie lub tylko negatywnie, usuwamy z niego wszystkie klauzule które go zawierają
jeśli w pewnym zbiorze klauzul jakaś klauzula to pojedynczy literał, usuwamy wszystkie klauzule zawierające ten literał, oraz zaprzeczenie tego literału z wszystkich klauzul zbioru które go zawierały
splitting - jeśli w pewnym zbiorze klauzul pewien literał występuje zarówno pozytywnie jak i negatywnie zastępujemy cały zbiór dwoma zbiorami:
- jednym w którym usunięte zostały wszystkie klauzule zawierające ten literał, oraz wszystkie wystąpienia jego negacji
- drugim w którym usunięte zostały wszystkie wystąpienia tego literału, oraz wszystkie klauzule zawierające jego negację
usuwamy każdy zbiór klauzul zawierają klauzulę pustą
- Wyjaśnienie: klauzula ta usuwa wszystkie inne przez subsumpcje i ma wartość fałsz, a co za tym idzie zbiór klauzul ma wartość fałsz, która jest nieistotna dla bloku będącego alternatywą)

Jeśli w bloku nie ma już zbiorów klauzul twierdzenie zostało udowodnione (taki blok, jako alternatywa, jest fałszywy - skoro negacja formuły jest fałszywa, to twierdzenie to jest prawdziwe). Jeśli został jakiś pusty zbiór klauzul, twierdzenie to jest fałszywe (jego zaprzeczenie jest spełnialne).