5.3 Propositional Definite Clauses

5.3.2 Proofs

So far, we have specified what an answer is, but not how it can be computed. The definition of specifies which propositions should be logical consequences of a knowledge base but not how to compute them. The problem of deduction is to determine if some proposition is a logical consequence of a knowledge base. Deduction is a specific form of inference.

A proof is a mechanically derivable demonstration that a proposition logically follows from a knowledge base. A theorem is a provable proposition. A proof procedure is a – possibly non-deterministic – algorithm for deriving consequences of a knowledge base. (See the box for a description of non-deterministic choice.)

Given a proof procedure, KBg means g can be proved or derived from knowledge base KB.

A proof procedure’s quality can be judged by whether it computes what it is meant to compute.

A proof procedure is sound with respect to a semantics if everything that can be derived from a knowledge base is a logical consequence of the knowledge base. That is, if KBg, then KBg.

A proof procedure is complete with respect to a semantics if there is a proof of each logical consequence of the knowledge base. That is, if KBg, then KBg.

We present two ways to construct proofs for propositional definite clauses: a bottom-up procedure and a top-down procedure.

Bottom-Up Proof Procedure

A bottom-up proof procedure can be used to derive all logical consequences of a knowledge base. It is called bottom-up as an analogy to building a house, where each part of the house is built on the structure already completed. The bottom-up proof procedure builds on atoms that have already been established. It should be contrasted with a top-down approach, which starts from a query and tries to find definite clauses that support the query. Sometimes we say that a bottom-up procedure is forward chaining on the definite clauses, in the sense of going forward from what is known rather than going backward from the query.

The general idea is based on one rule of derivation, a generalized form of the rule of inference called modus ponens:

If “ha1am” is a definite clause in the knowledge base, and each ai has been derived, then h can be derived.

An atomic clause corresponds to the case of m=0; modus ponens can always immediately derive any atomic clauses in the knowledge base.

1:procedure Prove_DC_BU(KB)
2:      Inputs
3:            KB: a set of definite clauses       
4:      Output
5:            Set of all atoms that are logical consequences of KB
6:      Local
7:            C is a set of atoms       
8:      C:={}
9:      repeat
10:            selectha1am” in KB where aiC for all i, and hC
11:            C:=C{h}
12:      until no more definite clauses can be selected
13:      return C
Figure 5.3: Bottom-up proof procedure for computing consequences of KB

Figure 5.3 gives a procedure for computing the consequence set C of a set KB of definite clauses. Under this proof procedure, if g is an atom, KBg if gC at the end of the Prove_DC_BU procedure. For a conjunction, KBg1gk, if {g1,,gk}C.

Example 5.9.

Suppose the system is given the knowledge base KB:

abc.
bde.
bge.
ce.
d.
e.
fag.

One trace of the value assigned to C in the bottom-up procedure is

{}
{d}
{e,d}
{c,e,d}
{b,c,e,d}
{a,b,c,e,d}.

The algorithm terminates with C={a,b,c,e,d}. Thus, 𝐾𝐵a, 𝐾𝐵b, and so on.

The last rule in KB is never used. The bottom-up proof procedure cannot derive f or g. This is as it should be because there is a model of the knowledge base in which f and g are both false.

The proof procedure of Figure 5.3 has a number of interesting properties:

Soundness

Every atom in C is a logical consequence of KB. That is, if KBg then KBg. To show this, assume that there is an atom in C that is not a logical consequence of KB. If such an atom exists, let h be first atom added to C that is not true in every model of KB. Suppose I is a model of KB in which h is false. Because h has been generated, there must be some definite clause in KB of the form ha1am such that a1am are all in C (which includes the case where h is an atomic clause and so m=0). Because h is the first atom added to C that is not true in all models of KB, and the ai are generated before h, all of the ai true in I. This clause’s head is false in I, and its body is true in I. Therefore, by the definition of truth of clauses, this clause is false in I. This is a contradiction to the fact that I is a model of KB. Thus, every element of C is a logical consequence of KB.

Complexity

The algorithm of Figure 5.3 halts, and the number of times the loop is repeated is bounded by the number of definite clauses in KB. This is easily seen because each definite clause is only used at most once. Thus, the time complexity of the bottom-up proof procedure is linear in the size of the knowledge base if it indexes the definite clauses so that the inner loop is carried out in constant time.

Fixed Point

The final C generated in the algorithm of Figure 5.3 is called a fixed point because any further application of the rule of derivation does not change C. C is the least fixed point because there is no smaller fixed point.

Let I be the interpretation in which every atom in the least fixed point is true and every atom not in the least fixed point is false. To show that I must be a model of KB, suppose “ha1amKB is false in I. The only way this could occur is if a1,,am are in the fixed point, and h is not in the fixed point. By construction, the rule of derivation can be used to add h to the fixed point, a contradiction to it being the fixed point. Therefore, there can be no definite clause in KB that is false in an interpretation defined by a fixed point. Thus, I is a model of KB.

I is the minimal model in the sense that it has the fewest true propositions. Every other model must also assign the atoms in C to be true.

Completeness

Suppose KBg. Then g is true in every model of KB, so it is true in the minimal model, and so it is in C, and so KBg.

Top-Down Proof Procedure

An alternative proof method is to search backward or top-down from a query to determine whether it is a logical consequence of the given definite clauses. This procedure is called propositional definite clause resolution or SLD resolution, where SL stands for Selecting an atom using a Linear strategy, and D stands for Definite clauses. It is an instance of the more general resolution method.

The top-down proof procedure can be understood in terms of answer clauses. An answer clause is of the form

yesa1a2am

where yes is a special atom. Intuitively, yes is going to be true exactly when the answer to the query is “yes.”

If the query is

𝖺𝗌𝗄 q1qm

the initial answer clause is

yesq1qm

Given an answer clause, the top-down algorithm selects an atom in the body of the answer clause. Suppose it selects a1. The atom selected is called a subgoal. The algorithm proceeds by doing steps of resolution. In one step of resolution, it chooses a definite clause in KB with a1 as the head. If there is no such clause, the algorithm fails.

Note the use of select and choose (box). Any atom in the body can be selected, and if one selection does not lead to a proof, other selections do not need to be tried. When choosing a clause, the algorithm may need to search for a choice that makes the proof succeed.

The resolvent of the above answer clause on the selection a1 with the definite clause

a1b1bp

is the answer clause

yesb1bpa2am

That is, the subgoal in the answer clause is replaced by the body of the chosen definite clause.

An answer is an answer clause with an empty body (m=0). That is, it is the answer clause yes.

An SLD derivation of a query “𝖺𝗌𝗄 q1qk” from knowledge base KB is a sequence of answer clauses γ0,γ1,,γn such that

  • γ0 is the answer clause corresponding to the original query, namely the answer clause yesq1qk

  • γi is the resolvent of γi-1 with a definite clause in KB

  • γn is an answer.

Another way to think about the algorithm is that the top-down algorithm maintains a collection G of atoms to prove. Each atom that must be proved is a subgoal. Initially, G is the set of atoms in the query. A clause ab1bp means subgoal a can be replaced by subgoals b1,,bp. The G to be proved corresponds to the answer clause yesG.

1:non-deterministic procedure Prove_DC_TD(KB,Query)
2:      Inputs
3:            KB: a set of definite clauses
4:            Query: a set of atoms to prove       
5:      Output
6:            yes if KBQuery and the procedure fails otherwise
7:      Local
8:            G is a set of atoms       
9:      G:=Query
10:      repeat
11:            select an atom a in G
12:            choose definite clause “aB” in KB with a as head
13:            G:=B(G{a})
14:      until G={}
15:      return yes
Figure 5.4: Top-down definite clause proof procedure

Figure 5.4 specifies a non-deterministic procedure for solving a query. It follows the definition of a derivation. In this procedure, G is the set of atoms in the body of the answer clause. The procedure is non-deterministic: at line 12 has to choose a definite clause to resolve against. If there are choices that result in G being the empty set, the algorithm returns yes; otherwise it fails, and the answer is no.

This algorithm treats the body of a clause as a set of atoms and G is also a set of atoms. An alternative is to have G as an ordered list of atoms, perhaps with an atom appearing more than once.

Example 5.10.

Suppose the system is given the knowledge base:

abc.
bde.
bge.
ce.
d.
e.
fag.

It is asked the query:

𝘢𝘴𝘬 a.

The following shows a derivation that corresponds to a sequence of assignments to G in the repeat loop of Figure 5.4. Here we have written G in the form of an answer clause, and always selected the leftmost atom in the body:

𝑦𝑒𝑠a
𝑦𝑒𝑠bc
𝑦𝑒𝑠dec
𝑦𝑒𝑠ec
𝑦𝑒𝑠c
𝑦𝑒𝑠e
𝑦𝑒𝑠

The following shows a sequence of choices, where the second definite clause for b was chosen. This choice does not lead to a proof.

𝑦𝑒𝑠a
𝑦𝑒𝑠bc
𝑦𝑒𝑠gec

If g is selected, there are no rules that can be chosen. This proof attempt is said to fail.

The non-deterministic top-down algorithm of Figure 5.4 together with a selection strategy induces a search graph. Each node in the search graph represents an answer clause. The neighbors of a node yesa1am, where a1 is the selected atom, represent all of the possible answer clauses obtained by resolving on a1. There is a neighbor for each definite clause whose head is a1. The goal nodes of the search are of the form yes.

Example 5.11.

Given the knowledge base

abc.ag.ah.bj.bk.dm.dp.fm.fp.gm.gf.km.hm.p.

and the query

𝘢𝘴𝘬 ad.

the search graph for an SLD derivation, assuming the leftmost atom is selected in each answer clause, is shown in Figure 5.5.

𝑦𝑒𝑠ad

𝑦𝑒𝑠gd

𝑦𝑒𝑠bcd

𝑦𝑒𝑠hd

𝑦𝑒𝑠jcd

𝑦𝑒𝑠kcd

𝑦𝑒𝑠mcd

𝑦𝑒𝑠md

𝑦𝑒𝑠fd

𝑦𝑒𝑠md

𝑦𝑒𝑠pd

𝑦𝑒𝑠d

𝑦𝑒𝑠m

𝑦𝑒𝑠p

𝑦𝑒𝑠

𝑦𝑒𝑠md

Figure 5.5: A search graph for a top-down derivation

The search graph is not defined statically, because this would require anticipating every possible query. Instead, the search graph is dynamically constructed as needed. All that is required is a way to generate the neighbors of a node. Selecting an atom in the node’s answer clause defines a set of neighbors: the node has a neighbor for each clause with the selected atom as its head.

Any of the search methods of Chapter 3 can be used to search the search space. Because we are only interested in whether the query is a logical consequence, we just require a path to a goal node; an optimal path is not necessary. The search space depends on the query and which atom is selected at each node.

When the top-down procedure has derived the answer, the rules used in the derivation can be used in a bottom-up proof procedure to infer the query. Similarly, a bottom-up proof of an atom can be used to construct a corresponding top-down derivation. This equivalence can be used to show the soundness and completeness of the top-down proof procedure. As defined, the top-down proof procedure may spend extra time re-proving the same atom multiple times, whereas the bottom-up procedure proves each atom only once. However, the bottom-up procedure proves every atom, but the top-down procedure proves only atoms that are relevant to the query.

It is possible that the proof procedure can get into an infinite loop, as in the following example (without cycle pruning).

Example 5.12.

Consider the knowledge base and query:

ga.
ab.
ba.
gc.
c.
𝘢𝘴𝘬 g.

Atoms g and c are the only atomic logical consequences of this knowledge base, and the bottom-up proof procedure will halt with fixed point {c,g}. However, the top-down proof procedure with a depth-first search will go on indefinitely, and not halt if the first clause for g is chosen, and there is no cycle pruning.

The algorithm requires a selection strategy to decide which atom to select at each time. In the above examples the leftmost atom a1 was selected, but any atom could be selected. Which atom is selected affects the efficiency and perhaps even whether the algorithm terminates if there is no cycle pruning. The best selection strategy is to select the atom that is most likely to fail. Ordering the atoms and selecting the leftmost atom is a common strategy, because this lets someone who is providing the rules provide heuristic knowledge about which atom to select.