• Alan Bundy
Part of the Symbolic Computation book series (SYMBOLIC)


A process, used in resolution <204>, for determining whether two expressions of the predicate calculus <180> will match. Terms of an expression in predicate calculus may be of one of three forms: constant, variable or function, where the last of these is made up of a function symbol applied to a number of terms. A substitution is a set of ordered pairs where the first element of each pair is a term and the second a variable. Applying such a substitution to a formula means that each variable appearing in the set of ordered pairs is replaced by the term which it is matched with in the substitution. Two expressions are unifiable if there is a substitution (the unifier) which when applied to both expressions makes them identical. A unification algorithm determines whether the given expressions are unifiable and, if so, finds a unifying substitution. It is usual in resolution based systems to specify that the substitution which is applied to unify two expressions is the most general such substitution, thus the expressions lose as little generality as is necessary to make the resolution go through.


Function Symbol Unification Algorithm Phrase Structure Grammar Definite Clause Universal Graph 
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. Nilsson, N.J. Principles of Artificial Intelligence, Tioga Pub. Co., Palo Alto, California, 1980.MATHGoogle Scholar
  2. Gazdar, G., Klein, E., Pullum, G. and Sag, I. Generalized Phrase Structure Grammar. Basil Blackwell, Oxford, 1985.Google Scholar
  3. Pereira, F.C.N. Grammars and Logics of Partial Information. SRI Technical Note 420, Menlo Park, California, 1987.Google Scholar
  4. Shieber, S.M. An Introduction to Unification-Based Approaches to Grammar. CSLI Lecture Notes 4, Chicago University Press, 1986.Google Scholar
  5. Levinson, R.A. Self-organising retrieval system for graphs. In Proceedings of the AAAI, pages 203–206. American Association for Artificial Intelligence, 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Alan Bundy
    • 1
  1. 1.Department of Artificial IntelligenceUniversity of EdinburghEdinburghScotland, UK

Personalised recommendations