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

Internet

http://www.dmi.unict.it/ojs/index.php/lematematiche/article/view/49

Similar Items