Im studying the SLD derivation for First Order Logic and a question came to me. I've tried to consult many books but i didnt find anything about.
Every time that i produce a SLD Derivation, using the same mgu $\theta$ i can produce a correct answer. It this true ?
Yes.
We have that:
Let $P$ be a program [i.e. a set of program clauses] and $G$ a goal clause [e.g. $\lnot A_1 \lor \ldots \lor \lnot A_n$]. A substitution $θ$ for the variables in $G$ is a correct answer substitution if $P \vDash \forall x_i[¬G]θ$, where the universal quantification is taken over all the free variables $x_i$ in $[¬G]θ$.
As said in the previous answer, the new goal clause produced with resolution and unification is the resolvent of the previous goal clause and one of the clauses in $P$.
Thus, the procedure of SLD-refutation (like that for propositional resolution) is aimed at the derivation of the empty clause, meaning that the set $P \cup \{ \lnot G \}$ is unsatisfiable.
This amounts to saying that $G$ is logical consequence of $P$, i.e. $P \vDash \forall x_i[¬G]θ$ means:
$P \vDash ∀x_i[(A_1 \land \ldots \land A_n)]θ$.
