Abstract
We present a procedure transforming intuitionistic matrix proofs into proofs within the intuitionistic standard sequent calculus. The transformation is based on L. Wallen's proof justifying his matrix characterization for the validity of intuitionistic formulae. Since this proof makes use of Fitting's non-standard sequent calculus our procedure consists of two steps. First a non-standard sequent proof will be extracted from a given matrix proof. Secondly we transform each non-standard proof into a standard proof in a structure preserving way. To simplify the latter step we introduce an extended standard calculus which is shown to be sound and complete.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. Bibel. On matrices with connections. Jour. of the ACM, 28, p. 633–645, 1981.
W. Bibel. Automated Theorem Proving. Vieweg Verlag 1987.
W. Bibel, S. Brüning, U. Egly, and T. Rath. Komet. In Proceedings of the Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 814, pages 783–787. Springer Verlag, 1994.
R. L. Constable et al. Implementing Mathematics with the NuPRL proof development system. Prentice Hall,1986.
M. C. Fitting. Intuitionistic logic, model theory and forcing. Studies in logic and the foundations of mathematics. North-Holland, 1969.
J. Gallier. Constructive logics. Part I: A tutorial on proof systems and typed λ-calculi. Technical Report 8, Digital Equipment Corporation, 1991.
I. Gassmann. Eine Matrix-basierte Beweisprozedur für intuitionistische Logik. Master's thesis, TH Darmstadt, FG Intellektik, 1994.
G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.
R. Letz, J. Schumann, S. Bayerl, and W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.
J. Otten and C. Kreitz. A connection based proof method for intuitionistic logic. In Proceedings Tableaux Workshop 1995, this volume.
S. Schmitt. Ein erweiterter intuitionistischer Sequenzenkalkül und dessen Anwendung im intuitionistischen Konnektionsbeweisen. Master's thesis, TH Darmstadt, FG Intellektik, 1994.
K. Schütte. Vollständige Systeme modaler und intuitionistischer Logik. Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer Verlag, 1968.
R. M. Smullyan. A generalization of intuitionistic and modal logics. In H. Leblanc, ed., Truth, Syntax and Modality, pages 274–293. North-Holland, 1973.
G. Takeuti. Proof Theory. North-Holland, 1975.
L. A. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.
L. Wos et. al. Automated reasoning contributes to mathematics and logic. In M. E. Stickel, editor, Proceedings of the 10 th Conference on Automated Deduction, Lecture Notes in Computer Science 449, pages 485–499. Springer Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmitt, S., Kreitz, C. (1995). On transforming intuitionistic matrix proofs into standard-sequent proofs. In: Baumgartner, P., Hähnle, R., Possega, J. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1995. Lecture Notes in Computer Science, vol 918. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59338-1_31
Download citation
DOI: https://doi.org/10.1007/3-540-59338-1_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59338-6
Online ISBN: 978-3-540-49235-1
eBook Packages: Springer Book Archive