### 12.4.2 Definite Resolution with Variables

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

A **generalized answer clause** is of the form

*yes(t*

_{1},...,t_{k})←a_{1}∧a_{2}∧...∧a_{m},where *t _{1},...,t_{k}* are terms and

*a*are atoms. The use of

_{1},...,a_{m}*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},...,V_{k})←q,

where *V _{1},...,V_{k}* are the variables that appear in

*q*. Intuitively this means that an instance of

*yes(V*is true if the corresponding instance of the query is true.

_{1},...,V_{k})The proof procedure maintains a current generalized answer clause.

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

*a*. The

_{i}**SLD resolution**of the generalized answer clause

*yes(t*on

_{1},...,t_{k})←a_{1}∧a_{2}∧...∧a_{m}*a*with the chosen clause

_{i}*a←b*

_{1}∧...∧b_{p},where *a _{i}* and

*a*have most general unifier

*σ*, is the answer clause

*(yes(t*

_{1},...,t_{k})←a_{1}∧...∧a_{i-1}∧b_{1}∧...∧b_{p}∧a_{i+1}∧...∧a_{m})σ,where the body of the chosen clause has replaced *a _{i}* in the answer
clause, and the MGU is applied to the whole answer
clause.

An **SLD derivation** is a sequence of generalized answer clauses
*γ _{0}*,

*γ*,

_{1}*...*,

*γ*such that

_{n}*γ*is the answer clause corresponding to the original query. If the query is_{0}*q*, with free variables*V*, the initial generalized answer clause_{1},...,V_{k}*γ*is_{0}*yes(V*_{1},...,V_{k})←q.*γ*is obtained by selecting an atom_{i}*a*in the body of_{i}*γ*; choosing a_{i-1}*copy*of a clause*a←b*in the knowledge base whose head,_{1}∧...∧b_{p}*a*, unifies with*a*; replacing_{i}*a*with the body,_{i}*b*; and applying the unifier to the whole resulting answer clause._{1}∧...∧b_{p}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.*γ*is an answer. That is, it is of the form_{n}*yes(t*_{1},...,t_{k})←.When this occurs, the algorithm returns the answer

*V*_{1}=t_{1},...,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.

**non-deterministic procedure**

*FODCDeductionTD*(

*KB,q*)

2:

**Inputs**

3:

*KB*: a set definite clauses

4: Query

*q*: a set of atoms to prove, with variables

*V*

_{1},...,V_{k}5:

**Output**

6: substitution

*θ*if

*KB q θ*and fail otherwise

7:

**Local**

8:

*G*is a generalized answer clause

9: Set

*G*to generalized answer clause

*yes(V*

_{1},...,V_{k})←q10:

**while**(

*G*is not an answer)

11: Suppose

*G*is

*yes(t*

_{1},...,t_{k})←a_{1}∧a_{2}∧...∧a_{m}12:

**select**atom

*a*in the body of

_{i}*G*

13:

**choose**clause

*a←b*in

_{1}∧...∧b_{p}*KB*

14: Rename all variables in

*a←b*to have new names

_{1}∧...∧b_{p}15: Let

*σ*be

*unify(a*. Fail if

_{i},a)*unify*returns

*⊥*.

16: assign

*G*the answer clause:

*(yes(t*

_{1},...,t_{k})←a_{1}∧...∧a_{i-1}∧b_{1}∧...∧b_{p}∧a_{i+1}∧...∧a_{m})σ17:

18:

**return**

*V*where

_{1}=t_{1},...,V_{k}=t_{k}*G*is

*yes(t*

_{1},...,t_{k})←A non-deterministic procedure that answers queries by finding SLD
derivations is given in Figure 12.3. 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 is implemented using search. This algorithm
assumes that *unify(a _{i},a)* returns an MGU of

*a*and

_{i}*a*, if there is one, and

*⊥*if they do not unify. Unification is defined in the next section.

**Example 12.21:**Consider the database of Figure 12.2 and the query

asktwo_doors_east(R,r107).

Figure 12.4 shows a successful derivation with answer *R=r111*.

*yes(R)←two_doors_east(R,r107)*

*resolve with two_doors_east(E*

_{1},W_{1}) ←*imm_east(E*

_{1},M_{1}) ∧imm_east(M_{1},W_{1}).*substitution: {E*

_{1}/R,W_{1}/r107}*yes(R)←imm_east(R,M*

_{1}) ∧imm_east(M_{1},r107)*select leftmost conjunct*

*resolve with imm_east(E*

_{2},W_{2})←imm_west(W_{2},E_{2})*substitution: {E*

_{2}/R,W_{2}/M_{1}}*yes(R)←imm_west(M*

_{1},R) ∧imm_east(M_{1},r107)*select leftmost conjunct*

*resolve with imm_west(r109,r111)*

*substitution: {M*

_{1}/r109,R/r111}*yes(r111)←imm_east(r109,r107)*

*resolve with imm_east(E*

_{3},W_{3})←imm_west(W_{3},E_{3})*substitution: {E*

_{3}/r109,W_{3}/r107}*yes(r111)←imm_west(r107,r109)*

*resolve with imm_west(r107,r109)*

*substitution: {}*

*yes(r111)←*

Note that this derivation used two instances of the rule

imm_east(E,W) ←imm_west(W,E).

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

Some choices of which clauses to resolve against may have resulted in a partial derivation that could not be completed.