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
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).
|Main Tools: Graph Searching | Consistency for CSP | SLS for CSP | Deduction | Belief and Decision Networks | Decision Trees | Neural Networks | STRIPS to CSP|