First order logic - SLD algorithm

Question

When we apply SLD algorithm we start with a definite program P and a goal clause. Must the goal clause initially be a single atom ? And why ?

Answer 1

Not necessarily.

The SLD-refutation algorithm is based on the resolution rule, with specific symbolism: it uses Horn clauses, and specific strategies for computational efficiency.

The "basic form" of resolution rule is simply modus ponens:

$\dfrac { p \to q \quad p } { q }$

written in the equivalent form:

$\dfrac { \lnot p \lor q \quad p } { q }.$

We may immediatley generalize it to:

$\dfrac { \lnot p \lor q \quad p \lor r } { q \lor r }$

and then generalize it again to clauses with a finite number of literals.