Unification in lambda-calculi with if-then-else

  • Michael Beeson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


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.


Unification Algorithm Reduction Rule Sequent Calculus Input Environment Automate Deduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [Barendregt 1981]
    H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1981).Google Scholar
  3. [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
  4. [Ginsberg 1989]
    M. Ginsberg. A circumscriptive theorem prover. Artificial Intelligence 39, No. 2 (1989).Google Scholar
  5. [Huet 1975]
    G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science 1 (1975) 27–52.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [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
  7. [McCarthy 1986]
    J. McCarthy. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence 28 (1986) 89–116.CrossRefMathSciNetGoogle Scholar
  8. [Miller 1992]
    D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation 14 (1992) 321–358.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [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
  10. [Prawitz 1967]
    D. Prawitz. Completeness and Hauptsatz for second order logic. Theoria 33, 246–258.Google Scholar
  11. [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
  12. [Wallen 1990]
    Automated Deduction in Nonclassical Logics. MIT Press, Cambridge, MA (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Michael Beeson
    • 1
  1. 1.Department of Mathematics and Computer ScienceSan Jose State UniversitySan JoseUSA

Personalised recommendations