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 , 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 . Clauses can be used to derive new conclusions. If there is a clause $h\leftarrow b_1\wedge \mathrm{\dots }\wedge b_m$ such that for each $b_i$ there is some $A_i$ such that , then can be added to $C$. Note that this covers the case of atomic clauses, with $m=0$, where 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 is generated, the assumptions $A$ form a conflict.

One refinement of this program is to prune supersets of assumptions. If and are in $C$, where $A_1\subset A_2$, then can be removed from $C$ or not added to $C$. There is no reason to use the extra assumptions to imply $a$. Similarly, if and are in $C$, where $A_1\subseteq A_2$, then 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.

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.