Abstract
This paper presents a formalization of a sequent presentation of intuitionisitic propositional logic and proof of decidability. The proof is implemented in the Nuprl system and the resulting proof object yields a “correct-by-construction” program for deciding intuitionisitc propositional sequents. The extracted program turns out to be an implementation of the tableau algorithm. If the argument to the resulting decision procedure is a valid sequent, a formal proof of that fact is returned, otherwise a counter-example in the form of a Kripke Countermodel is returned. The formalization roughly follows Aitken, Constable and Underwood’s presentation in [1] but a number of adjustments and corrections have been made to ensure the extracted program is clean (no non-computational junk) and efficient.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
William Aitken, Robert Constable, and Judith Underwood. Metalogical frame works II: Using reflected decision procedures. Unpublished Manuscript.
Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The semantics of reflected proof. In Proceedings of the Fifth Symposium on Logic in Computer Science, pages 95–197. IEEE, June 1990.
E. W. Beth. The Foundations of Mathematics. North-Holland, 1959.
J. L. Caldwell. Classical propositional decidability via Nuprl proof extraction. In Jim Grundy and Malcolm Newey, editors, Theorem Proving In Higer Order Logics, volume 1479 of Lecture Notes in Computer Science, 1998.
James Caldwell. Moving proofs-as-programs into practice. In Proceedings, 12th IEEE International Conference Automated Software Engineering, pages 10–17. IEEE Computer Society, 1997.
James Caldwell. Decidability Extracted: Synthesizing “Correct-by-Construction” Decision Procedures from Constructive Proofs. PhD thesis, Cornell University, Ithaca, NY, August 1998.
Robert L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
A._G. Dragalin. Mathematical Intuitionism: Introduction to Proof Theory, volume 67 of Translations of Mathematical Monographs. American Mathematical Society, 1987.
Michael Dummett. Elements of Intuitionism. Oxford Logic Series. Clarendon Press, 1977.
U. Egly and S. Schmitt. Intuitionistic proof transformations and their application to constructive program synthesis. In J. Calmet and J. Plaza, editors, Proceedings of the 4 th International Conference on Artificial Intelligence and Symbolic Computation (AISC’98), number 1476 in Lecture Notes in Artificial Intelligence, pages 132–144. Springer Verlag, Berlin, Heidelberg, New-York, 1998.
Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library. D. Reidel, 1983.
Susumu Hayashi and Hiroshi Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988.
J. Hudelmaier. A note on Kripkean countermodels for intuitionistically unprovable sequents. In W. Bibel, U. Furbach, R. Hasegawa, and M. Stickel, editors, Seminar on Deduction, February 1997. Dagstuhl report 9709.
C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15(5–6):607–640, 1993.
L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana, pages 225–232, Berlin, New York, 1995. Walter de Gruyter and Co.
N. Shankar. Towards mechanical metamathematics. J. Automated Reasoning, 1(4):407–434, 1985.
C. A. Smorynski. Applications of Kripke models. In A. Troelstra, editor, Metamathematical Investigation of Intuitionistic Mathematics, volume 344 of Lecture Notes in Mathematics, pages 324–391. Springer-Verlag, 1973.
J. Underwood. Aspects of the Computational Content of Proofs. PhD thesis, Cornell University, 1994.
Judith 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, pages 245–248, 1993.
Judith Underwood. Tableau for intuitionistic predicate logic as metatheory. In Peter Baumgartner, Reiner Hahnle, and Joachim Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, volume 918 of Lecture Notes in Artificial Intelligence. Springer, 1995.
K. Weich. Decision procedures for intuitionistic propositional logic by program extraction.
K. Weich. Private communication. February 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caldwell, J. (1999). Intuitionisitic Tableau Extracted. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_11
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive