Abstract
We present a uniform algorithm fot transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. Making use of a similarity between matrix methods and Fitting's prefixed tableaus we first develop a procedure for extracting a prefixed sequent proof from a given matrix proof. By considering the additional restrictions on the order of rule applications we then extend this procedure into an algorithm which generates a conventional sequent proof.
Our algorithm is based on unified representations of matrix characterizations for various logics as well as of prefixed and usual sequent calculi. The peculiarities of a logic are encoded by certain parameters which are summarized in tables to be consulted by the algorithm.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E. W. Beth. The foundations of mathematics. North-Holland, 1959.
W. Bibel, S. Brüning, U. Egly, T. Rath. Komet. In CADE-12, LNAI 814, pp. 783–787. Springer, 1994.
W. Bibel. On matrices with connections. J. of the ACM, 28:633–645, 1981.
W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.
B. I. Dahn, J. Gehne, Th. Honigmann, L. Walther, A. Wolf. Integrating Logical Functions with ILF; Preprint 94-10, Humboldt University Berlin, 1994.
M. C. Fitting. Intuitionistic logic, model theory and forcing. Studies in logic and the foundations of mathematics. North-Holland, 1969.
M. C. Fitting. Proof Methods for Modal and Intuitionistic Logic. D. Reidel, 1983.
R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.
C. Lingenfelder. Structuring computer generated proofs. IJCAI-89, 1989.
C. Lingenfelder. Transformation and Structuring of Computer Generated Proofs. PhD thesis, Universität Kaiserslautern, 1990.
H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis, Universität Kaiserslautern, 1988.
J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. TABLEAUX-95, LNAI 918, pp. 122–137, Springer, 1995.
J. Otten, C. Kreitz. A Uniform Proof Procedure for Classical and Non-Classical Logics Technical Report, TH Darmstadt, 1996.
J. A. Robinson. A machine-oriented logic based on the resolution principle. J. of the ACM, 12(1):23–41, 1965.
S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standardsequent proofs. TABLEAUX-95, LNAI 918, pp. 106–121, Springer, 1995.
S. Schmitt. Ein erweiterter intuitionistischer Sequenzenkalkül und dessen Anwendung im intuitionistischen Konnektionsbeweisen. TH Darmstadt, 1994.
L. Wallen. Matrix proof methods for modal logics. IJCAI-87, p. 917–923. 1987.
L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.
L. Wos Et. Al. Automated reasoning contributes to mathematics and logic. CADE-10, LNCS 449, p. 485–499. Springer 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmitt, S., Kreitz, C. (1996). Converting non-classical matrix proofs into sequent-style systems. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_104
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_104
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive