SLD Resolution

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 $P\to Q$ is equivalent to $\neg P \vee Q$. Therefore, in

we can unify $socrates$ with $X$. This will give us

which is equivalent to

By distribution, we have

Since $P\wedge \neg P = false$, we have

Through this resolution process, we proved $mortal(socrates)$. 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:

• Enforce the descriptions on the head arguments, in left-to-right order.
• Enforce the descriptions on the arguments of the first body goal, in left-to-right order.
• Call the first body goal.
• Repeat the last two steps on all remaining body goals.

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.