A Tableau Calculus for Partial Functions

Conference paper
Part of the Collegium Logicum book series (COLLLOGICUM, volume 2)


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.


Partial functions many-valued logic sorted logic tableau 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [And86]
    Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, 1986.Google Scholar
  2. [Bee85]
    Michael J. Beeson. Foundations of Constructive Mathematics. Springer Ver-lag, 1985.Google Scholar
  3. [Bet55]
    E. W. Beth. Semantic entailment and formal derivability. Medelingen von de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, 18 (13): 309–342, 1955.MathSciNetGoogle Scholar
  4. [BF92]
    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.Google Scholar
  5. [BFZ93]
    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.Google Scholar
  6. [Car87]
    Walter A. Carnielli. Systematization of finite many-valued logics through the method of tableaux. The Journal of Symbolic Logic, 52: 473–493, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  7. [Car91]
    Walter A. Carnielli. On sequents and tableaux for many-valued logics. Jour-nal of Non-Classical Logic, 8 (1): 59–76, 1991.zbMATHGoogle Scholar
  8. [Far90]
    William M. Farmer. A partial functions version of Church’s simple theory of types. The Journal of Symbolic Logic, 55 (3): 1269–1291, 1990.MathSciNetzbMATHCrossRefGoogle Scholar
  9. [FGT93]
    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.zbMATHCrossRefGoogle Scholar
  10. [Fit90]
    Melvin Fitting. First-Order Logic and Automated Theorem Proving. Sprin-ger Verlag, 1990.Google Scholar
  11. [Häh92]
    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.Google Scholar
  12. [Hin55]
    K. J. J. Hintikka. Form and content in quantification theory. Acta Philo-sophica Fennica, 8: 7–55, 1955.MathSciNetGoogle Scholar
  13. [HS94]
    Reiner Hähnle and Peter H. Schmitt The liberalized 6-rule in free variable tableaux. Journal of Automated Reasoning, 12 (2): 211–222, 1994.CrossRefGoogle Scholar
  14. [KK93]
    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.Google Scholar
  15. [KK94]
    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.Google Scholar
  16. [K1e52]
    Stephen C. Kleene. Introduction to Metamathematics. Van Nostrand, 1952.Google Scholar
  17. [LCGF89]
    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.Google Scholar
  18. [Pra60]
    Dag Prawitz. An improved proof procedure. Theoria, 26: 102–139, 1960.MathSciNetzbMATHCrossRefGoogle Scholar
  19. [Ree87]
    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.Google Scholar
  20. [Sch68]
    R. Schock. Logics without Existence Assumptions. Almquist & Wisell, 1968.Google Scholar
  21. [Sco70]
    Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, 1970.Google Scholar
  22. [Smu63]
    Raymond M. Smullyan. A unifying principle for quantification theory. Proc. Nat. Acad Sciences, 49: 828–832, 1963.CrossRefGoogle Scholar
  23. [Smu68]
    Raymond M. Smullyan. First-Order Logic. Springer Verlag, 1968.Google Scholar
  24. [SS89]
    Manfred Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations,Springer Verlag, LNAI 395, 1989.Google Scholar
  25. [Tic82]
    Pawel Tichy. Foundations of partial type theory. Reports on Mathematical Logic, 14: 59–72, 1982.MathSciNetzbMATHGoogle Scholar
  26. [Wei89]
    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.Google Scholar
  27. [Wei91]
    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.Google Scholar
  28. [Wei94]
    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.Google Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  1. 1.Fachbereich InformatikUniversität des SaarlandesSaarbrückenGermany

Personalised recommendations