Abstract
We present an automated proof method for constructive logic based on Wallen's matrix characterization for intuitionistic validity. The proof search strategy extends Bibel's connection method for classical predicate logic. It generates a matrix proof which will then be transformed into a proof within a standard sequent calculus. Thus we can use an efficient proof method to guide the development of constructive proofs in interactive proof/program development systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. W. Beth. The foundations of mathematics. North-Holland, 1959.
W. Bibel, S. Brüning, U. Egly, T. Rath. Komet. In Proceedings of the 12th CADE, LNAI 814, pp. 783–787. Springer Verlag, 1994.
W. Bibel. On matrices with connections. Jour, of the ACM, 28, p. 633–645, 1981.
W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.
A. Bundy, F. van Harmelen, C. Horn, A. Smaill. The Oyster-Clam system. In Proceedings of the 10th CADE, LNCS 449, pp. 647–648. Springer Verlag, 1990.
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. North-Holland, 1969.
G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.
R. Letz, J. Schumann, S. Bayerl, W. Bibel Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.
H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis (SEKI Report SR-88-08), Universität Kaiserslautern, 1988.
J. Otten, C. Kreitz A connection based proof method for intuitionistic logic. In Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 122–137, Springer Verlag, 1995.
J. Otten, C. Kreitz T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. Report AIDA-95-09, FG Intellektik, TH Darmstadt, 1995.
J. Otten. Ein konnektionenorientiertes Beweisverfahren für intuitionistische Logik. Master's thesis, TH Darmstadt, 1995.
L. Paulson. Isabelle: The next 700 theorem provers. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pp. 361–386. Academic Press, 1990.
R. Pollack. The theory of LEGO — a proof checker for the extendend calculus of constructions. PhD thesis, University of Edinburgh, 1994.
S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standardsequent proofs. In Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 106–121, Springer, 1995.
S. Schmitt. Ein erweiterter intuitionistischer Sequenzenkalkül und dessen Anwendung im intuitionistischen Konnektionsbeweisen. Master's thesis, TH Darmstadt, 1994.
G. Takeuti. Proof Theory. North-Holland, 1975.
L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.
L. Wos et. al. Automated reasoning contributes to mathematics and logic. In Proceedings of the 10th CADE, LNCS 449, p. 485–499. Springer Verlag 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kreitz, C., Otten, J., Schmitt, S. (1996). Guiding program development systems by a connection based proof strategy. In: Proietti, M. (eds) Logic Program Synthesis and Transformation. LOPSTR 1995. Lecture Notes in Computer Science, vol 1048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60939-3_10
Download citation
DOI: https://doi.org/10.1007/3-540-60939-3_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60939-1
Online ISBN: 978-3-540-49745-5
eBook Packages: Springer Book Archive