Using aetnanova to formally prove that the Davis-Putnam satisfiability test is correct

  • Eugenio G. Omodeo
  • Alexandru I. Tomescu University of Bucharest
Keywords: Proof checking, Program-correctness verification, Set theory, Computable set theory, Cumulative hierarchy, Satisfiability decision procedures, Proof modularization


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.

Author Biographies

Eugenio G. Omodeo
Faculty of Mathematics and Computer Science
Alexandru I. Tomescu, University of Bucharest
Faculty of Mathematics and Computer Science