foundations of computational agents
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 are terms and are atoms. The use of 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 is
where are the variables that appear in . Intuitively this means that an instance of 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 with the chosen clause
where and have most general unifier , is the answer clause
where the body of the chosen clause has replaced in the answer clause, and the MGU is applied to the whole answer clause.
An SLD derivation is a sequence of generalized answer clauses , , , such that
is the answer clause corresponding to the original query. If the query is , with free variables , the initial generalized answer clause is
is obtained by selecting an atom in the body of ; choosing a copy of a clause in the knowledge base whose head, , unifies with ; replacing with the body, ; 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.
is an answer. That is, it is of the form
When this occurs, the algorithm returns the answer
Notice how the answer is extracted; the arguments to 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 returns an MGU of and , if there is one, and if they do not unify. The algorithm for is given in Figure 13.3.
Consider the database of Figure 13.2 and the query
Figure 13.5 shows a successful derivation with answer .
Note that this derivation used two instances of the rule
One instance eventually substituted for , and one instance substituted for .
When the atom was selected, other choices of the clause to resolve with would have resulted in a partial derivation that could not be completed.