Extracting the resolution algorithm from a completeness proof for the propositional calculus. (English) Zbl 1221.03015
Summary: We prove constructively that, for any propositional formula \(\phi\) in conjunctive normal form, we can either find a satisfying assignment of true and false to its variables, or a refutation of \(\phi\) showing that it is unsatisfiable. This refutation is a resolution proof of \(\lnot \phi\). 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.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B05 | Classical propositional logic |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
type theory; resolution; program extraction; automated reasoning; intuitionism; Coq; Haskell programReferences:
| [1] | Chang, C. C.; Keisler, H. J., (Model Theory. Model Theory, Studies in Logic and the Foundations of Mathematics, vol. 73 (1973), North-Holland: North-Holland Netherlands) · Zbl 0276.02032 |
| [2] | Constable, R. L.; Allen, S. F.; Bromley, H. M.; Cleaveland, W. R.; Cremer, J. F.; Harper, R. W.; Howe, D. J.; Knoblock, T. B.; Mendler, N. P.; Panangaden, P.; Sasaki, J. T.; Smith, S. F., Implementing Mathematics with the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall NJ |
| [3] | Constable, R. L.; Howe, D. J., Implementing metamathematics as an approach to automatic theorem proving, (Banerji, R. B., Formal Techniques in Artificial Intelligence: A Source Book (1990), Elsevier Science Publishers: Elsevier Science Publishers North-Holland), 45-76 · Zbl 0704.68094 |
| [4] | Constable, R.; Moczydłowski, W., Extracting programs from constructive HOL proofs via IZF set-theoretic semantics, (Proceedings of 3rd International Joint Conference on Automated Reasoning. Proceedings of 3rd International Joint Conference on Automated Reasoning, IJCAR 2006. Proceedings of 3rd International Joint Conference on Automated Reasoning. Proceedings of 3rd International Joint Conference on Automated Reasoning, IJCAR 2006, Lecture Notes in Computer Science, vol. 4130 (2006), Springer), 162-176 · Zbl 1222.68359 |
| [5] | Gallier, J. H., Logic for Computer Science, Foundations of Automatic Theorem Proving (1986), Harper and Row: Harper and Row NY · Zbl 0605.03004 |
| [6] | Gallier, J. H., The completeness of propositional resolution: A simple and constructive proof, Logical Methods in Computer Science, 2, 5, 1-7 (2006) · Zbl 1127.03008 |
| [7] | Lewis, H. R.; Papadimitriou, C. H., Elements of the Theory of Computation (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [8] | P. Mendler, Inductive definition in type theory, Ph.D. Thesis, Cornell University, Ithaca, NY, 1988; P. Mendler, Inductive definition in type theory, Ph.D. Thesis, Cornell University, Ithaca, NY, 1988 |
| [9] | Robinson, J., A machine oriented logic based on the resolution principle, Journal of the Association of Computing Machinery, 12, 23-41 (1965) · Zbl 0139.12303 |
| [10] | J.L. Underwood, The tableau algorithm for intuitionistic propositional calculus as a constructive completeness proof, in: Proceedings of the Workshop on Theorem Proving with Analytic Tableaux, Marseille, France, 1993, pp. 245-248, Available as Technical Report MPI-I-93-213 Max-Planck-Institut für Informatik, Saarbrücken, Germany; J.L. Underwood, The tableau algorithm for intuitionistic propositional calculus as a constructive completeness proof, in: Proceedings of the Workshop on Theorem Proving with Analytic Tableaux, Marseille, France, 1993, pp. 245-248, Available as Technical Report MPI-I-93-213 Max-Planck-Institut für Informatik, Saarbrücken, Germany |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
