A first-order logic for partial recursive functions

  • Antonio Gavilanes-Franco
Part of the Lecture Notes in Computer Science book series (LNCS, volume 452)


This paper is an extension of the first-order logic for partial functions [GL 89a] [GL 89b] to a logic of programs in the framework of a first order λμ-calculus. We define a typed functional language coupled to a logic with a definedness operator and a three-boolean valued semantics with an associated consequence relation. We study the proof theory of our logic through a tableaux method and show how to obtain complete sequent calculi for reasoning about partial recursive functions.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Apt 81]
    Ten years of Hoare's logic: a survey — Part I. K. R. Apt. ACM Trans. Prog. Lang. Syst. 3, 431–483, 1981.Google Scholar
  2. [BCJ 84]
    A logic covering undefinedness in program proofs. H. Barringer, J. H. Cheng, C. B. Jones. Acta Informatica 21, 251–269, 1984.Google Scholar
  3. [Bla 86]
    Partial logic. S. Blamey. Handbook of Philosophical Logic, Vol. III, 1–70, D. Reidel Publishing Company, 1986.Google Scholar
  4. [Bur 86]
    A model theoretic oriented approach to partial algebras. P. Burmeister. Part I. Akademie Verlag, Berlin, 1986.Google Scholar
  5. [BW 82]
    Partial abstract types. M. Broy, M. Wirsing. Acta Informatica 18, 47–64, 1982.Google Scholar
  6. [Del 88]
    Programmation en logique trivaluée. J. P. Delahaye. European Workshop on Logical Method in Artificial Intelligence, JELIA 88, 1988.Google Scholar
  7. [Fit 86]
    Partial models and logic programming. M. Fitting. Theoretical Computer Science 48, 229–255, 1986.Google Scholar
  8. [Gav 89a]
    Una lógica trivalorada para functiones recursivas parciales. A. Gavilanes. Thesis. Madrid, 1989.Google Scholar
  9. [Gav 89b]
    A first-order logic for partial recursive functions. A. Gavilanes. Technical Report DIA 89/2, FEB/89. Univ. Comp. Madrid, 1989.Google Scholar
  10. [GHR 89]
    Standard versus nonstandard semantics in logics for functional programs. A. Gil-Luezas, T. Hortalá-González, M. Rodríguez-Artalejo. Technical Report DIA 89/7, AUG/89. Univ. Comp. Madrid, 1989.Google Scholar
  11. [GL 89a]
    A first order logic for partial functions. A. Gavilanes, F. Lucio. To appear in Theoretical Computer Science.Google Scholar
  12. [GL 89b]
    A first order logic for partial functions. A. Gavilanes, F. Lucio. STACS'89. Proceedings. Lecture Notes in Computer Science 349, 47–58, 1989.Google Scholar
  13. [Goe 86]
    Ein Hoare kalkül für die sprache der getypten lambda-terme. Korrektheit, vollständigkeit, anwendungen. A. Goerdt. Thesis, 1986.Google Scholar
  14. [Goe 87]
    Hoare logic for lambda-terms as basis of Hoare logic for imperative languages. A. Goerdt. IEEE, 293–299, 1987.Google Scholar
  15. [Hoo 87]
    Partial-predicate logic in computer science. A. Hoogewijs. Acta Informatica 24, 281–293, 1987.Google Scholar
  16. [KTB 88]
    A three-valued logic for software specification and validation. B. Konikowska, A. Tarlecki, A. Blikle. VDM'88. Proceedings. Lecture Notes in Computer Science 328, 218–242, 1988.Google Scholar
  17. [KU 89]
    ALGOL-like languages with higher-order procedures and their expressive power. A. J. Kfoury, P. Urzyczyn. Logic at Botik'89. Proceedings. Lecture Notes in Computer Science 363, 186–199, 1989.Google Scholar
  18. [Loe 87]
    Algorithmic specifications: a constructive specification method for abstract data types. J. Loeckx. ACM Trans. on Prog. Lang., vol. 9, n. 4, 646–685, 1987.Google Scholar
  19. [Man 74]
    Mathematical theory of computation. Z. Manna. McGraw Hill, 1974.Google Scholar
  20. [Rei 87]
    Initial Computability, Algebraic Specifications, and Partial Algebras. H. Reichel. Oxford Science Publications, 1987.Google Scholar
  21. [Sco 70]
    Outline of a mathematical theory of computation technical monograph PRG-2. D. S. Scott. Oxford University Computing Laboratory, 1970.Google Scholar
  22. [Sco 82]
    Domains for denotational semantics. D. S. Scott. ICALP'82, Aarhus, Denmark, 1982.Google Scholar
  23. [Smu 68]
    First-order logic. R. M. Smullyan. Springer-Verlag, 1968.Google Scholar
  24. [Sto 77]
    Denotational semantics: The Scott-Strachey approach to programming language theory. J. Stoy. MIT Press, 1977.Google Scholar
  25. [Ten 76]
    The denotational semantics of programming languages. R. D. Tennent. Comm. ACM 19 (8), 437–453, 1976.Google Scholar
  26. [THM 83]
    From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview. B. A. Trakhtenbrot, J. Y. Halpern, A. R. Meyer. Logics of Programs. Proceedings. Lecture Notes in Computer Science 164, 474–500, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Antonio Gavilanes-Franco
    • 1
  1. 1.Departamento de Informática y Automática Facultad de MatemáticasUniversidad ComplutenseMadridSpain

Personalised recommendations