ABSTRACT
A logic language such as Prolog obtains its results by backward chaining through a series of relations in a database of clauses until a unification is achieved. Bindings occur through the unification of the goal with database clauses, but each binding may be undone through backtracking to allow subsequent attempts at unification. Prolog keeps track of all the substitutions made in reaching a certain point, so at unification it can report the full set. At this point, the goal is said to be satisfied. The Prolog search mechanism does not and could not substitute terms in the relations themselves because it is an animated form of logic without equality. Instead it keeps track of the substitutions in a separate list. Functional languages, on the other hand, admit the concept of denotational equality and compute a result by rewriting terms until the simplest possible result is obtained. Clearly there is no backtracking in a functional language.
