Skip to main content
SpringerLink
Log in

Reasoning with higher order partial functions

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 702))

Included in the following conference series:

  • 137 Accesses

Abstract

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.

Research partially supported by the PRONTIC Project TIC 89/0104 and the ESPRIT BR Working Group nb. 6028 CCL.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. H. Barringer, J. H. Cheng, C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica 22, 251–269, 1984.

    Google Scholar 

  3. M. Broy, M. Wirsing. Partial Abstract Types. Acta Informatica 18, 47–64, 1982.

    Google Scholar 

  4. A. Church. A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68, 1940.

    Google Scholar 

  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. H.-D. Ebbinghaus, J. Flum, W. Thomas. Mathematical Logic. Springer-Verlag, 1984.

    Google Scholar 

  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. M. Fitting. A Kripke-Kleene semantics for logic programs. J. Logic Programming 2 (4), 295–312, 1985.

    Google Scholar 

  9. M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.

    Google Scholar 

  10. A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. Theoretical Computer Science 74, 37–69, 1990.

    Google Scholar 

  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. L. Henkin. Completeness in the theory of types. J. Symbolic Logic 15, 81–91, 1950.

    Google Scholar 

  13. M. Holden. Weak logic theory. Theoretical Computer Science 79, 295–321, 1991.

    Google Scholar 

  14. A. Hoogewijs. Partial-predicate logic in computer science. Acta Informatica 24, 281–293, 1987.

    Google Scholar 

  15. J. R. Hindley, J. P. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.

    Google Scholar 

  16. S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.

    Google Scholar 

  17. B. Krieg-Brückner et al. PROSPECTRA Project Summary. University of Bremen, 1985.

    Google Scholar 

  18. K. Kunen. Negation in logic programming. J. Logic Programming 4, 289–308, 1987.

    Google Scholar 

  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. J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. 9 (4), 646–685, 1987.

    Google Scholar 

  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. G. Nadathur, D. Miller. An overview of λ-prolog. Procs. ICLP'88. The MIT Press, 810–827, 1988.

    Google Scholar 

  23. B. Nordström, K. Peterson, J. M. Smith. Programming in Martin-Löf's Type Theory. Oxford Science Publications, 1990.

    Google Scholar 

  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. L. C. Paulson. Logic and computation. Interactive proof with Cambridge LCF. Cambridge University Press, 1987.

    Google Scholar 

  26. The PRL group (Constable et al.). Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986.

    Google Scholar 

  27. R. M. Smullyan. First-Order Logic. Springer, Berlin, 1968.

    Google Scholar 

  28. S. Thompson. A Logic for Miranda. Formal Aspects of Computing 1, 339–365, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dep. de Informática y Automática. Fac. de Matemáticas, Univ. Complutense, Madrid

    A. Gavilanes-Franco & M. Rodríguez-Artalejo

  2. Dep. de Lenguajes y Sistemas Informáticos. Fac. de Informática, Univ. del País, Vasco. San Sebastián

    F. Lucio-Carrasco

Authors
  1. A. Gavilanes-Franco
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. F. Lucio-Carrasco
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. M. Rodríguez-Artalejo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

E. Börger G. Jäger H. Kleine Büning S. Martini M. M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gavilanes-Franco, A., Lucio-Carrasco, F., Rodríguez-Artalejo, M. (1993). Reasoning with higher order partial functions. In: Börger, E., Jäger, G., Kleine Büning, H., Martini, S., Richter, M.M. (eds) Computer Science Logic. CSL 1992. Lecture Notes in Computer Science, vol 702. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56992-8_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-56992-8_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56992-3

  • Online ISBN: 978-3-540-47890-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation