AIspace

Tutorials

Definite Clause Deduction

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.¹

Input:	Two Terms T₁ and T₂ to be unified
Output:	Theta, the mgu of T₁ and T₂, or failure
Algorithm:	Initialize the substitution Theta to be empty,
	the stack to contain the equation T₁ = T₂, and failure to false while stack not empty and no failure do pop X = Y from the stack case 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: continue X is f(X₁,...,X_n) and Y is f(Y₁,...,Y_n) for sume functor f and n > 0: push X_i = Y_i, i = 1...n, on the stack otherwise: 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.

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

Back to tutorials.