foundations of computational agents
This section presents a bottom-up implementation and a top-down implementation for finding conflicts in Horn clause knowledge bases.
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 is an atom and is a set of assumables that imply in the context of Horn clause knowledge base KB.
Initially, the conclusion set is . Clauses can be used to derive new conclusions. If there is a clause such that for each there is some such that , then can be added to . Note that this covers the case of atomic clauses, with , where is added to .
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 form a conflict.
One refinement of this program is to prune supersets of assumptions. If and are in , where , then can be removed from or not added to . There is no reason to use the extra assumptions to imply . Similarly, if and are in , where , then can be removed from because and any superset – including – are inconsistent with the clauses given, and so nothing more can be learned from considering such sets of assumables.
Initially, in the algorithm of Figure 5.9, has the value
The following shows a sequence of values added to under one sequence of selections:
Thus, the knowledge base entails
The other conflict can be found by continuing the algorithm.
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.
Consider the representation of the circuit in Example 5.23. The following is a sequence of the values of for one sequence of selections and choices that leads to a conflict:
The set is returned as a conflict. Different choices of the clause to use can lead to another answer.