Abstract
The introduction of sorts to first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing search spaces. This suggests that sort information can be employed in higher-order theorem proving with similar results. This paper develops a sorted λ-calculus suitable for automatic theorem proving applications. It extends the simply typed λ-calculus by a higher-order sort concept that includes term declarations and functional base sorts. The term declaration mechanism studied here is powerful enough to subsume subsorting as a derived notion and therefore gives a justification for the special form of subsort inference. We present a set of transformations for sorted (pre-) unification and prove the nondeterministic completeness of the algorithm induced by these transformations.
This work was supported by the Deutsche Forschungsgemeinschaft in SFB 314 (D2)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.
Peter B. Andrews, Eve Longini-Cohen, Dale Miller, and Frank Pfenning. Automating higher order logics. Contemp. Math, 29:169–192, 1984.
Kim B. Bruce and Giuseppe Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87:196–240, 1990.
Luca Cardelli. A semantics of multiple inheritance. In G. Kahn and G. Plotkin D.G. MacQueen, editors. Semantics of Data Types, volume 173 of LNCS. Springer Verlag, 1984.
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
A. G. Cohn. Taxonomic reasoning with many-sorted logics. Artificial Intelligence Review, 3:89–128, 1989.
Gérard P. Huet. Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University, 1972.
Patricia Johann and Michael Kohlhase. Unification in an extensional lambda calculus with ordered function sorts and constant overloading. SEKI-Report SR-93-14, Universität des Saarlandes, 1993.
Patricia Johann and Michael Kohlhase. Unification in an extensional lambda calculus with ordered function sorts and constant overloading. In Proc. CADE'94, LNCS,Springer Verlag, 1994.
Manfred Kerber and Michael Kohlhase. A mechanization of strong Kleene logic for partial functions. In Proc. CADE'94, LNCS Springer Verlag, 1994.
Michael Kohlhase. Unification in order-sorted type theory. In Proc. LPAR'92, pages 421–432, volume 624 of LNAI. Springer Verlag, 1992.
Michael Kohlhase. Automated Deduction in Order-Sorted Type Theory. PhD thesis, Universität des Saarlandes, 1994. to appear.
Michael Kohlhase. Higher-order order-sorted resolution. Seki Report SR-94-01, FB Informatik, Universität des Saarlandes, 1994.
Michael Kohlhase and Frank Pfenning. Unification in a λ-calculus with intersection types. In Proc. ILPS'93, pages 488–505. MIT Press, 1993.
Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321–358, 1992.
Tobias Nipkow and Zhenyu Qian. Reduction and unification in lambda calculi with subtypes. In Proc. CADE'92 volume 607 of LNCS, pages 66–78, 1992. Springer Verlag.
Benjamin C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, 1991.
Zhenyu Qian. Extensions of Order-Sorted Algebraic Specifications: Parameterization, Higher-Functions and Polymorphism. PhD thesis, Universität Bremen, 1991.
Manfred Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations, volume 395 of LNAI. Springer Verlag, 1989.
Wayne Snyder. A Proof Theory for General Unification. Birkhäuser, 1991.
Christoph Walther. A Many-Sorted Calculus Based on Resolution and Paramodulation. Pitman, London. Morgan Kaufman Publishers, Inc, 1987.
C. Weidenbach. Unification in sort theories and its applications. MPI-Report MPI-I-93-211, MPI Informatik, Saarbrücken, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kohlhase, M. (1994). Unification in a sorted λ-calculus with term declarations and function sorts. In: Nebel, B., Dreschler-Fischer, L. (eds) KI-94: Advances in Artificial Intelligence. KI 1994. Lecture Notes in Computer Science, vol 861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58467-6_29
Download citation
DOI: https://doi.org/10.1007/3-540-58467-6_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58467-4
Online ISBN: 978-3-540-48979-5
eBook Packages: Springer Book Archive