# 13.4.4 Definite Resolution with Variables

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

 $\displaystyle{yes(t_{1},\ldots,t_{k})\leftarrow\mbox{}a_{1}\wedge\mbox{}a_{2}% \wedge\mbox{}\ldots\wedge\mbox{}a_{m}}$

where $t_{1},\ldots,t_{k}$ are terms and $a_{1},\ldots,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

 $yes(V_{1},\ldots,V_{k})\leftarrow\mbox{}q$

where $V_{1},\ldots,V_{k}$ are the variables that appear in $q$. Intuitively this means that an instance of $yes(V_{1},\ldots,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

 $yes(t_{1},\ldots,t_{k})\leftarrow\mbox{}a_{1}\wedge\mbox{}a_{2}\wedge\mbox{}% \ldots\wedge\mbox{}a_{m}$

on $a_{1}$ with the chosen clause

 $\displaystyle{a\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{p}}$

where $a_{1}$ and $a$ have most general unifier $\sigma$, is the answer clause

 $\displaystyle{(yes(t_{1},\ldots,t_{k})\leftarrow\mbox{}b_{1}\wedge\mbox{}% \ldots\wedge\mbox{}b_{p}\wedge\mbox{}a_{2}\wedge\mbox{}\ldots\wedge\mbox{}a_{m% })\sigma}$

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}$, $\ldots$, $\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},\ldots,V_{k}$, the initial generalized answer clause $\gamma_{0}$ is

 $\displaystyle{yes(V_{1},\ldots,V_{k})\leftarrow\mbox{}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\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{p}$ in the knowledge base whose head, $a$, unifies with $a_{i}$; replacing $a_{1}$ with the body, $b_{1}\wedge\mbox{}\ldots\wedge\mbox{}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

 $\displaystyle{yes(t_{1},\ldots,t_{k})\leftarrow\mbox{}.}$

When this occurs, the algorithm returns the answer

 $V_{1}=t_{1},\ldots,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 $\bot$ if they do not unify. The algorithm for $Unify$ is given in Figure 13.3.

###### Example 13.23.

Consider the database of Figure 13.2 and the query

 $\mbox{{ask}~{}}~{}two\_doors\_east(R,r107).$

Figure 13.5 shows a successful derivation with answer $R=r111$.

Note that this derivation used two instances of the rule

 ${imm\_east(E,W)\leftarrow\mbox{}imm\_west(W,E)}.$

One instance eventually substituted $r111$ for $E$, and one instance substituted $r109$ for $E$.

When the atom $imm\_west(M_{1},R)$ was selected, other choices of the clause to resolve with would have resulted in a partial derivation that could not be completed.