# 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

 $h\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}.$

where $h$ is an atom, the head of the clause, and each $a_{i}$ is an atom. It can be read “$h$ if $a_{1}$ and …and $a_{m}$”.

If $m>0$, the clause is called a rule, where $a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}$ 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:

 $\neg{apple\_is\_eaten}.$ ${apple\_is\_eaten}\wedge\mbox{}{bird\_eats\_apple}.$ ${sam\_is\_in\_room}\wedge\mbox{}{night\_time}\leftarrow\mbox{}{switch\_1\_is\_% up}.$ ${Apple\_is\_eaten}\leftarrow\mbox{}{Bird\_eats\_apple}.$ ${happy}\vee{sad}\vee\neg{alive}.$

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

A definite clause $h\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}$ is false in interpretation $I$ if $a_{1},\dots,a_{m}$ 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

 $a\leftarrow\mbox{}b\wedge\mbox{}c\wedge\mbox{}d$

is equivalent to the clause

 $a\vee\neg b\vee\neg c\vee\neg d.$

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., $a\vee\mbox{}b$) or disjunctions of negated atoms (e.g., $\neg c\vee\mbox{}\neg d$).

###### 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\_s}_{2}$ is true when switch $s_{2}$ is up. ${ok\_l}_{1}$ is true when light $l_{1}$ is working properly (will be lit if it is has power coming into it). ${live\_w}_{1}$ is true when $w_{1}$ 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

 $\begin{array}[]{lll}{{light\_l}_{1}.{}{}{}{}{}}&{{light\_l}_{2}.{}{}{}{}{}}&{{% ok\_l}_{1}.}\\ {{ok\_l}_{2}.}&{{ok\_cb}_{1}.}&{{ok\_cb}_{2}.}\\ {{live\_outside}.}\end{array}$

The designer may look at part of the domain and know that light $l_{1}$ is live if wire $w_{0}$ is live, because they are connected together, but may not know whether $w_{0}$ is live. Such knowledge is expressible in terms of rules:

 $\begin{array}[]{ll}{{live\_l}_{1}\leftarrow\mbox{}{live\_w}_{0}.}&{{live\_p}_{% 1}\leftarrow\mbox{}{live\_w}_{3}.}\\ {{live\_w}_{0}\leftarrow\mbox{}{live\_w}_{1}\wedge\mbox{}{up\_s}_{2}.}&{{live% \_w}_{3}\leftarrow\mbox{}{live\_w}_{5}\wedge\mbox{}{ok\_cb}_{1}.}\\ {{live\_w}_{0}\leftarrow\mbox{}{live\_w}_{2}\wedge\mbox{}{down\_s}_{2}.{}{}{}{% }{}{}}&{{live\_p}_{2}\leftarrow\mbox{}{live\_w}_{6}.}\\ {{live\_w}_{1}\leftarrow\mbox{}{live\_w}_{3}\wedge\mbox{}{up\_s}_{1}.}&{{live% \_w}_{6}\leftarrow\mbox{}{live\_w}_{5}\wedge\mbox{}{ok\_cb}_{2}.}\\ {{live\_w}_{2}\leftarrow\mbox{}{live\_w}_{3}\wedge\mbox{}{down\_s}_{1}.}&{{% live\_w}_{5}\leftarrow\mbox{}{live\_outside}.}\\ {{live\_l}_{2}\leftarrow\mbox{}{live\_w}_{4}.}&{{lit\_l}_{1}\leftarrow\mbox{}{% light\_l}_{1}\wedge\mbox{}{live\_l}_{1}\wedge\mbox{}{ok\_l}_{1}.}\\ {{live\_w}_{4}\leftarrow\mbox{}{live\_w}_{3}\wedge\mbox{}{up\_s}_{3}.}&{{lit\_% l}_{2}\leftarrow\mbox{}{light\_l}_{2}\wedge\mbox{}{live\_l}_{2}\wedge\mbox{}{% ok\_l}_{2}.}\end{array}$

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

 ${{down\_s}_{1}.}~{}~{}~{}~{}~{}{{up\_s}_{2}.}~{}~{}~{}~{}~{}{{up\_s}_{3}.}$

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

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\_s}_{3}$ 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

 $\mbox{{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

 $\mbox{{ask}~{}}~{}{light\_l}_{1}.$

for which the answer is yes. The query

 $\mbox{{ask}~{}}~{}{light\_l}_{6}.$

has answer no. The computer does not have enough information to know whether or not $l_{6}$ is a light. The query

 $\mbox{{ask}~{}}~{}{lit\_l}_{2}.$

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 $\models$ 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, ${KB}\vdash g$ 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 ${KB}\vdash g$, then ${KB}\models g$.

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 ${KB}\models g$, then ${KB}\vdash g$.

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 “$h\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}$” is a definite clause in the knowledge base, and each $a_{i}$ 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.

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, ${KB}\vdash g$ if $g\in C$ at the end of the ${Prove\_DC\_BU}$ procedure. For a conjunction, ${KB}\vdash g_{1}\land\dots\land g_{k}$, if $\{g_{1},\dots,g_{k}\}\subseteq C$.

###### Example 5.10.

Given the knowledge base ${KB}$:

 $\begin{array}[]{ll}{a\leftarrow\mbox{}b\wedge\mbox{}c.{}{}{}{}{}}&{d.}\\ {b\leftarrow\mbox{}d\wedge\mbox{}e.}&{e.}\\ {b\leftarrow\mbox{}g\wedge\mbox{}e.}&{f\leftarrow\mbox{}a\wedge\mbox{}g.}\\ {c\leftarrow\mbox{}e.}\end{array}$

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, ${KB}\vdash a$, ${KB}\vdash 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

The bottom-up proof procedure is sound. Every atom in $C$ is a logical consequence of ${KB}$. That is, if ${KB}\vdash g$ then ${KB}\models g$. 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 $h\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}$ such that $a_{1},\ldots,a_{m}$ 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 $a_{i}$ are generated before $h$, all of the $a_{i}$ 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}$.

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 “$h\leftarrow\mbox{}a_{1}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}\hbox{''}\in{KB}$ is false in $I$. The only way this could occur is if $a_{1},\ldots,a_{m}$ 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

The bottom-up proof procedure is sound. Suppose ${KB}\models g$. 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 ${KB}\vdash g$.

### 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

 ${yes}\leftarrow\mbox{}a_{1}\wedge\mbox{}a_{2}\wedge\mbox{}\ldots\wedge\mbox{}a% _{m}$

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

 $\mbox{{ask}~{}}~{}q_{1}\wedge\mbox{}\dots\wedge\mbox{}q_{m}$

then the initial answer clause is

 ${yes}\leftarrow\mbox{}q_{1}\wedge\mbox{}\dots\wedge\mbox{}q_{m}.$

Given an answer clause ${yes}\leftarrow\mbox{}a_{1}\wedge\mbox{}a_{2}\wedge\mbox{}\ldots\wedge\mbox{}a% _{m}$, the top-down algorithm selects an atom in the body of the answer clause. Suppose it selects the leftmost atom, $a_{1}$. 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 $a_{1}$ as the head. If there is no such clause, the algorithm fails.

Suppose the chosen clause is $a_{1}\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{p}$.

The resolvent of the answer clause ${yes}\leftarrow\mbox{}a_{1}\wedge\mbox{}a_{2}\wedge\mbox{}\ldots\wedge\mbox{}a% _{m}$ with the definite clause $a_{1}\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{p}$ is the answer clause

 ${yes}\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{p}\wedge\mbox{}a% _{2}\wedge\mbox{}\ldots\wedge\mbox{}a_{m}.$

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}\leftarrow\mbox{}{}$.

An SLD derivation of a query “$\mbox{{ask}~{}}~{}q_{1}\wedge\mbox{}\ldots\wedge\mbox{}q_{k}$” from knowledge base ${KB}$ is a sequence of answer clauses $\gamma_{0},\gamma_{1},\ldots,\gamma_{n}$ such that:

• $\gamma_{0}$ is the answer clause corresponding to the original query, namely the answer clause ${yes}\leftarrow\mbox{}q_{1}\wedge\mbox{}\ldots\wedge\mbox{}q_{k}$

• $\gamma_{i}$ is the resolvent of $\gamma_{i-1}$ with a definite clause in ${KB}$

• $\gamma_{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 $a\leftarrow\mbox{}b_{1}\wedge\mbox{}\dots\wedge\mbox{}b_{p}$ means  $a$ can be replaced by $b_{1},\dots,b_{p}$. The query is proved when $G$ becomes empty.

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:

 $\begin{array}[]{ll}{a\leftarrow\mbox{}b\wedge\mbox{}c.{}{}{}{}{}}&{d.}\\ {b\leftarrow\mbox{}d\wedge\mbox{}e.}&{e.}\\ {b\leftarrow\mbox{}g\wedge\mbox{}e.}&{f\leftarrow\mbox{}a\wedge\mbox{}g.}\\ {c\leftarrow\mbox{}e.}\end{array}$

 $\mbox{{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:

 $\begin{array}[]{ll}\mbox{Answer Clause}&\mbox{Resolved with}\\ \hline\cr{{yes}\leftarrow\mbox{}a}&a\leftarrow\mbox{}b\wedge\mbox{}c\\ {{yes}\leftarrow\mbox{}b\wedge\mbox{}c}&b\leftarrow\mbox{}d\wedge\mbox{}e\\ {{yes}\leftarrow\mbox{}d\wedge\mbox{}e\wedge\mbox{}c}&d\\ {{yes}\leftarrow\mbox{}e\wedge\mbox{}c}&e\\ {{yes}\leftarrow\mbox{}c}&c\leftarrow\mbox{}e\\ {{yes}\leftarrow\mbox{}e}&e\\ {{yes}\leftarrow\mbox{}}&\end{array}$

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

 $\begin{array}[]{ll}\mbox{Answer Clause}&\mbox{Resolved with}\\ \hline\cr{{yes}\leftarrow\mbox{}a}&a\leftarrow\mbox{}b\wedge\mbox{}c\\ {{yes}\leftarrow\mbox{}b\wedge\mbox{}c}&b\leftarrow\mbox{}g\wedge\mbox{}e\\ {{yes}\leftarrow\mbox{}g\wedge\mbox{}e\wedge\mbox{}c}\end{array}$

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 ${yes}\leftarrow\mbox{}a_{1}\wedge\mbox{}\dots\wedge\mbox{}a_{m}$, where $a_{1}$ is the selected atom, represent all of the possible answer clauses obtained by resolving on $a_{1}$. There is a neighbor for each definite clause whose head is $a_{1}$. The goal nodes of the search are of the form ${yes}\leftarrow\mbox{}$.

###### Example 5.12.

Given the knowledge base

 $\begin{array}[]{lll}a\leftarrow\mbox{}b\land c.{}{}{}{}&a\leftarrow\mbox{}g.{}% {}{}{}&a\leftarrow\mbox{}h.\\ b\leftarrow\mbox{}j.&b\leftarrow\mbox{}k.&d\leftarrow\mbox{}m.\\ d\leftarrow\mbox{}p.&f\leftarrow\mbox{}m.&f\leftarrow\mbox{}p.\\ g\leftarrow\mbox{}m.&g\leftarrow\mbox{}f.&k\leftarrow\mbox{}m.\\ h\leftarrow\mbox{}m.&p.\end{array}$

and the query

 $\mbox{{ask}~{}}~{}a\wedge\mbox{}d.$

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

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

 $\begin{array}[]{ll}{g\leftarrow\mbox{}a.{}{}{}{}{}}&{a\leftarrow\mbox{}b.}\\ {g\leftarrow\mbox{}c.}&{b\leftarrow\mbox{}a.}\\ {c.}\end{array}$

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 $a_{1}$ 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.