Abstract
We present a technique that efficiently translates prepositional intuitionistic formulas into propositional classical formulas. This technique allows the use of arbitrary classical theorem provers for deciding the intuitionistic validity of a given propositional formula. The translation is based on the constructive description of a finite counter-model for any intuitionistic non-theorem. This enables us to replace universal quantification over all accessible worlds by a conjunction over the constructed finite set of these worlds within the encoding of a refuting Kripke-frame. This way, no additional theory handling by the theorem prover is required.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Dyckhoff: Contraction-Free Sequent Calculi for Intuitionistic Logic, Journal of Symbolic Logic, Vol. 57, No. 3, pp. 795–807, 1992
R. Dyckhoff, L. Pinto: Loop-free construction of counter-models for intuitionistic propositional logic, In Behara, Fritsch, Lintz (eds.): Symposia Gaussiana, Conf. A, pp. 225–232, de Gruyter, 1995
M. Fitting: Intuitionistic Logic Model Theory and Forcing, Amsterdam, 11969
A. Heuerding, e. a.: Propositional Logics on the Computer, Proceedings of the 4th TABLEAUX '95, LNAI 918, pp. 310–323, 1995
J. Hudelmaier: An O(nlogn)-space decision procedure for intuitionistic propositional logic, In: Journal of Logic and Computation 3(1)1, pp. 63–75, 1993
D. Korn, C. Kreitz.: A Constructively Adequate Refutation System for Intuitionistic Logic, Tech. Rep. AIDA-96-14, TH Darmstadt, 1996.
D. Korn, C. Kreitz: Efficiently Deciding Intuitionistic Propositional Logic via Translation into Classical Logic., Tech. Rep. AIDA-96-10, TH Darmstadt, 1996.
P. Miglioli, U. Moscato, M. Ornaghi: An Improved Refutation System for Intuitionistic Predicate Logic, Journal of Automated Reasoning 13, pp 361–373, 1994
Robert C. Moore: Reasoning about Knowledge and Action, Proceedings of the IJCAI-77, pp 223–227, Stanford, California 94305, 1977
H. J. Ohlbach: Semantics-Based Translation Methods for Modal Logics, Journal of Logic and Computation, Vol. 1, no. 6, pp 691–746, 1991
J. Otten, C. Kreitz: A Connection Based Proof Method for Intuitionistic Logic, Proceedings of the 4th TABLEAUX '95, LNAI 918, pp. 122–137, 1995
J. Otten: On the Advantage of a Non-Clausal Davis-Putnam Procedure, Tech. Rep. AIDA-97-1, TH Darmstadt, 1997
F. J. Pelletier: Seventy-Five Problems for Testing Automatic Theorem Provers, Journal of Automated Reasoning 2, pp 191–216, 1986
D. Sahlin, T. Franzén, S. Haridi: An Intuitionistic Predicate logic Theorem Prover, Journal of Logic and Computation, Vol. 2, no. 5, pp 619–656, 1992
R. B. Scherl: A Constraint Logic Approach to Automated Modal Deduction, Report UIUCDCS-R-93-1803, University of Illinois at Urbana-Champaign, 1993
K. Schütte: Vollständige Systeme modaler und intuitionistischer Logik, Springer, 1968
J. van Benthem: Correspondence Theory, In: D. Gabbay and F. Guenther (eds.): Handbook of Philosophical logic, Vol. II, pp. 167–247, Reidel, 11984
L. Wallen: Automated Proof Search in Non-Classical Logics, MIT Press, 11990
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korn, D.S., Kreitz, C. (1997). Deciding intuitionistic propositional logic via translation into classical logic. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_15
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive