The term resolution in logic refers to a mechanical method for proving statements in first-order logic. It is applied to two clauses in a sentence, and by unification, it eliminates a literal that occurs positive in one clause and negative in the other. A literal stated in the antecedent of an implication is negative because an implication is equivalent to . Therefore, in
we can unify with . This will give us
which is equivalent to
By distribution, we have
Since , we have
Through this resolution process, we proved . Resolution with backtracking is the basic control mechanism in Prolog.12.1
SLD resolution is a term used in logic programming to refer to the control strategy used in such languages to resolve issues of nondeterminism. By definition, SLD resolution is linear resolution with a selection function for definite sentences. A definite sentence has exactly one positive literal in each clause and this literal is selected to be resolved upon, i.e., replaced in the goal clause by the conjunction of negative literals which form the body of the clause.
SLD resolution in ALE is identical to what Prolog does. In fact, in implementation ALE relies on Prolog for SLD resolution. For more information on how Prolog handles nondeterminism, refer to chapter 5 of Sterling and Shapiro (1986).
ALE compiles a clause declaration into instructions, and processes these instructions as follows:
A few built-in operators merit considerationl. =@/2 is compiled to an equality check (using Prolog ==/2) on the Tags of the ALE data structure. =/2 is compiled to unification. when/2 is compiled as stated in Chapter 6. Prolog hooks are compiled directly to Prolog calls. Cut, shallow-cut and negation-by-failure are compiled to their Prolog equivalents.