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 “$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, $\text{KB}⊢g$ if $g\in C$ at the end of the Prove_DC_BU procedure. For a conjunction, $\text{KB}⊢g_1\wedge \mathrm{\dots }\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

Every atom in $C$ is a logical consequence of KB. That is, if $\text{KB}⊢g$ then $\text{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 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$ 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 \text{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

Suppose $\text{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 $\text{KB}⊢g$.

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

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

the initial answer clause is

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

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 $a_1$ with the definite clause

is the answer clause

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

An SLD derivation of a query “$\text{𝖺𝗌𝗄}{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 $\text{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 $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 $a\leftarrow b_1\wedge \mathrm{\dots }\wedge b_p$ means subgoal $a$ can be replaced by subgoals $b_1,\mathrm{\dots },b_p$. The $G$ to be proved corresponds to the answer clause $\text{yes}\leftarrow G$.

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.

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 $\text{yes}\leftarrow a_1\wedge \mathrm{\dots }\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 $\text{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. 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).

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.