SLD Resolution and Logic Consequence

Question

I have a program P and i start the SLD Resolution with a certain goal clause. Is every clause generated a logical consequence of P ? And why ?

ps: the very fact, is that i havent understood why , starting with a goal clase, we are sure that if a goal clause generate a success so this goal clause belong to the Least Herbrand Set....

psS : if every goal is also a logical consequence of P, why if we have a success we are sure that the goal that produce it belong to the Least Herbrand Set ?

Answer 1

Regarding Resolution rule in general, it is a valid rule of inference, where the validity property means that:

it is impossible for the premises to be true and the conclusion nevertheless to be false.

Thus, if the conclusion of the rule is true wherever the premises are, this means that the conclusion is logical consequence of the premises.

---

Regarding SLD, we have that:

Let $P$ be a definite program and $G$ a definite goal $\leftarrow A_1, \ldots, A_k$. An answer for $P \cup \{ G \}$ is a substitution for variables of $G$.

If $\theta$ is an answer for $P \cup \{ G \}$, we say that $\theta$ is a correct answer for $P \cup \{ G \}$ if $\forall x_i[(A_1 \land \ldots \land A_k)]\theta$ is a logical consequence of $P$.

This amounts to saying that $\theta$ is a correct answer iff $P \cup \{ \lnot \forall x_i[(A_1 \land \ldots \land A_k)]\theta \}$ ia unsatisfiable.

For the definition of SLD-derivation, see the previous post.

An SLD-refutation of $P \cup \{ G \}$ is a finite SLD-derivation of $P \cup \{ G \}$ which has the empty clause $\square$ as the last goal in the derivation. If $G_n = \square$, we say the refutation has length $n$.

A computed answer $\theta$ for $P \cup \{ G \}$ is the substitution obtained by restricting the composition $\theta_1\ldots \theta_n$ to the variables of $G$, where $\theta_1,\ldots, \theta_n$ is the sequence of $\text{mgu}$'s used in an SLD-refutation of $P \cup \{ G \}$.

SLD-refutation is sound:

let $P$ be a definite program and $G$ a definite goal. Then every computed answer for $P \cup \{ G \}$ is a correct answer for $P \cup \{ G \}$.

---

Regarding substitution and unification, we have that a substitution $\theta$ is an operation that replaces variables $x_i$ into an expression with terms $ti$.

If the $t_i$ are all ground terms (i.e. "closed"), the subst is called ground substitution.

Let $S = \{ A_1,\ldots, A_n \}$ be a finite set of atoms. A unifier $\theta$ is a substitution such that: $A_1 \theta = \ldots =A_n \theta$.

A most general unifier ($\text{mgu}$) for $S$ is a unifier $\mu$ such that any unifier $\theta$ of $S$ can be expressed as: $\theta = μλ$ for some substitution $λ$.

We can prove that:

Let $P$ be a definite program and $G$ a definite goal $\leftarrow A_1, \ldots, A_k$. Suppose $\theta$ is an answer for $P \cup \{ G \}$ such that $[A_1 \land \ldots \land A_k)]\theta$ is ground.

Then the following are equivalent:

(a) $\theta$ is correct;

(b) $[A_1 \land \ldots \land A_k)]\theta$ is true in every Herbrand model of $P$;

(c) $[A_1 \land \ldots \land A_k)]\theta$ is true wit the least Herbrand model of $P$.