5.3 Propositional Definite Clauses

The rest of this chapter considers some restricted languages and reasoning tasks that are useful and can be efficiently implemented.

The language of propositional definite clauses is a subset of propositional calculus that does not allow uncertainty or ambiguity. In this language, propositions have the same meaning as in propositional calculus, but not all compound propositions are allowed in a knowledge base.

The syntax of propositional definite clauses is defined as follows:

  • An atomic proposition or atom is the same as in propositional calculus.

  • A definite clause is of the form


    where h is an atom, the head of the clause, and each ai is an atom. It can be read “h if a1 and …and am”.

    If m>0, the clause is called a rule, where a1am is the body of the clause.

    If m=0, the arrow can be omitted and the clause is called an atomic clause or fact. The clause has an empty body.

  • A knowledge base is a set of definite clauses.

Example 5.7.

The elements of the knowledge base in Example 5.2 are all definite clauses.

The following are not definite clauses:


The fourth statement is not a definite clause because an atom must start with a lower-case letter.

A definite clause ha1am is false in interpretation I if a1,,am are all true in I and h is false in I; otherwise, the definite clause is true in I.

A definite clause is a restricted form of a clause. For example, the definite clause


is equivalent to the clause


In general, a definite clause is equivalent to a clause with exactly one positive literal (non-negated atom). Propositional definite clauses cannot represent disjunctions of atoms (e.g., ab) or disjunctions of negated atoms (e.g., ¬c¬d).

Refer to caption
Figure 5.2: An electrical environment with components named
Example 5.8.

Consider how to axiomatize the electrical environment of Figure 5.2 following the methodology for the user’s view of semantics. This axiomatization will allow us to simulate the electrical system. It will be expanded in later sections to let us diagnose faults based on observed symptoms.

The representation will be used to determine whether lights are on or off, based on switch positions and the status of circuit breakers.

The knowledge base designer must choose a level of abstraction. The aim is to represent the domain at the most general level that will enable the agent to solve the problems it must solve. We also want to represent the domain at a level that the agent will have information about. For example, we could represent the actual voltages and currents, but exactly the same reasoning would be done if this were a 12-volt DC system or a 120-volt AC system; the voltages and frequencies are irrelevant for questions about how switch positions (up or down) affect whether lights are on. Our agent is not concerned here with the color of the wires, the design of the switches, the length or weight of the wire, the date of manufacture of the lights and the wires, or any of the other myriad details one could imagine about the domain.

Let’s represent this domain at a commonsense level that non-electricians may use to describe the domain, in terms of wires being live and currents flowing from the outside through wires to the lights, and that circuit breakers and light switches connect wires if they are turned on and working.

The designer must choose what to represent. Here we represent propositions about whether lights are lit, whether wires are live, whether switches are up or down, and whether components are working properly.

We then choose atoms with a specific meaning in the world. We can use descriptive names for these. For example, up_s2 is true when switch s2 is up. ok_l1 is true when light l1 is working properly (will be lit if it is has power coming into it). live_w1 is true when w1 has power coming in. The computer does not know the meaning of these names and does not have access to the components of the atom’s name.

At this stage, we have not told the computer anything. It does not know what the atoms are, let alone what they mean.

Once we have decided which symbols to use and what they mean, we tell the system, using definite clauses, background knowledge about what is true in the world. The simplest forms of definite clauses are those without bodies – the atomic clauses – such as


The designer may look at part of the domain and know that light l1 is live if wire w0 is live, because they are connected together, but may not know whether w0 is live. Such knowledge is expressible in terms of rules:


Online, the user is able to input the observations of the current switch positions, such as


The knowledge base consists of all the definite clauses, whether specified as background knowledge or as observations.

5.3.1 Queries and Answers

One reason to build a description of a real or imaginary world is to be able to determine what else must be true in that world. After the computer is given a knowledge base about a particular domain, a user might like to ask the computer questions about that domain. The computer can answer whether or not a proposition is a logical consequence of the knowledge base. A user that knows the meaning of the atoms, for example when is up_s3 true, can interpret the answer in terms of the domain.

A query is a way of asking whether a proposition is a logical consequence of a knowledge base. Once the system has been provided with a knowledge base, a query is used to ask whether a proposition is a logical consequence of the knowledge base. Queries have the form

ask b.

where b is an atom or a conjunction of atoms (analogous to the body of a rule).

A query is a question that has the answer yes if the body is a logical consequence of the knowledge base, or the answer no if the body is not a consequence of the knowledge base. The latter does not mean that body is false in the intended interpretation but rather that it is impossible to determine whether it is true or false based on the knowledge provided.

Example 5.9.

Once the computer has been told the knowledge base of Example 5.8, it can answer queries such as

       ask light_l1.

for which the answer is yes. The query

       ask light_l6.

has answer no. The computer does not have enough information to know whether or not l6 is a light. The query

       ask lit_l2.

has answer yes. This atom is true in all models.

The user can interpret this answer with respect to the intended interpretation.

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 the 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 the 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 can be used to prove 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.10.

Given the knowledge base KB:


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


The algorithm terminates with C={a,b,c,e,d}. Thus, KBa, KBb, 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:


The bottom-up proof procedure is sound. 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 the 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 a1,,am 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 are 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.


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.


The bottom-up proof procedure is sound. 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 backwards 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 as refining an answer clause of the form


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

ask q1qm

then the initial answer clause is


Given an answer clause yesa1a2am, the top-down algorithm selects an atom in the body of the answer clause. Suppose it selects the leftmost atom, 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.

Suppose the chosen clause is a1b1bp.

The resolvent of the answer clause yesa1a2am with the definite clause a1b1bp is the answer clause


That is, an atom is replaced by the body of a definite clause with that atom in the head.

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 “ask 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 γi1 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 (list or set) G of atoms to prove. Each atom that must be proved is a subgoal. Initially, G contains the atoms in the query. A clause ab1bp means  a can be replaced by b1,,bp. The query is proved when G becomes empty.

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 it 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, used by the language Prolog, is to have G as a list of atoms, in which case duplicates are not eliminated, as they would be if G were a set. In Prolog, the order of the atoms is defined by the programmer. It does not have the overhead of checking for duplicates, which is needed for maintaining a set.

Example 5.11.

The system is given the knowledge base of Example 5.10:


It is asked the query

ask a.

The following shows a derivation that corresponds to a sequence of assignments to G in the repeat loop of Figure 5.4, where the leftmost atom in the body is selected:

Answer ClauseResolved withyesaabcyesbcbdeyesdecdyeseceyescceyeseeyes

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

Answer ClauseResolved withyesaabcyesbcbgeyesgec

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

Note the use of select and choose (see 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. Given a selection strategy, the algorithm 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.12.

Given the knowledge base


and the query

ask ad.

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

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.

Any of the search methods of Chapter 3 can be used to search the search space. The search space depends on the query and which atom is selected at each node. Whether the query is a logical consequence does not depend on the path found, so an optimal path is not necessary.

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.13.

Consider the knowledge base


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, trying to prove g, 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.