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

MaRDI QIDQ3645586zbMATH OpenFDO

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

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)

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

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)