Artificial
Intelligence

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

where t₁,...,t_k are terms and a₁,...,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₁,...,V_k)←q,

where V₁,...,V_k are the variables that appear in q. Intuitively this means that an instance of yes(V₁,...,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 a_i in the body of the generalized answer clause. It then chooses a clause in the knowledge base whose head unifies with a_i. The SLD resolution of the generalized answer clause yes(t₁,...,t_k)←a₁∧a₂∧...∧a_m on a_i with the chosen clause

where a_i and a have most general unifier σ, is the answer clause

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 γ₀, γ₁, ..., γ_n such that

• γ₀ is the answer clause corresponding to the original query. If the query is q, with free variables V₁,...,V_k, the initial generalized answer clause γ₀ is
  yes(V₁,...,V_k)←q.
• γ_i is obtained by selecting an atom a_i in the body of γ_i-1; choosing a copy of a clause a←b₁∧...∧b_p in the knowledge base whose head, a, unifies with a_i; replacing a_i with the body, b₁∧...∧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.

• γ_n is an answer. That is, it is of the form
  yes(t₁,...,t_k)←.

  When this occurs, the algorithm returns the answer

  V₁=t₁,...,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₁,...,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₁,...,V_k)←q
10:           while (G is not an answer)
11:                     Suppose G is yes(t₁,...,t_k)←a₁∧a₂∧...∧a_m
12:                     select atom a_i in the body of G
13:                     choose clause a←b₁∧...∧b_p in KB
14:                     Rename all variables in a←b₁∧...∧b_p to have new names
15:                     Let σ be unify(a_i,a). Fail if unify returns ⊥.
16:                     assign G the answer clause: (yes(t₁,...,t_k)←a₁∧...∧a_i-1 ∧b₁∧...∧b_p∧a_i+1∧...∧a_m)σ
17:           
18:           return V₁=t₁,...,V_k=t_k where G is yes(t₁,...,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_i and a, if there is one, and ⊥ if they do not unify. Unification is defined in the next section.

• 12.4.2.1 Unification