5.5.4 Reasoning with Assumptions and Horn Clauses

This section presents a bottom-up implementation and a top-down implementation for finding conflicts in Horn clause knowledge bases.

Bottom-Up Implementation

The bottom-up implementation is an augmented version of the bottom-up algorithm for definite clauses presented in Section 5.3.2.

The modification to that algorithm is that the conclusions are pairs $\left$, where $a$ is an atom and $A$ is a set of assumables that imply $a$ in the context of Horn clause knowledge base KB.

Initially, the conclusion set $C$ is $\{\left:a\hbox{ is assumable}\}$. Clauses can be used to derive new conclusions. If there is a clause $h\leftarrow\mbox{}b_{1}\wedge\mbox{}\ldots\wedge\mbox{}b_{m}$ such that for each $b_{i}$ there is some $A_{i}$ such that $\left\in C$, then $\left$ can be added to $C$. Note that this covers the case of atomic clauses, with $m=0$, where $\left$ is added to $C$.

Figure 5.9 gives code for the algorithm. This algorithm is sometimes called an assumption-based truth maintenance system (ATMS), particularly when it is combined with the incremental addition of clauses and assumables.

When the pair $\left<\mbox{false},A\right>$ is generated, the assumptions $A$ form a conflict.

One refinement of this program is to prune supersets of assumptions. If $\left$ and $\left$ are in $C$, where $A_{1}\subset A_{2}$, then $\left$ can be removed from $C$ or not added to $C$. There is no reason to use the extra assumptions to imply $a$. Similarly, if $\left<\mbox{false},A_{1}\right>$ and $\left$ are in $C$, where $A_{1}\subseteq A_{2}$, then $\left$ can be removed from $C$ because $A_{1}$ and any superset – including $A_{2}$ – are inconsistent with the clauses given, and so nothing more can be learned from considering such sets of assumables.

Example 5.25.

Consider the axiomatization of Figure 5.8, discussed in Example 5.23.

Initially, in the algorithm of Figure 5.9, $C$ has the value

 $\displaystyle{\{\left<\mbox{ok\_l}_{1},\{\mbox{ok\_l}_{1}\}\right>,\left<\mbox% {ok\_l}_{2},\{\mbox{ok\_l}_{2}\}\right>,\left<\mbox{ok\_s}_{1},\{\mbox{ok\_s}_% {1}\}\right>,\left<\mbox{ok\_s}_{2},\{\mbox{ok\_s}_{2}\}\right>,}$ $\displaystyle\ \ \ \ {\left<\mbox{ok\_s}_{3},\{\mbox{ok\_s}_{3}\}\right>,\left% <\mbox{ok\_cb}_{1},\{\mbox{ok\_cb}_{1}\}\right>,\left<\mbox{ok\_cb}_{2},\{% \mbox{ok\_cb}_{2}\}\right>\}.}$

The following shows a sequence of values added to $C$ under one sequence of selections:

 $\displaystyle{{\left<\mbox{live\_outside},\{\}\right>}}$ $\displaystyle{{\left<\mbox{live\_w}_{5},\{\}\right>}}$ $\displaystyle{{\left<\mbox{live\_w}_{3},\{\mbox{ok\_cb}_{1}\}\right>}}$ $\displaystyle{{\left<\mbox{up\_s}_{3},\{\}\right>}}$ $\displaystyle{{\left<\mbox{live\_w}_{4},\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{3}\}% \right>}}$ $\displaystyle{{\left<\mbox{live\_l}_{2},\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{3}\}% \right>}}$ $\displaystyle{{\left<\mbox{light\_l}_{2},\{\}\right>}}$ $\displaystyle{{\left<\mbox{lit\_l}_{2},\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{3},% \mbox{ok\_l}_{2}\}\right>}}$ $\displaystyle{{\left<\mbox{dark\_l}_{2},\{\}\right>}}$ $\displaystyle{{\left<\mbox{false},\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{3},\mbox{% ok\_l}_{2}\}\right>.}}$

Thus, the knowledge base entails

 $\displaystyle{\neg\mbox{ok\_cb}_{1}\vee\neg\mbox{ok\_s}_{3}\vee\neg\mbox{ok\_l% }_{2}.}$

The other conflict can be found by continuing the algorithm.

Top-Down Implementation

The top-down implementation is similar to the top-down definite clause interpreter described in Figure 5.4, except the top-level query is to prove false, and the assumables encountered in a proof are not proved but collected.

The algorithm is shown in Figure 5.10. Different choices can lead to different conflicts being found. If no choices are available, the algorithm fails.

Example 5.26.

Consider the representation of the circuit in Example 5.23. The following is a sequence of the values of $G$ for one sequence of selections and choices that leads to a conflict:

 $\displaystyle{\{\mbox{false}\}}$ $\displaystyle{\{\mbox{dark\_l}_{1},\mbox{lit\_l}_{1}\}}$ $\displaystyle{\{\mbox{lit\_l}_{1}\}}$ $\displaystyle{\{\mbox{light\_l}_{1},\mbox{live\_l}_{1},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_l}_{1},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_w}_{0},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_w}_{1},\mbox{up\_s}_{2},\mbox{ok\_s}_{2},\mbox{ok% \_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_w}_{3},\mbox{up\_s}_{1},\mbox{ok\_s}_{1},\mbox{up% \_s}_{2},\mbox{ok\_s}_{2},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_w}_{5},\mbox{ok\_cb}_{1},\mbox{up\_s}_{1},\mbox{ok% \_s}_{1},\mbox{up\_s}_{2},\mbox{ok\_s}_{2},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{live\_outside},\mbox{ok\_cb}_{1},\mbox{up\_s}_{1},\mbox{% ok\_s}_{1},\mbox{up\_s}_{2},\mbox{ok\_s}_{2},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{ok\_cb}_{1},\mbox{up\_s}_{1},\mbox{ok\_s}_{1},\mbox{up\_% s}_{2},\mbox{ok\_s}_{2},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{1},\mbox{up\_s}_{2},\mbox{ok\_% s}_{2},\mbox{ok\_l}_{1}\}}$ $\displaystyle{\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{1},\mbox{ok\_s}_{2},\mbox{ok\_% l}_{1}\}.}$

The set $\{\mbox{ok\_cb}_{1},\mbox{ok\_s}_{1},\mbox{ok\_s}_{2},\mbox{ok\_l}_{1}\}$ is returned as a conflict. Different choices of the clause to use can lead to another answer.