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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
H. Barringer, J. H. Cheng, C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica 22, 251–269, 1984.
M. Broy, M. Wirsing. Partial Abstract Types. Acta Informatica 18, 47–64, 1982.
A. Church. A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68, 1940.
H.-D-Ebbinghaus. Über eine Prädikatenlogik mit partiell definierten Prädikaten und Funktionen. Arch. Math. Logik 12, 39–53, 1969.
H.-D. Ebbinghaus, J. Flum, W. Thomas. Mathematical Logic. Springer-Verlag, 1984.
W. M. Farmer. A partial function version of Church's simple theory of types. J. Symbolic Logic 55 (3), 1269–1291, 1990.
M. Fitting. A Kripke-Kleene semantics for logic programs. J. Logic Programming 2 (4), 295–312, 1985.
M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.
A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. Theoretical Computer Science 74, 37–69, 1990.
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.
L. Henkin. Completeness in the theory of types. J. Symbolic Logic 15, 81–91, 1950.
M. Holden. Weak logic theory. Theoretical Computer Science 79, 295–321, 1991.
A. Hoogewijs. Partial-predicate logic in computer science. Acta Informatica 24, 281–293, 1987.
J. R. Hindley, J. P. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.
S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.
B. Krieg-Brückner et al. PROSPECTRA Project Summary. University of Bremen, 1985.
K. Kunen. Negation in logic programming. J. Logic Programming 4, 289–308, 1987.
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.
J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. 9 (4), 646–685, 1987.
J. McCarthy. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems. North-Holland, 33–70, 1963.
G. Nadathur, D. Miller. An overview of λ-prolog. Procs. ICLP'88. The MIT Press, 810–827, 1988.
B. Nordström, K. Peterson, J. M. Smith. Programming in Martin-Löf's Type Theory. Oxford Science Publications, 1990.
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.
L. C. Paulson. Logic and computation. Interactive proof with Cambridge LCF. Cambridge University Press, 1987.
The PRL group (Constable et al.). Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986.
R. M. Smullyan. First-Order Logic. Springer, Berlin, 1968.
S. Thompson. A Logic for Miranda. Formal Aspects of Computing 1, 339–365, 1989.
Author information
Authors and Affiliations
Editor information
Rights 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