Reasoning with higher order partial functions

  • A. Gavilanes-Franco
  • F. Lucio-Carrasco
  • M. Rodríguez-Artalejo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 702)


In this paper we introduce the logic PHOL, which embodies higher-order functions through a simply-typed λ-calculus and deals with partial objects by using partially ordered domains and three truth values. We define a refutationally complete tableaux method for PHOL and we show how to derive a sound and complete cut free sequent calculus through a systematic analysis of the rules for tableaux construction.


Proof System Sequent Calculus Strong Model Open Branch Logical Axiom 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Arnold, M. Nivat. The metric space of infinite trees. Algebraic and topological properties. Ann. Soc. Math. Polon. Ser. IV Fund. Inform. 4, 445–476, 1980.Google Scholar
  2. 2.
    H. Barringer, J. H. Cheng, C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica 22, 251–269, 1984.Google Scholar
  3. 3.
    M. Broy, M. Wirsing. Partial Abstract Types. Acta Informatica 18, 47–64, 1982.Google Scholar
  4. 4.
    A. Church. A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68, 1940.Google Scholar
  5. 5.
    H.-D-Ebbinghaus. Über eine Prädikatenlogik mit partiell definierten Prädikaten und Funktionen. Arch. Math. Logik 12, 39–53, 1969.Google Scholar
  6. 6.
    H.-D. Ebbinghaus, J. Flum, W. Thomas. Mathematical Logic. Springer-Verlag, 1984.Google Scholar
  7. 7.
    W. M. Farmer. A partial function version of Church's simple theory of types. J. Symbolic Logic 55 (3), 1269–1291, 1990.Google Scholar
  8. 8.
    M. Fitting. A Kripke-Kleene semantics for logic programs. J. Logic Programming 2 (4), 295–312, 1985.Google Scholar
  9. 9.
    M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.Google Scholar
  10. 10.
    A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. Theoretical Computer Science 74, 37–69, 1990.Google Scholar
  11. 11.
    M. J. Gordon. HOL: a proof generating system for higher-order logic. In VLSI specification, verification, and synthesis. (G. Birtwistle, P. A. Subrahmanyam, eds.). Kluwer, Dordrecht, 73–128, 1987.Google Scholar
  12. 12.
    L. Henkin. Completeness in the theory of types. J. Symbolic Logic 15, 81–91, 1950.Google Scholar
  13. 13.
    M. Holden. Weak logic theory. Theoretical Computer Science 79, 295–321, 1991.Google Scholar
  14. 14.
    A. Hoogewijs. Partial-predicate logic in computer science. Acta Informatica 24, 281–293, 1987.Google Scholar
  15. 15.
    J. R. Hindley, J. P. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.Google Scholar
  16. 16.
    S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.Google Scholar
  17. 17.
    B. Krieg-Brückner et al. PROSPECTRA Project Summary. University of Bremen, 1985.Google Scholar
  18. 18.
    K. Kunen. Negation in logic programming. J. Logic Programming 4, 289–308, 1987.Google Scholar
  19. 19.
    B. Konikowska, A. Tarlecki and A. Blikle. A three-valued logic for software specification and validation.In Proc. VDM'88, VDM-The Way Ahead. LNCS 328, 218–242, 1988.Google Scholar
  20. 20.
    J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. 9 (4), 646–685, 1987.Google Scholar
  21. 21.
    J. McCarthy. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems. North-Holland, 33–70, 1963.Google Scholar
  22. 22.
    G. Nadathur, D. Miller. An overview of λ-prolog. Procs. ICLP'88. The MIT Press, 810–827, 1988.Google Scholar
  23. 23.
    B. Nordström, K. Peterson, J. M. Smith. Programming in Martin-Löf's Type Theory. Oxford Science Publications, 1990.Google Scholar
  24. 24.
    O. Owe. An approach to program reasoning based on a first-order logic for partial functions. Comp. Sc. Techn. Report No CS-081. Dep. Elect. Engien. and Comp. Sc., Univ. of California, 1984.Google Scholar
  25. 25.
    L. C. Paulson. Logic and computation. Interactive proof with Cambridge LCF. Cambridge University Press, 1987.Google Scholar
  26. 26.
    The PRL group (Constable et al.). Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986.Google Scholar
  27. 27.
    R. M. Smullyan. First-Order Logic. Springer, Berlin, 1968.Google Scholar
  28. 28.
    S. Thompson. A Logic for Miranda. Formal Aspects of Computing 1, 339–365, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • A. Gavilanes-Franco
    • 1
  • F. Lucio-Carrasco
    • 2
  • M. Rodríguez-Artalejo
    • 1
  1. 1.Dep. de Informática y Automática. Fac. de MatemáticasUniv. ComplutenseMadrid
  2. 2.Dep. de Lenguajes y Sistemas Informáticos. Fac. de InformáticaUniv. del PaísVasco. San Sebastián

Personalised recommendations