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

Abstract

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
Published
2008-08-06
Section
Articoli