Definite Clause Deduction

Back to tutorials.

Tutorial Four (Supplementary): The Algorithms

The previous tutorial discussed the search strategies used in searching for a solution to a query. However, at the very centre of it all is the unification algorithm for terms. For a clause to be successfully applied, its head must be successfully unified with the atom. Unification is an essentially recursive procedure that will be described in this tutorial. For two goals to unify, they must have the same predicate (in name as well as arity), and their terms must unify. The following is pseudo-code for a unification algorithm for terms.1

Input: Two Terms T1 and T2 to be unified
Output: Theta, the mgu of T1 and T2, or failure
Algorithm: Initialize the substitution Theta to be empty,
the stack to contain the equation T1 = T2,
and failure to false

while stack not empty and no failure do

pop X = Y from the stack

X is a variable that does not occur in Y:
substitute Y for X in the stack and in Theta, add X = Y to Theta.

Y is a variable that does not occur in X:
substitute X for Y in the stack and in Theta, add Y = X to Theta.

X and Y are identical constants or variables:
X is f(X1,...,Xn) and Y is f(Y1,...,Yn) for sume functor f and n > 0:
push Xi = Yi, i = 1...n, on the stack
failure is true
If failure, then output failure else output Theta.

The check in the first two cases that Y does not occur in X before substituting X for Y, is called the occurs check. The applet offers the option to turn it off and on. Without the occurs check, soundness is sacrificed but efficiency is increased. The occurs check option in the deduction applet is found under the 'Search Options' menu.

1Leon Sterling and Ehud Shapiro, The Art of Prolog, (Cambridge: MIT Press, 1994).

Back to tutorials.

Valid HTML 4.0 Transitional