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

zbMATH Open1180.03015MaRDI QIDQ3645586FDOQ3645586

Authors: Alexandru I. Tomescu, Eugenio Omodeo 

Publication date: 18 November 2009

Full work available at URL: http://www.dmi.unict.it/ojs/index.php/lematematiche/article/view/49

Recommendations

• scientific article; zbMATH DE number 5713654
• scientific article; zbMATH DE number 956865
• Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• The mechanical verification of a DPLL-based satisfiability solver
• Implementing the Davis-Putnam method

zbMATH Keywords

proof checkingcumulative hierarchycomputable set theoryproof modularizationprogram-correctness verificationproof-verification systemsatisfiability decision procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Axiomatics of classical set theory and its fragments (03E30)

Cited In (1)

• Banishing ultrafilters from our consciousness

This page was built for publication: Using ÆtnaNova to formally prove that the Davis-Putnam satisfiability test is correct

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3645586)