Goal Clause as resolvent

Question

I have studied the Robinson Resolution Principle and i've notice that my prof considers the goal clauses (used for example in SLD Resolution) as resolvent. How is it possibile to convert a resolvent into a goal clause ?

Answer 1

SLD-Resolution uses Horn clauses, written:

$A \leftarrow B_1, \ldots, B_n$

that are equivalent to "usual" clauses: $\lnot B_1 \lor \ldots \lor \lnot B_n \lor A$ [$A$ is called the head of the clause]

A goal clause is a Horn clause with no positive literals $\leftarrow B_1, \ldots, B_n$ (i.e. $\lnot B_1 \lor \ldots \lor \lnot B_n$).

A program clause is a Horn clause with one positive literal and one or more negative literals.

SLD-Resolution consider a set $P$ of program clauses and a goal clause $G$.

A derivation by SLD-resolution is a sequence of resolution steps between goal clauses and the program clauses.

The first goal clause $G_0$ is $G$. $G_{i+1}$ is derived from $G_i$ selecting a literal $A_i^j \in G_i$, choosing a clause $C_i \in P$ such that the head of $C_i$ (call it $B_i^0$) unifies with $A_i^j$ by the most general unifier $θ_i$ and resolving.

That is, in "usual" clause form, we have:

$G_i := \lnot A_i^1 \lor \ldots \lor \lnot A_i^j \lor \lnot A_i^{j+1} \lor \ldots \lnot A_i^{n_i}$,

and:

$C_i := \lnot B_i^1 \lor \ldots \lor \lnot B_i^{k_i} \lor B_i^0$.

Considering $[A_i^j]θ_i=[B_i^0]θ_i$, we get the resolvent:

$G_{i+1} := [\lnot A_i^1 \lor \ldots \lor \lnot A_i^{j-1} \lor \lnot B_i^1 \lor \ldots \lor \lnot B_i^{k_i}\lor \lnot A_i^{j+1} \lor \ldots \lnot A_i^{n_i}]θ_i.$

As you can see, the resolvent $G_{i+1}$ is a new goal clause: it has no positive literals.