5.5 Proving by Contradiction

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 a,A, 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 {a,{a}:a is assumable}. Clauses can be used to derive new conclusions. If there is a clause hb1bm such that for each bi there is some Ai such that bi,AiC, then h,A1Am can be added to C. Note that this covers the case of atomic clauses, with m=0, where h,{} is added to C.

1:procedure Prove_conflict_BU(KB,Assumables)
2:      Inputs
3:            KB: a set of Horn clauses
4:            Assumables: a set of atoms that can be assumed       
5:      Output
6:            set of conflicts
7:      Local
8:            C is a set of pairs of an atom and a set of assumables       
9:      C:={a,{a}:a is assumable}
10:      repeat
11:            select clause “hb1bm” in KB such that
12:            bi,AiC for all i and
13:            h,AC where A=A1Am
14:            C:=C{h,A}
15:      until no more selections are possible
16:      return {A:false,AC}
Figure 5.9: Bottom-up proof procedure for computing conflicts

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 false,A is generated, the assumptions A form a conflict.

One refinement of this program is to prune supersets of assumptions. If a,A1 and a,A2 are in C, where A1A2, then a,A2 can be removed from C or not added to C. There is no reason to use the extra assumptions to imply a. Similarly, if false,A1 and a,A2 are in C, where A1A2, then a,A2 can be removed from C because A1 and any superset – including A2 – 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

{ok_l1,{ok_l1},ok_l2,{ok_l2},ok_s1,{ok_s1},ok_s2,{ok_s2},
    ok_s3,{ok_s3},ok_cb1,{ok_cb1},ok_cb2,{ok_cb2}}.

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

live_outside,{}
live_w5,{}
live_w3,{ok_cb1}
up_s3,{}
live_w4,{ok_cb1,ok_s3}
live_l2,{ok_cb1,ok_s3}
light_l2,{}
lit_l2,{ok_cb1,ok_s3,ok_l2}
dark_l2,{}
𝑓𝑎𝑙𝑠𝑒,{ok_cb1,ok_s3,ok_l2}.

Thus, the knowledge base entails

¬ok_cb1¬ok_s3¬ok_l2.

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.

1:non-deterministic procedure Prove_conflict_TD(KB,Assumables)
2:      Inputs
3:            KB: a set Horn clauses
4:            Assumables: a set of atoms that can be assumed       
5:      Output
6:            A conflict
7:      Local
8:            G is a set of atoms (that implies false)       
9:      G:={false}
10:      repeat
11:            select an atom a in G such that aAssumables
12:            choose clause “aB” in KB with a as head
13:            G:=(G{a})B
14:      until  GAssumables
15:      return G
Figure 5.10: Top-down Horn clause interpreter to find conflicts

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:

{𝑓𝑎𝑙𝑠𝑒}
{dark_l1,lit_l1}
{lit_l1}
{light_l1,live_l1,ok_l1}
{live_l1,ok_l1}
{live_w0,ok_l1}
{live_w1,up_s2,ok_s2,ok_l1}
{live_w3,up_s1,ok_s1,up_s2,ok_s2,ok_l1}
{live_w5,ok_cb1,up_s1,ok_s1,up_s2,ok_s2,ok_l1}
{live_outside,ok_cb1,up_s1,ok_s1,up_s2,ok_s2,ok_l1}
{ok_cb1,up_s1,ok_s1,up_s2,ok_s2,ok_l1}
{ok_cb1,ok_s1,up_s2,ok_s2,ok_l1}
{ok_cb1,ok_s1,ok_s2,ok_l1}.

The set {ok_cb1,ok_s1,ok_s2,ok_l1} is returned as a conflict. Different choices of the clause to use can lead to another answer.