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