zbMATH — the first resource for mathematics

Extracting the resolution algorithm from a completeness proof for the propositional calculus. (English) Zbl 1132.03316
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 147-161 (2007).
Summary: We prove constructively that for any propositional formula \(\varphi \) in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of \(\varphi \) showing that it is unsatisfiable. This refutation is a resolution proof of \(\lnot \varphi \). From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.
For the entire collection see [Zbl 1121.03005].
Reviewer: Reviewer (Berlin)
03B35 Mechanization of proofs and logical operations
03B05 Classical propositional logic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Coq; Haskell
Full Text: DOI