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.
KeywordsFunction Symbol Unification Algorithm Phrase Structure Grammar Definite Clause Universal Graph
Unable to display preview. Download preview PDF.
- Gazdar, G., Klein, E., Pullum, G. and Sag, I. Generalized Phrase Structure Grammar. Basil Blackwell, Oxford, 1985.Google Scholar
- Pereira, F.C.N. Grammars and Logics of Partial Information. SRI Technical Note 420, Menlo Park, California, 1987.Google Scholar
- Shieber, S.M. An Introduction to Unification-Based Approaches to Grammar. CSLI Lecture Notes 4, Chicago University Press, 1986.Google Scholar
- 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