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.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 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(X1,...,Xn) and Y is f(Y1,...,Yn) for sume functor f and n > 0: push Xi = Yi, 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.

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