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 a_1\wedge \mathrm{\dots }\wedge 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⊢g$ if $g\in C$ at the end of the $Prove\mathrm{\_}DC\mathrm{\_}BU$ procedure. For a conjunction, $KB⊢g_1\wedge \mathrm{\cdots }\wedge g_k$, if $\{g_1,\mathrm{\dots },g_k\}\subseteq C$.

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⊢g$ then $KB\vDash 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 a_1\wedge \mathrm{\dots }\wedge a_m$ such that $a_1,\mathrm{\dots },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 a_1\wedge \mathrm{\dots }\wedge a_m\text{”}\in KB$ is false in $I$. The only way this could occur is if $a_1,\mathrm{\dots },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\vDash 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⊢g$.

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

then the initial answer clause is

Given an answer clause $yes\leftarrow a_1\wedge a_2\wedge \mathrm{\dots }\wedge 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 b_1\wedge \mathrm{\dots }\wedge b_p$.

The resolvent of the answer clause $yes\leftarrow a_1\wedge a_2\wedge \mathrm{\dots }\wedge a_m$ with the definite clause $a_1\leftarrow b_1\wedge \mathrm{\dots }\wedge b_p$ 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\leftarrow$.

An SLD derivation of a query “$\text{ask}{q}_1\wedge \mathrm{\dots }\wedge q_k$” from knowledge base $KB$ is a sequence of answer clauses ${\gamma }_0,{\gamma }_1,\mathrm{\dots },{\gamma }_n$ such that:

• •

  ${\gamma }_0$ is the answer clause corresponding to the original query, namely the answer clause $yes\leftarrow q_1\wedge \mathrm{\dots }\wedge 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 b_1\wedge \mathrm{\cdots }\wedge b_p$ means  $a$ can be replaced by $b_1,\mathrm{\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.

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 a_1\wedge \mathrm{\cdots }\wedge 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$.

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

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.