Definite Clause Deduction |
Home | News | Older Versions | Downloads | Supported Platforms | People | Report a bug! |
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 pseudocode 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 substition 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 stackIf 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).