期刊论文详细信息
Le Matematiche | |
Using aetnanova to formally prove that the Davis-Putnam satisfiability test is correct | |
关键词: Proof checking; Program-correctness verification; Set theory; Computable set theory; Cumulative hierarchy; Satisfiability decision procedures; Proof modularization; | |
DOI : | |
来源: DOAJ |
【 摘 要 】
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.
【 授权许可】
Unknown