Using aetnanova to formally prove that the Davis-Putnam satisfiability test is correct
Keywords:
Proof checking, Program-correctness verification, Set theory, Computable set theory, Cumulative hierarchy, Satisfiability decision procedures, Proof modularizationAbstract
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.
Downloads
Published
Issue
Section
License
The authors retain all rights to the original work without any restrictions.
License for Published Contents
"Le Matematiche" published articlesa are distribuited with Creative Commons Attribution 4.0 International. You are free to copy, distribute and transmit the work, and to adapt the work. You must attribute the work in the manner specified by the author or licensor (but not in any way that suggests that they endorse you or your use of the work).
License for Metadata
"Le Matematiche" published articles metadata are dedicated to the public domain by waiving all publisher's rights to the work worldwide under copyright law, including all related and neighboring rights, to the extent allowed by law.
You can copy, modify, distribute and perform the work, even for commercial purposes, all without asking permission.
No Fee Charging
No fee is required to complete the submission/review/publishing process of authors paper.
