A Correct Non-Monotonic ATMS

1. Introduction

Reason maintenance systems can be applied to capture special phenomena occurring in non-monotonic reasoning. E.g. Doyle's TMS [Doyle, 1979] handles exceptions properly. On the other hand, the multiple context facility of de Kleer's ATMS [de Kleer, 1986a] may be used to deal with ambiguity in the presence of inconsistencies. However, none of these systems is suitable for non-monotonic reasoning in general. Let us consider some examples that demonstrate the advantages and limits of reason maintenance techniques. For this purpose we use Reiter's default logic (DL) [Reiter, 1980] because it is powerful enough to illustrate all problems. On the other hand, it is simple enough to relate its concepts and reason maintenance constructs1 .

Example 1: (the familiar Nixon example)

As usual, quakers typically are doves and republicans normally are hawks. Nobody can be a hawk and a dove, but

1 We write (a: Mbi; ... ;Mt>Wc) for Reiter's defaults, (a 1 , ...· 1lJclc) for inference rules, a 1·· .. ,ak -+ c for monotonic justifications, and (SL c (a1 ... ak) (o1 .. . oj)) for Doyle's non-monotonic justifications.

REPUBUCAN, ( REPUBUCAN : MHA WK I HAWK), QUAKER, (QUAKER : MDOVE I DOVE), DOVE & HAWK::::> FALSE

There are two extensions of this default theory: One contains DOVE and -,HAWK, the other one -,DOVE and HAWK. First, we want to determine these extensions using the ATMS. Following [Dressler, 1988a] and [Junker, 1988], we can translate a default (a: Mbl b) into a monotonic justification a, out(-,b) ~ b and an assumption out(-,b). DL premises are also A TMS premises. Furthermore, assume that modus ponens is applied and that every inference step is protocolled by an A TMS justification. Then, we obtain:

justifications:

assumptions:

no goods:

maximal consistent

assumption sets:

REPUBUCAN, out(-,HA WK) ~HAWK QUAKER, out(.OOVE) ~DOVE DOVE, HAWK~ FALSE out( -,DOVE), out( oHA WK) ({out( -,DOVE), out(-,HAWK)})

(out( -,DOVE)}, (out( -,HAWK)}

In this case, every maximal consistent assumption set corresponds to an extension (and vice versa). Therefore, ATMS may be used for normal defaults (whose prerequisites are theorems of premises). In contrast to Doyle's TMS it finds all extensions. However, there are examples where Doyle's system is superior to ATMS:

Example 2: (working example)

On workdays, Peter must normally go to work. This is not true, if he has an excuse. If he is ill he normally has an excuse. However, his employer does not accept this if Peter has only caught a cold. Hence, there is an exception of an exception! Now, assume that Peter is ill on a workday. What happens? Again, we formalize this story using simplified defaults:

WORKDAY,

ILL,

COLD::::>ILL

(WORKDAY: M-,EXCUSE I WORK),

( ILL: M.COLD I EXCUSE)

There exists only one extension that contains EXCUSE, but not WORK. If we use Doyle's TMS to compute this extension, we obtain two non-monotonic justifications:

(SL WORK (WORKDAY) ( EXCUSE) ),

(SL EXCUSE (ILL) (COLD))

WORKDAY and ll..L are labelled with IN because they are premises. COLD is labelled with OUT because it has no justification at all. Then, EXCUSE gets IN and the only justification for WORK is invalid. Therefore, WORK is labelled with OUT just as we expected. Figure 1 shows the complete labelling using Goodwin's notation [Goodwin, 1987].

However, if we apply the ATMS we get in trouble. In addition to example 1, we use extra consistency rules to ensure that no context contains out(x) and x:

Astonishingly, there are two maximal consistent assumption sets. One, namely {out( COLD)}, corresponds to the extension mentioned above. However, also the set { out(EXCUSE)} which infers WORK is consistent! The A TMS detects the conflict between both conflicing defaults, but it does not know anything about priorities between interacting defaults. Expressions like out( COLD) are simple assumptions. Reasons for such expressions are ignored. The same problem arises if we apply de Kleer' s original encoding of non-monotonic justifications [de Kleer, 1986b]. The TMS, however, uses a special rule to label a node with out:

If all justifications of a node x are invalid label x with our.

To sum up, both reason maintenance systems are restricted to special cases: A TMS is suitable for normal defaults, but gets in trouble with exceptions of exceptions. Doyle's TMS works correctly if the default theory is stratified or acyclic (i.e. the justification network contains no non-monotonic odd or even loop). Then the existence of a unique extension is guaranteed. If there are even loops there may be different extensions, but the TMS finds only one. If there are odd loops a TMS may enter an endless loop [Doyle, 1979] or stop without defmite result [Goodwin, 1987].

In the sequel, we develop a hybrid reason maintenance system that benefits from advantages of the ATMS and the TMS and overcomes their limitations. We use the ATMS as a basic system that records the applications of nonmonotonic or monotonic rules in different contexts. However, not all assumption sets occurring in A TMS labels are valid in the sense that they describe a subset of any extension. Therefore, a separate test algorithm is needed that takes account of exceptions. For this purpose we adapt Doyle's Out-labelling rule mentioned above. We also want to verify the resulting system. Therefore we need a suitable specification of non-monotonic reasoning. Again, we choose Reiter's default logic.

2. Theoretical Considerations

In this section, we develop the theoretical framework for realizing non-monotonic reasoning using the A TMS. First of all, we consider Reiter's definition of a default logic extension. ·

Definition 1: Let ..:1 = (D,W) be a closed default theory (Dis a set of defaults and W is a set of first-order formulas). An extension of ..:1 is a fixpoint of an operator r that is defined as follows : Let S be an arbitrary set of first-order formulas. Then l(S) is the smallest set such that

1. T(S) contains W
2. l(S) is closed with respect to first order derivability
3. if (a:MbJ; ... ;Mbnlc) ED, a E l(S), -,bi ~ S then c E l(S).

Can we determine r(S) using a monotonic reasoner for multiple contexts? At least, the definition of r resembles the usual definition of a closure of a monotonic inference system: Let I = (L, AX, R) be an arbitrary monotonic inference system (L is a formal language, AX is a set of axioms, and R contains inference rules). The closure Thi of a subset P of L can be defined by: ThJ{P) is the smallest set such that:

1. ThJ(P) contains AX and P
2. if (a] , ... ,ak I c) E Rand a; E ThJ(P) then c E ThJ(P).

Both definitions mainly differ in the condition -.bi e S used in (3). In the monotonic case, we don't ask whether a formula is not contained in a set. Fortunately, this unusual condition only refers to S, not to r(S). We can introduce additional expressions of the form out(-.bi) for -.bi e S. Furthermore, we replace S by a corresponding set A(S) containing such out-expressions. Then we ask out(-.bi) E ThJ(A(S)) instead of -.bi e S. Let 0 be the set of all out­ expressions needed for any default of D. Then A(S) must contain out(x) if and only if S does not contain x:

There is another difference between both definitions. (2) requires completeness with respect to first-order derivability. Therefore, we need a complete and sound inference system for first-order derivability. Later, we will restrict the first­ order language to hom clauses and consider only derivability of atomic formulas. Then modus ponens will be sufficient to achieve (2).

Now, let L be a first-order language and~= (D,W) be a closed default theory using L. Furthermore, let LI = (L, AX, R) be a complete inference system for first-order derivability in L. We extend this inference system to obtain a tool for determining r(S). We add the premises of W as axioms and translate every default of D into an inference rule as follows. We apply a default (a:Mb1; ... ;MbtJc) and derivec if we infer a, out( -.b1), ... ,out( -.btc):

Then we obtain a new inference system DI := (L v 0, AX v W, R v MD). Because we are not interested in derivation of out-expressions we modify the closure Thm of DI slightly: Let A be a set of out-expressions. Then Th(A):= ThDJ(A) nL. Now, we can formulate the first result:

Theorem 1: Let S be a set of first-order formulas. Then T'(S) = Th( A(S))

Proof: in [Junker, 1988]

Thus, we are able to determine r(S) using a monotonic reasoner if A(S) is specified. However, we are only interested in fix points of r. Is there a simple criterion that decides which assumption sets correspond to extensions? A fixpoint S satisfies: S = r(S) = Th(A(S)). Then an assumption out(x) is contained in A(S) if and only if x is not contained in S = Th(A(S)). Therefore we defme:

Definition 2: A subset A of 0 is an extension base iff for every out(x) E 0 either out(x) E A or x E Th(A) (not both!).

We already know that this criterion is a necessary condition for an assumption set obtained from a fixpoint S. Is it also a sufficient condition for a fixpoint ? Assume that A is an extension base. Then out(x) is contained in A if and only if x e Th(A) if and only if out(x) E A(Th(A)). Since every out-expression satisfies this fact the sets A and A(Th(A)) are equal. Hence, Th(A) is an extension because of Th(A) = Th(A(Th(A))) = r(Th(A)). Now, we can summarize:

Theorem 2: If E is an extension then A(E) is an extension base. If A is an extension base then Th(A) is an extension.

We illustrate this result using example 2. We get four cases because there are two out-expressions, namely out(COLD), out(EXCUSE) :

A= 0:

Th(A) = {WORKDAY, ILL, COLD:::::>ILL}

A = { out(EXCUSE)}: Th(A) = Th(0) u {WORK}

A= {out(COLD)}: Th(A) = Th(0) u {EXCUSE}

A= { out(EXCUSE),

out(COLD)}: Th(A) = Th(0) u {EXCUSE, WORK}

In the first and second case, we miss out(COLD) and don't infer COLD. In the last case, we assumed out(EXCUSE) and inferred EXCUSE. Thus, we only obtain an extension base in the third case, where out(COLD) is assumed and EXCUSE is inferred.

3. Which defaults & formulas are needed ?

Because we only want to develop a reason maintenance system we introduce some restrictions concerning the defaults and first-order formulas. First of all, we assume that the number of defaults and premises is finite. In [Doyle, 1979], reason maintenance nodes are viewed as propositional constants. We interpret monotonic justifications of the form

(SL c (a1 ... ak) () ) as propositional implications (or hom clauses). Therefore, we restrict the language L to pro­ positional horn clauses. We use the special symbol FALSE as a consequent of horn clauses without positive literal. In section 4 and 5, we consider only defaults of the form (a:M-.b1 ; ... ;M-.bk/c) where a,b1 , ... ,bk,c are propositional constants. Such defaults correspond to non-monotonic justifications of the form (SL c (a) (bl ... bk)) (cf. [Brewka, 1989]).

Now, it is easy to satisfy the completeness requirement of (2). We are only interested in the derivation of propositional constants. There are two cases: If an assumption set is consistent we need only generalized modus ponens to derive any constant. If an assumption set is inconsistent (i.e. FALSE is derivable) then any formula can be derived. Modus ponens is also sufficient to detect inconsistencies. Besides the set MD, we take only account of inference rules of the form

where a1, ... ,ak are constants and cis a constant or FALSE.

4. Techniques for Multiple Contexts

The results of section 2 are still independent from the ATMS. If we want to determine extensions we must consider a lot of overlapping contexts. Therefore, we can benefit from the facilities of the ATMS. First we translate the concepts of section 2 into the A TMS terminology:

Every premise of the inference system DI is also a premise of ATMS. An out-expression out(x) is added as an assumption to the ATMS. Furthermore, every inference rule (a1 , ... ,ak/ c) mentioned in the paragraph above is trans­ formed into a justification a 1 , ... ,ak ~ c. Now, we can check whether a formula x is contained in Th(A) by inspecting its ATMS-Iabel which is denoted by LABEL(x):

x E Th(A) iff LABEL(x) contains a subset of A or A is inconsistent

Furthermore, we can check the inconsistency of an assumption set by inspecting the set NOGOODS that is maintained by the ATMS and contains all minimal inconsistent assumption sets:

A is inconsistent iff NOGOODS contains a subset of A

However, it is still possible that x is inferred from an assumption set containing out(x). Consider the set {out(EXCUSE), out(COLD)} of the working example where EXCUSE E Th(A) and out(EXCUSE) E A. According to definition 2, this set is no extension base. Even if the default theory is extended by new defaults or premises EXCUSE E Th(A) remains true. Such a set is completely useless. We can use the consistency mechanism of the ATMS to get rid of such sets. Following [Dressler, 1988a], we introduce additional constraints of the form

for every out-expression. Now, assume that a set A containing out(x) infers x. Then it infers FALSE and is handled as a nogood. These additional nogoods do not represent logical inconsistencies, but are also used to get rid of assumption sets that can never become extension bases. Therefore, we call them pruning no goods.

With respect to this extended form of inconsistency, extension bases are maximal consistent assumption sets of the A TMS. If we extend an extension base A by a further assumption out(y) ~ A then y e Th(A u {out(y)}) because of y e Th(A). Normally, an extension base is consistent. Only if FALSE e Th(0)) then there is an inconsistent extension base, namely the empty set:

Lemma 1: If A is a non empty extension base then A is a maximal consistent set of out-expressions. An inconsistent set A is an extension base if and only ifF ALSE E Th( 0) and A=0.

Example 2 shows that there are still maximal consistent sets that are no extension bases (e.g. {out{EXCUSE)}). Therefore, the A TMS techniques are not sufficient

5. Techniques for Exceptions

In a lot of cases, we are not interested in complete extensions, but in a particular formula x. We want to know the extensions containing x. For this purpose, we can inspect the A TMS label of x. It contains minimal sets of out-expressions that infer x, but we don't know whether these sets are contained in any extension base. In example 2, we are interested in the formula WORK the label of which consists of the set { out(EXCUSE)). Then we ask whether this set is valid in the following sense:

Definition 3: A set A of out-expressions is valid if A is contained in any extension base.

How can we check this property? We try to add further out-expressions to A. For every out-expression out(x), we choose out(x) or test whether x can be inferred afterwards. Thus, we obtain a binary search tree and apply a backtracking procedure. In the sequel, we ignore the special case that the empty set is inconsistent. Hence, we drop inconsistent supersets of A. Then we obtain a first version of a test algorithm. We assume that the elements of 0 are ordered in a sequence out(xl), ... ,out(xk)·

Algorithm SLOWTEST

input:

output:

an assumption set A and an optional number i (default value: 1)

true, if there is a consistent extension base E that {out(xi), ... ,out(xk)} uA ;;;JE .:.>A

false, otherwise

jf. NOGOODS contains a subset of A lhm false rlH. jf. i > k and LABEL(x) contains a subset of A

for all out(x) E 0 -A lhm true rlH.

jf. i > k lhfiLfalse rlH.

jf. SLOWIEST(A u{out(xi)J, i+1) lhm true

rlH_ SLOWIEST(A, i+ 1 ).

This algorithm does not handle exceptions efficiently. Consider a long chain consisting of ( :M-,Ai I Ai+ I) where i=l, ... ,k. At worst, SLOWTEST needs 0(2k) steps, while Doyle's TMS finishes after k steps. How does TMS gain this efficiency ? In contrast to SLOWTEST, TMS exploits dependencies between out-assumptions. There are circumstances, where a formula x cannot be derived even if out-assumptions are added. Then we must choose out(x). In section 1, we showed that TMS uses a rule to determine an out-label of a node. We need a corresponding argument for the ATMS-based system.

Can we check whether xi is inferred by a superset of A or not? If A already infers xi we cannot choose out(xi) any more. Otherwise, Xi ~ Th(A). Now, assume that every out­ assumption out(xj) occurring in LABEL{xi) has been considered before out(xi) (i.e. j < i). Then the remaining out-assumptions out(xi), ... ,out(xk) do not contribute to any proof of xi. We summarize this fact after introducing another term: Let PRED{x) := { out(y) e 0 I 3 A e LABEL{x): out(y) e A) be the set of all out-expressions that can be used to prove x. We call members of PRED(x) predecessors of out(x).

Lemma 2: Let A and PRED(xi) be subsets of {out(x1 ), ... ,out(xi-1)}. Let B be a consistent superset of A and a subset of A u {out(xi), ... ,out(xk)}. Then B infers Xi if and only if A infers Xi·

If the prerequisites of lemma 2 are satisfied we can easily check whether we must add or drop out(x). Thus, we can improve SLOWTEST if we order the set of out-expressions in a useful sequence. In example 2, we start with out{COLD) because LABEL{ COLD) and PRED{COLD) are empty. Because out{ COLD) is the only predecessor of out(EXCUSE) we add it and get a complete sequence. Things are not so easy if there are non-monotonic loops. E.g. consider a non-trivial odd loop consisting of three defaults:

Then out{ A) is a predecessor of out{B) which is a predecessor of out{C). However, out{C) is predecessor of out(A). Therefore, we must cut off this loop, choose any assumption e.g. out(A) and investigate two cases. We can generalize this idea:

Definition 4: A cut Cut is a minimal subset of 0 (with respect to set inclusion) such that the elements of 0 can be ordered in a sequence out(x1), ... ,out(xk) that satisfies for all i = 1, ... ,k: out(xi) E Cut or PRED(xi) is a subset of {out( X] ), ... ,out(xi-1 )} .

We can compute such a cut and a sequence using an algorithm with quadratic time complexity. We only determine a cut and a sequence if the A TMS has finished. Mterwards, we can apply a fast modification of SLOWTEST to any assumption set of interest

Algorithm TEST

input:

output:

an assumption set A and an optional number i (default value: 1)

true, if there is a consistent extension base E that {out(xi), ... ,out(xk)} u A.:.> E;:? A false, otherwise

if NOGOODS contains a subset of A lhm false ~ j[ i > k and LABEL(x) contains a subset of A

for all out(x) E Cut- A lhm true ~ if i > k lhm false clH. if out( xi) E A or LABEL( xi) contains a subset of A

lhm TEST(A, i+l) ~ j[ out(xi) ~ Cut lhm TEST(A u {out(xi)J, i+l) t:1..s-'. j[ TEST(A u {out(xi)J, i+l) lhm true ~ TEST(A, i+l).

The improvements of TEST are explained briefly: If out(x) is already contained in A or x is inferred from A we have no choice. Otherwise, if out(x) is no cut assumption, out(x) must be added to A because x cannot derived from A (cf. lemma 2). Only for cut assumptions, we have to consider both cases. If we don't choose a cut assumption out(x) we must check afterwards whether x can be inferred.

Now, we apply TEST to the working example:

input from LABEL( COLD) = 0,

ATMS:

LABEL(EXCUSE) = { {out(COLD))},

sequence:

cut:

NOOOODS = { {out(EXCUSE), out(COLD))) out(COLD), out(EXCUSE)

0

First, we try TEST( { out(EXCUSE)) ). Since COLD cannot be proved the algorithm adds out(COLD) and calls TEST({out(EXCUSE), out(COLD)), 2). Then the first argument is a nogood and TEST returns false. Hence, the single set of the label of WORK is invalid. However, calling TEST( {out( COLD))) results in true: Because out( COLD) is already contained in A, TEST( { out(COLD)), 2) is called immediately. Then we can infer EXCUSE and must not add out(EXCUSE). As there is no cut assumption TEST({out(COLD)), 3) yields true.

In contrast to this stratified example a cut assumption, say out(A), is introduced for the odd loop mentioned above. Then we obtain the sequence out(A), out(B), out(C). If we call TEST(0) we first choose out(A). Then we can proof B and must not add out(B). Hence, we cannot prove c and must add out( C) yielding a nogood, namely { out(A), out(B)). Therefore, we go back and drop out(A). Then we must add out(B) and drop out( C). However, we cannot prove A using { out(B)). Hence, TEST(0) results in false. TEST has detected that there is no extension at all.

In the worst case, the complexity of TEST is O(n * 2m) where n is the number of all out-assumptions and m is the number of cut assumptions or choice points. If there are no non-monotonic loops we can avoid cut assumptions and the complexity reduces to O(n). Otherwise, TEST explores different alternatives if it chooses a wrong assumption of an even loop or runs into an odd loop. Efficiency is strongly influenced by the number of cut members and their ordering.

TEST is a non-incremental algorithm because it presupposes that all proofs for some formulas have been found. That's not so bad because all monotonic inference steps are performed by an incremental system, namely the ATMS. Furthermore, we should only call TEST after the problem solver added all justifications.

6. Dealing with Inconsistencies

We are still not able to handle the Nixon example because we restricted our default language in section 3. What is the special problem of the Nixon example ? Nixon is a dove and a hawk per default. However, the conjunction of both properties implies a logical inconsistency. How can we resolve this inconsistency? In default logic, we just require that the consequent c of a default is consistent by writing (a: M-.b; Me I c). Such an expression is similar to a semi­ normal default. Let (ai: M-.bi; Mci I ci) be some defaults (i=1, ... ,n) whose consequents imply an inconsistency as in the Nixon example. Assume that I= denotes first-order derivability. Then we can select an arbitrary ck and apply the deduction theorem (as in [de Kleer, 1988]):

Then (ak: M-.bk; Mck I ck) is blocked if we apply the other defaults. In this case, there are no implicit priorities between the defaults. Thus, a logical inconsistency can lead to multiple extensions.

Now, we can use defaults of the form (a:M-.bt; ... ;M-.bm; Me I c) to resolve logical inconsistencies. If we translate such a default according to section 2 we obtain an out­ expression out(-.c) and must find all proofs for a negative constant -.c. Are there special techniques to facilitate this task? Can we exploit (*) and start a refutation proof for -.ck?

For this purpose, Doyle's TMS uses dependency-directed backtracking. If TMS detects an inconsistency by labelling FALSE with IN it traces back and finds the non-monotonic justifications underlying the contradiction. As above, it selects an arbitrary justification (SL ck (a) (bl ... bm)) and any bj. Then it justifies bj with (SL bj (C] ... ck-1 Ck+ 1 ... en) (b1 ... bj-1 bj+ 1 ... bm)). Hence, TMS justifies bj instead of -.ck! However, we could slightly change the backtracking procedure if we want to achieve (*).

Can we adapt dependency-directed backtracking to assumption-based techniques? Dressler proposes the following meta rule that inspects nogoods:

Compared with (*), there are some important differences:

Because rule (**) inspects nogoods it refers to out­ expressions instead of consequents of non-monotonic justifications.

Furthermore, we apply (**) to all nogoods while (*) requiresfirst-order-derivability. In our RMS, the translated default rules and constraints of the form x, out(x) ~FALSE do not correspond to first-order inference steps. Especially, if we apply (**) to pruning nogoods our DL-specification "is violated. Consider again the pruning no good { out(EXCUSE), out(COLD)) of the working example (cf. section 4). Then, rule(**) adds {out(EXCUSE)) to the label of COLD and { out(EXCUSE)} becomes another extension base. This is wrong because no DL-extension contains COLD. Therefore, we must not apply (**) to pruning nogoods.

However, if we restrict (**) to logical nogoods we get another problem. The A TMS does not detect every logical nogood:

Here, we obtain a pruning no good {out( -.A), out( A)} and a logical no good {out( -.A), out( A), out( -.C)}. Because the ATMS stores only minimal nogoods it ignores the second one. Thus, we are not able to apply (**) to { out(-.A), out(A), out(-.C)}.

Finally, rule(**) implicitly applies defaults in 'backward' direction. In the following example, it infers -.A from out(B) using the no good {out( -.A), out(B)}:

Because of these problems, we do not get a sound method that finds refutation proofs of -.x if we inspect nogoods consisting of out-assumptions. If we want to prove -.x directly we need further inference rules (and justifications). For example, we can use contraposition rules:

where c,a1, ... ,ak are constants. With these prerequisites we obtain the missing labels in the Nixon example:

This approach works for examples where unit clause resolution is complete w.r.t. the derivation of negated formulas.

7. Related Work

We started this work by examinating the ideas of 0. Dressler. In [Dressler, 1988a], he already proposed how to encode defaults using monotonic justifications and out­ assumptions. Furthermore, he introduced the meta rule to resolve inconsistencies. However, he did not verify his approach using default logic and did not specify a semantics for the meta rule. After the author had detected the problem imposed by exceptions and presented a first solution, 0. Dressler developed an own test algorithm to deal with exceptions of exceptions. In contrast to our test, it inspects justifications instead of labels and uses a backward strategy (cf. [Dressler, 1988b]). This algorithm is yet not verified and a precise comparison is a goal of further discussions.

[.de Kleer and Reiter, 1987] and [de Kleer, 1988] generalize ATMS by propositional clauses, but do not capture non­ monotonic justifications. Brown et. al. [1987] translate justifications into boolean equations where non-monotonic antecedents are handled by the complement operator. Their approach is also non-incremental. If we add a new justification for x we must exchange the equation of x. Furthermore, they need extra effort to find well-founded (or grounded) solutions.

8. Conclusion

We developed a correct non-monotonic reason maintenance system that is able to deal with exceptions, inconsistencies, and multiple extensions. It overcomes the limits of Doyle's TMS and A TMS. TMS only finds a single extension and gets in trouble with odd loops. ATMS produces too many extensions if there are exceptions of exceptions. Therefore, we extended the ATMS by an additional test algorithm which uses an efficient technique for exception handling. Its complexity is nearly linear in a lot of examples. We implemented this algorithm in Common Lisp and used the hybrid RMS to realize a simple default prover.

We verified our hybrid reason maintenance system using Reiter's default logic (DL). To enable this task, we related DL concepts to the concepts of monotonic inference systems and replaced the fixpoint criterion by a simpler criterion for assumption sets.

Finally we discussed some problems caused by special techniques for contradiction handling. We proposed to resolve logical inconsistencies by semi-normal defaults. Then the reason maintenance system must be able to derive negated formulas.

Acknowledgements

Especially, I am grateful to Gerd Brewka and Hans Voss for their support and encouragement. Furthermore, I would like to thank Johan de Kleer, Paul Morris, and Oskar Dressler who spent time for discussion.