USING ÆTNANOVA TO FORMALLY PROVE THAT THE DAVIS-PUTNAM SATISFIABILITY TEST IS CORRECT

This paper reports on using the ÆtnaNova/Referee proof-verification system to formalize issues regarding the satisfiability of CNF-formulae of propositional logic. We specify an “archetype” version of the Davis-Putnam-Logemann-Loveland algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn lemma, we develop a straightforward proof of the compactness theorem.This paper reports on using the ÆtnaNova/Referee proof-verificationsystem to formalize issues regarding the satisfiability of CNF-formulaeof propositional logic. We specify an “archetype” version of the Davis-Putnam-Logemann-Loveland algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn lemma, we develop a straightforward proof of the compactness theorem