The top-down proof procedure can be extended to handle variables by allowing instances of rules to be used in the derivation.

A generalized answer clause is of the form

where $t_1,\mathrm{\dots },t_k$ are terms and $a_1,\mathrm{\dots },a_m$ are atoms. The use of $yes$ enables answer extraction: determining which instances of the query variables are a logical consequence of the knowledge base.

Initially, the generalized answer clause for query $q$ is

where $V_1,\mathrm{\dots },V_k$ are the variables that appear in $q$. Intuitively this means that an instance of $yes(V_1,\mathrm{\dots },V_k)$ is true if the corresponding instance of the query is true.

The proof procedure maintains a current generalized answer clause.

At each stage, the algorithm selects an atom in the body of the generalized answer clause. It then chooses a clause in the knowledge base whose head unifies with the atom.

The SLD resolution of the generalized answer clause

on $a_1$ with the chosen clause

where $a_1$ and $a$ have most general unifier $\sigma$, is the answer clause

where the body of the chosen clause has replaced $a_1$ in the answer clause, and the MGU $\sigma$ is applied to the whole answer clause.

An SLD derivation is a sequence of generalized answer clauses ${\gamma }_0$, ${\gamma }_1$, $\mathrm{\dots }$, ${\gamma }_n$ such that

• •

  ${\gamma }_0$ is the answer clause corresponding to the original query. If the query is $q$, with free variables $V_1,\mathrm{\dots },V_k$, the initial generalized answer clause ${\gamma }_0$ is

  $yes(V_1,\mathrm{\dots },V_k)\leftarrow q.$

• •

  ${\gamma }_i$ is obtained by selecting an atom $a_1$ in the body of ${\gamma }_{i-1}$; choosing a copy of a clause $a\leftarrow b_1\wedge \mathrm{\dots }\wedge b_p$ in the knowledge base whose head, $a$, unifies with $a_i$; replacing $a_1$ with the body, $b_1\wedge \mathrm{\dots }\wedge b_p$; and applying the unifier to the whole resulting answer clause.

  The main difference between this and the propositional top-down proof procedure is that, for clauses with variables, the proof procedure must take copies of clauses from the knowledge base. The copying renames the variables in the clause with new names. This is both to remove name clashes between variables and because a single proof may use different instances of a clause.

• •

  ${\gamma }_n$ is an answer. That is, it is of the form

  $yes(t_1,\mathrm{\dots },t_k)\leftarrow .$

  When this occurs, the algorithm returns the answer

  $$V_1=t_1,\mathrm{\dots },V_k=t_k.$$

Notice how the answer is extracted; the arguments to $yes$ keep track of the instances of the variables in the initial query that lead to a successful proof.

Figure 13.4 gives a non-deterministic algorithm that answer queries by searching for SLD derivations. This is non-deterministic in the sense that all derivations can be found by making appropriate choices that do not fail. If all choices fail, the algorithm fails, and there are no derivations. The “choose” on line 13 is implemented using search. Recall that $Unify(a_i,a)$ returns an MGU of $a_i$ and $a$, if there is one, and $\perp$ if they do not unify. The algorithm for $Unify$ is given in Figure 13.3.