13.4 Proofs and Substitutions

13.4.2 Bottom-up Procedure with Variables

The propositional bottom-up proof procedure can be extended to Datalog by using ground instances of the clauses. A ground instance of a clause is obtained by uniformly substituting constants for the variables in the clause. The constants required are those appearing in the knowledge base or in the query. If there are no constants in the knowledge base or the query, one must be invented.

Example 13.19.

Suppose the knowledge base is

q(a).
q(b).
r(a).
s(W)r(W).
p(X,Y)q(X)s(Y).

The set of all ground instances is

q(a).
q(b).
r(a).
s(a)r(a).
s(b)r(b).
p(a,a)q(a)s(a).
p(a,b)q(a)s(b).
p(b,a)q(b)s(a).
p(b,b)q(b)s(b).

The propositional bottom-up proof procedure of Section 5.3.2 can be applied to the grounding to derive q(a), q(b), r(a), s(a), p(a,a), and p(b,a) as the ground instances that are logical consequences.

Example 13.20.

Suppose the knowledge base is

p(X,Y).
gp(W,W).

The bottom-up proof procedure for query “𝖺𝗌𝗄 g” must invent a new constant symbol, say c. The set of all ground instances is then

p(c,c).
gp(c,c).

The propositional bottom-up proof procedure will derive p(c,c) and g.

If the query were “𝖺𝗌𝗄 p(b,d)” the set of ground instances would change to reflect the constants b and d.

The bottom-up proof procedure applied to the grounding of the knowledge base is sound, because each instance of each rule is true in every model. This procedure is essentially the same as the variable-free case, but it uses the set of ground instances of the clauses, all of which are true because the variables in a clause are universally quantified.

This bottom-up procedure will eventually halt for Datalog because there are only finitely many grounded atoms, and one ground atom is added to the consequence set each time through the loop.

This procedure is also complete for ground atoms. That is, if a ground atom is a consequence of the knowledge base, it will be derived. To prove this, as in the propositional case, we construct a particular generic model. Recall that a model specifies the domain, what the constants denote, and what is true. A Herbrand interpretation is an interpretation where the domain is symbolic and consists of all constants of the language. A constant is invented if there are no constants in the knowledge base or the query. In a Herbrand interpretation, each constant denotes itself. Thus, in the definition of an interpretation, D and ϕ are fixed for a given program, and all that needs to be specified is π, which defines the predicate symbols.

Consider the Herbrand interpretation where the true atoms are the ground instances of the relations that are eventually derived by the bottom-up procedure. It is easy to see that this Herbrand interpretation is a model of the rules given. As in the variable-free case, it is a minimal model in that it has the fewest true atoms of any model. If KBg for ground atom g, then g is true in the minimal model and, thus, is eventually derived.

Example 13.21.

Consider the clauses of Figure 13.2. The bottom-up proof procedure can immediately derive each instance of imm_west given as a fact. The algorithm can then add the imm_east atoms to the consequence set:

imm_east(r103,r101)
imm_east(r105,r103)
imm_east(r107,r105)
imm_east(r109,r107)
imm_east(r111,r109)
imm_east(r129,r131)
imm_east(r127,r129)
imm_east(r125,r127)

Next, the next_door relations that follow can be added to the set of consequences, including

next_door(r101,r103)
next_door(r103,r101)

The two_door_east relations can be added to the set of consequences, including

two_door_east(r105,r101)
two_door_east(r107,r103)

Finally, the west relations that follow can be added to the set of consequences.