Abstract
Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truth-functional, does not fit the framework directly. We solve this problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi.
This work was supported by the Deutsche Forschungsgemeinschaft (SFB 314, D2)
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, 1986.
Michael J. Beeson. Foundations of Constructive Mathematics. Springer Ver-lag, 1985.
E. W. Beth. Semantic entailment and formal derivability. Medelingen von de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, 18 (13): 309–342, 1955.
Matthias Baaz and Christian G. Fermüller. Resolution for many-valued logics. In A. Voronkov, editor, Proceedings of LPAR, pages 107–118, St. Petersburg, Russia, 1992. Springer Verlag, LNAI 624.
Matthias Baaz, Christian G. Fermüller, and Richard Zach. Dual systems of sequents and tableaux for many-valued logics. Technical Report TUWE185.2BFZ.2–92, Technische Universität Wien, 1993.
Walter A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. The Journal of Symbolic Logic, 52: 473–493, 1987.
Walter A. Carnielli. On sequents and tableaux for many-valued logics. Jour-nal of Non-Classical Logic, 8 (1): 59–76, 1991.
William M. Farmer. A partial functions version of Church’s simple theory of types. The Journal of Symbolic Logic, 55 (3): 1269–1291, 1990.
William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning, 11 (2): 213–248, October 1993.
Melvin Fitting. First-Order Logic and Automated Theorem Proving. Sprin-ger Verlag, 1990.
Reiner Hähnle. Automated Theorem Proving in Multiple Valued Logics. PhD thesis, Fachbereich Informatik, Universität Karlsruhe, Karlsruhe, Germany, March 1992. revised version: Automated Deduction in Multiple-Valued Logics, Oxford University Press, 1994.
K. J. J. Hintikka. Form and content in quantification theory. Acta Philo-sophica Fennica, 8: 7–55, 1955.
Reiner Hähnle and Peter H. Schmitt The liberalized 6-rule in free variable tableaux. Journal of Automated Reasoning, 12 (2): 211–222, 1994.
Manfred Kerber and Michael Kohlhase. A mechanization of strong Kleene logic for partial functions. SEKI Report SR-93–20, Fachbereich Informatik, Universität des Saarlandes, Im Stadtwald, Saarbrücken, Germany, 1993.
Manfred Kerber and Michael Kohlhase. A mechanization of strong Kleene logic for partial functions. In Alan Bundy, editor, Proceedings of the 12th CADE, pages 371–385, Nancy, France, 1994. Springer Verlag, LNAI 814.
Stephen C. Kleene. Introduction to Metamathematics. Van Nostrand, 1952.
Francisca Lucio-Carrrasco and Antonio Gavilanes-Franco. A first order logic for partial functions. In Proceedings STACS’89, pages 47–58. Springer Verlag, LNCS 349, 1989.
Dag Prawitz. An improved proof procedure. Theoria, 26: 102–139, 1960.
S. Reeves. Semantic tableaux as a framework for automated theorem-proving. In J. Hallam and C. Mellish, editors, Advances in Artificial Intelligence, AISB-87, pages 125–139. Wiley, 1987.
R. Schock. Logics without Existence Assumptions. Almquist & Wisell, 1968.
Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, 1970.
Raymond M. Smullyan. A unifying principle for quantification theory. Proc. Nat. Acad Sciences, 49: 828–832, 1963.
Raymond M. Smullyan. First-Order Logic. Springer Verlag, 1968.
Manfred Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations,Springer Verlag, LNAI 395, 1989.
Pawel Tichy. Foundations of partial type theory. Reports on Mathematical Logic, 14: 59–72, 1982.
Christoph Weidenbach. A resolution calculus with dynamic sort structures and partial functions. SEKI Report SR-89–23, Fachbereich Informatik, Universität Kaiserslautern, Kaiserslautern, Germany, 1989. Short version in ECAI’90, p. 688–693.
Christoph Weidenbach. A sorted logic using dynamic sorts. Technical Report MPI-I-91–218, Max-Planck-Institut für Informatik, Im Stadtwald, Saarbrücken, Germany, 1991. Short version in IJCAI’93, p. 60–65.
Christoph Weidenbach. First-order tableaux with sorts. In Krysia Broda and Marcello D’Agostino et al., editors, TABLEAUX-’94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 247–261. Imperial College of Science Technology and Medicine, TR-94/5, April 1994. To appear in the Bulletin of the IGPL.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer-Verlag/Wien
About this paper
Cite this paper
Kerber, M., Kohlhase, M. (1996). A Tableau Calculus for Partial Functions. In: Collegium Logicum. Collegium Logicum, vol 2. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9461-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-7091-9461-4_2
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82796-3
Online ISBN: 978-3-7091-9461-4
eBook Packages: Springer Book Archive