Procedura Davisa-Putnama – 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ę.
Reguły systemu: 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