Unification in lambda-calculi with if-then-else
A new unification algorithm is introduced, which (unlike previous algorithms for unification in λ-calculus) shares the pleasant properties of first-order unification. Proofs of these properties are given, in particular uniqueness of the answer and the most-general-unifier property. This unification algorithm can be used to generalize first-order proofsearch algorithms to second-order logic, making possible for example a straighforward treatment of McCarthy's circumscription schema.
KeywordsUnification Algorithm Reduction Rule Sequent Calculus Input Environment Automate Deduction
Unable to display preview. Download preview PDF.
- [Baker-Ginsberg 1989]A. Baker and M. Ginsberg. A theorem prover for prioritized circumscription. Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pp. 463–467, Morgan Kaufmann, Los Altos, Calif. (1989).Google Scholar
- [Barendregt 1981]H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1981).Google Scholar
- [Beeson 1991]M. Beeson. Some applications of Gentzen's proof theory in automated deduction. In Schroeder-Heister (ed.), Extensions of Logic Programming, Lecture Notes in Artificial Intelligence 475, Springer-Verlag, Berlin/Heidelberg/New York (1991).Google Scholar
- [Ginsberg 1989]M. Ginsberg. A circumscriptive theorem prover. Artificial Intelligence 39, No. 2 (1989).Google Scholar
- [Huet 1975]
- [Lifschitz 1985]V. Lifschitz. Computing circumscription. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pp. 121–127, Morgan Kaufmann, Los Altos, Calif. (1985).Google Scholar
- [McCarthy 1986]
- [Miller 1992]
- [Miller and Nadathur 1988]D. Miller and G. Nadathur. An Overview of λ-Prolog In Proceedings of the Fifth International Symposium on Logic Programming, Seattle, August 1988.Google Scholar
- [Prawitz 1967]D. Prawitz. Completeness and Hauptsatz for second order logic. Theoria 33, 246–258.Google Scholar
- [Synder 1990]W. Snyder. Higher-order E-unification. In M. E. Stickel (ed.), CADE-10, Tenth International Conference on Automated Deduction 573–587 Springer-Verlag (1990).Google Scholar
- [Wallen 1990]Automated Deduction in Nonclassical Logics. MIT Press, Cambridge, MA (1990)Google Scholar