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 ?

Thanks Mauro. The thing i dont understand is that , in many definitions ( for example the one for "Close World Assumptions" and "Negation as Failure") there is a specific reference to atomic goal — Qwerto, Feb 20 '18 at 08:57
Maybe it's due to the fact the we use one atom at the time , in the sld resolution — Qwerto, Feb 20 '18 at 09:00

score 0 · Accepted Answer · answered Feb 20 '18 at 10:47

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.

1 Answers1