Catalogue of Artificial Intelligence Techniques
Keywords: resolution, substitution, terms
Categories: Theorem Proving
Author(s): Dave Plummer
A process, used in Resolution, for determining whether two expressions of the Predicate Calculus 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, known as the `most general unifier'. Thus the expressions lose as little generality as is necessary to make the resolution go through.
- Nilsson, N.J., Principles of Artificial Intelligence
, Tioga Pub. Co., Palo Alto, California, 1980.