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

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

<p>This paper reports on using the <em>&AElig;tnaNova/Referee</em> proof-verification system to formalize issues regarding the satisfiability of CNF-formulae of propositional logic. We specify an &ldquo;archetype&rdquo; version of the Davis-Putnam-Logemann-Loveland algori...

Full description

Bibliographic Details
Main Authors: Eugenio G. Omodeo, Alexandru I. Tomescu
Format: Article
Language:English
Published: Università degli Studi di Catania 2008-05-01
Series:Le Matematiche
Subjects:
Proof checking
Program-correctness verification
Set theory
Computable set theory
Cumulative hierarchy
Satisfiability decision procedures
Proof modularization
Online Access:http://www.dmi.unict.it/ojs/index.php/lematematiche/article/view/49
Description
Summary:<p>This paper reports on using the <em>&AElig;tnaNova/Referee</em> proof-verification system to formalize issues regarding the satisfiability of CNF-formulae of propositional logic. We specify an &ldquo;archetype&rdquo; 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.</p><p><br />Within the same framework, and by resorting to the Zorn lemma, we develop a straightforward proof of the compactness theorem.</p>
ISSN:0373-3505
2037-5298

Similar Items