Towards Efficient Default Reasoning

1 Introduction

In this paper we develop a theorem-proving method for default logic of Reiter [1980). Default logic is one of the most well-known nonmonotonic logics [Marek and Truszczynski, 1993). There is a body of results indicat­ ing that default logic captures a large number of different forms of nonmonotonic reasoning. Default logic is closely related to logic programs and deductive databases [Gel­ fond and Lifschitz, 1990]. Connections have been es­ tablished between default logic and autoepistemic logic and McDermott and Doyle style nonmonotonic modal logics [Konolige, 1988; Truszczynski, 1991), circumscrip­ tion [Etherington, 1987), diagnosis [Reiter, 1987), and abductive reasoning [Poole, 1988).

In default logic knowledge is represented by a default theory, which consists of ordinary first-order formulae and nonmonotonic inference rules, default rules. Possi­ ble sets of conclusions from a default theory are defined in terms of extensions of the default theory. In this pa­ per we consider three basic reasoning tasks: extension existence (whether a default theory has an extension), brave reasoning (whether a formula is in some extension of a default theory) and cautious reasoning (whether a formula belongs to every extension of a default theory).

Computational properties of nonmonotonic reason­ ing have received considerable attention. This research provides a valuable basis for developing nonmonotonic theorem-proving techniques. The complexity of proposi­ tional default reasoning has been located at the second level of the polynomial time hierarchy [Garey and John­ son, 1979): extension existence and brave reasoning are E~-complete and cautious reasoning 11~-complete [Got­ tlob, 1992]. This means that full propositional default logic can be implemented in polynomial space and that it is strictly harder than propositional reasoning unless the polynomial time hierarchy collapses.

Developing theorem-proving techniques for default logic and other nonmonotonic logics has turned out to be difficult. Existing techniques are quite straightforward and little emphasis has been laid on efficiency consider­ ations. For example, in recent approaches [Junker and Konolige, 1990; Risch and Schwind, 1994; Baader and Hollunder, 1992) to automating default logic exponen­ tial space is needed or the methods are based on solving subtasks that seem to be computationallyharder than the original default reasoning task.

We consider first approaches where a reasoning prob­ lem in default logic is reduced into another problem like a truth maintenance problem [Junker and Konolige, 1990) or a constraint satisfaction problem [Ben-Eliyahu and Dechter, 1991]. A crucial feature of the reduction map­ pings is that classical deductions needed in default rea­ soning have to be encoded. This implies that reductions are computationally feasible only for very restricted sub­ classes of default logic. Typically, the reductions lead to an exponential increase in the problem size because of the exponential number of deductions to be encoded. Moreover, computing the reduction mapping appears to be harder than the original default reasoning problem. This is because even the problem of finding a single de­ duction, {i.e., a proof of a given formula from a set of for­ mulae) is closely related to logic-based abduction, which is E~-complete [Eiter and Gottlob, 1992). For a more detailed discussion, see [Niemela., 1994].

Risch and Schwind [1994) propose a tableau-based method for finding extensions. Also this approach suffers from the problem of exponential worst-case space complexity. Baader and Hollunder [I992) present an ap­ proach to generate all extensions of a default theory by pruning defaults in a top-down way. When eliminating defaults, this method uses heavily a subroutine comput­ ing all maximal consistent subsets, i.e., given sets :E and H the subroutine is expected to find all maximal sub­ sets H' of H such that :E U H' is consistent. It seems that finding all such maximal subsets is computationally expensive and at least as hard as the decision problems in default logic. This is because, for example, finding a maximal subset not containing a given formula in H is closely related to logic-based abduction. To see this consider a maximal subset H' ~ H for which :E U H' is consistent but 1/J E H - H'. Hence, :E U H' U { 1/J} is not consistent which implies that ·1/J is a logical consequence of :E U H', i.e. H' is an abductive explanation of ·1/J from the hypotheses H and the background theory :E.

In this paper we develop a decision method for de­ fault logic that handles important subclasses of default reasoning (i.e., the full propositional case as well as closed default rules together with a decidable fragment of the underlying first-order logic) but does not suffer from the two problems: (i) exponential space require­ ments and (ii) the use of computationally too difficult subtasks as a part of the method. As a basis of the work we have taken a decision method for autoepistemic logic presented in [Niemela., I994) because this approach satisfies the two requirements. As autoepistemic logic and default logic are closely related [Konolige, I988; Niemela., I992), the approach is directly applicable to default logic. However, there seems to be some room for improvements. In this paper we take the basic ideas from [Niemela., I994) and apply them directly to default logic in order to fully exploit the special characteristics of default reasoning.

The paper is organized as follows. Section 2 intro­ duces default logic and develops a concise representa­ tion of extensions. This representation is based on ideas from autoepistemic reasoning and it forms the basis for the decision method. Section 3 develops a basic algo­ rithm for default reasoning. It provides a framework for integrating optimization techniques. Section 4 presents optimizations of the basic algorithm and Section 5 con­ tains the concluding remarks.

2 Default Logic

We are going to use intuitions from autoepistemic rea­ soning and to facilitate this we employ somewhat non­ standard notations for default logic. First, we introduce a new operator nb(·): nb(¢) expresses that a formula¢ is "not believed", i.e. ¢ does not belong to the extension in question. Second, we write default rules using the new operator. A default rule is an expression of the form

where a1, ... , an, b1, ... , bm, care arbitrary (first-order) formulae. This is just an alternative notation for a de­ fault rule in the standard form

A default theory is a set of default rules of the form (I). In Reiter's [I980) original presentation a default the­ ory can contain ordinary first-order formulae in addition to default rules. Here for uniformity the first-order for­ mulae are represented as default rules, i.e., a first-order formula ¢ is represented as a rule ....._. ¢.

A default rule of the form (I) can be thought of as representing an autoepistemic formula

Under this translation, proposed by Truszczynski [I99I), an extension of a default theory is the L free part of an L­ hierarchic expansion of the translated theory [Niemela, I992) or the L free part of a consistent S-expansion of the translated theory for a ranf.e of nonmonotonic modal logics S [Truszczynski, I99I . Hence default rules of the form (I) provide an interesting "standard" form of autoepistemic formulae.

Next we give the definition of an extension of a default theory. Technically our definition is somewhat different from that given by Reiter [I980) but it leads to the same class of extensions. The definition is given by using the notions of a deductive closure and NB-formulae.

We call NB-formulae expressions of the form nb(¢) where¢ is a formula. For a set offormulae S, nb(S) = {nb(¢) I ¢ E S}. By s+ (s-) we denote set of formulae (NB-formulae) in S. For example, if S = {a,nb(b),nb(c)}, s+ = {a} and s- = {nb(b),nb(c)}.

We denote by Dcl(:E, L) the deductive closure of a set of rules :E of the form (I) and a set offormulae and NB­ formulae L. Dcl(:E, L) is the smallest set of formulae which contains L + and which is closed under :E' and first-order derivations where

For example, let :E = { nb(p) ....._. q; ··q ....._. ··r} and L = {p, nb(p)}. Then :E' = { ....._. q; ··q ....._. ··r} and Dcl(:E, L) = Th( {p, q, ··r}) where Th(S) denotes the set of the first-order consequences of a set of formulae S . This means that, e.g., r E Dcl(:E, {p, nb(p)} ).

Notice that the deductive closure is a monotonic oper­ ator also with respect to the premises L : if L ~ L', then Dcl(:E, L) ~ Dcl(:E, L').

For a set of rules :E, a set of formulae 6. is called an extension of :E iff 6. = Dcl(:E, nb(6.)) where 6. is the complement of 6., i.e., the formulae not in 6..

We develop a compact characterizing condition for ex­ tensions. The formulae that occur inside the nb( ·) oper­ ator play a crucial role. For a set of rules :E, we denote by NAnt(:E) the negative antecedents in :E, i.e., the set of formulae b such that nb(b) appears in :E. For example, NAnt({nb(p) ....._. q; ··q ....._. ··r}) = {p}. The follow­ ing proposition makes the role of NAnt(:E) evident. It is based on the observation that for the deductive clo­ sure of a set of rules only the NB-formulae appearing in the rules are of importance, i.e., Dcl(:E, nb(6.)) = Dcl(:E,nb(NAnt(:E)- 6.)).

Proposition 2.1 For a set of rules :E, a set of formulae 6. is an extension of:E iff 6. = Dcl(:E, nb(NAnt(:E)-6.)).

The situation is similar to that in autoepistemic logic where a stable expansion is uniquely determined by the modal subformulae in the premises [Niemelli., 1990]. For characterizing extensions, we are able to use ideas from the full set based characterization of stable expan­ sions [Niemelli., 1990]. The novelty here is that we exploit the strong groundedness of extensions which implies that ordinary formulae appearing as antecedents of rules (pre­ requisites) do not play a role in determining extensions and only NB-formulae (justifications) are essential.

Our aim is to provide a compact characterizing set for each extension. The characterizing sets are called full sets and they are sets of NB-formulae built from formulae in NAnt(I:).

Definition 2.2 For a set of rules I:, a set A of NB­ formulae is called 1::-full iff the following condition holds for all¢ E NAnt(I:), nb(¢) E A iff¢ r/. Dcl(I:, A).

For example, let 1:: = {nb(p) <.......t -,p; nb(-,p) <.......t p}. Then {nb(p)} is 1::-full, because p r/. Dcl(I:, {nb(p)}) and -,p E Dcl(I:, {nb(p)}) but, e.g., 0 is not 1::-full, as p r/. Dcl(I:, 0). It turns out that for every full set there is an extension and for each extension a corresponding full set.

Theorem 2.3 Let 1:: be a set of rules.

(i) If a set A is I:-full, Dcl(I:, A) is an extension of 1::. (ii) If there is an extension ~ of I:, then A = nb(NAnt(I:)-~) is a 1::-full set such that~ = Dcl(I:, A) .

Proof. (i) Let ~ = Dcl(I:, A). If ¢ E NAnt(I:) - ~, then as A is I:-full, nb( ¢) E A. If nb( ¢) E A, then as A is 1::-full, ¢ E NAnt(I:) - ~- Thus nb(NAnt(I:) - ~) = A holds which by Proposition 2.1 implies that Dcl(I:, A) is an extension of 1::.

(ii) Let ~ be an extension of 1::. By Proposition 2.1 ~ = Dcl(I:, A) for A = nb(NAnt(I:) - ~). Let ¢ E NAnt(I:). If¢ E Dcl(I:, A), then ¢ E ~ and nb(¢) r/. A. If¢ rf. Dcl(I:, A) , then¢ rf. ~and nb(¢) EA. Hence, A is 1::-full. D

Theorem 2.3 suggests the following straightforward method for finding all extensions. For each subset S of NAnt(I:), test whether nb(S) is 1::-full. If a full set A is found , Dcl(I:, A) is an extension of 1:: by Theorem 2.3 (i) and by Theorem 2.3 (ii) for each extension~ there is a corresponding full set A such that ~ = Dcl(I:, A).

Example 2.1 The straightforward method is not very practical. If there are n NB-formulae in 1::, 2n fullness tests are needed although there can be a single extension which is easily constructible as the following set of rules 1:: shows.

There are 2n candidates for 1::-full sets but only one 1::­ full set A = 0. This can be seen by the following ar­ gument. For any set F, a0 E Dcl(I: , F) which implies a1 E Dcl(I:,F) . Hence nb(a1) cannot belong to any 1::­ full set neither can nb(a2) and so on. ·

3 The Basic Algorithm

In this section we develop a basic algorithm for solv­ ing default reasoning problems. The basic algorithm serves as a framework for developing further optimiza­ tion methods, which are discussed in the next section. The algorithm is based on ideas introduced in [Niemel:i., 1994] in the context of autoepistemic reasoning. The algorithm presented in Figure 1 is given as a function extensionsnL that is the skeleton for the decision pro­ cedures for brave and cautious reasoning as well as for checking the existence of extensions.

When describing the algorithm we use the following three concepts.

• (i) A set of formulae and NB-formulae A is grounded in a set of rules 1:: if A+ ~ Dcl(I:,A-). For example, {nb(b)} and {b, nb(a)} are grounded in {nb(a) <.......t b; a'-+ a} but {a} is not.
• (ii) We say that a set of formulae S agrees with a set of formulae and NB-formulae A if for all formulae ¢ E A+, ¢ E Sand for all nb(¢) E A-, ¢ rf. S. For example, the set {a,b} agrees with {a,nb(c)} but not with {a,nb(b)}.
• (iii) A set of formulae and NB-formulae A covers a formula ¢ if either ¢ E A or nb(¢) E A. For example, the set { nb( a), b} covers a. A set of formulae S is covered by A if each formula in S is covered by A.

The function extensionsnL takes as input a set of rules 1::, sets B and F which determine the common part of the extensions to be considered and a formula ¢ which is just passed as an argument to the function test. The aim of extensionsnL is to return true iff there is an extension ~of 1:: agreeing with B U F such that test(~,¢) returns true. This is accomplished by constructing 1::-full sets agreeing with B U F until a full set A is found such that for the corresponding extension ~ = Dcl(I:, A), test(~,¢) returns true.

We represent a partially constructed full set using the set B that contains NB-formulae and ordinary formulae. The NB-formulae B- are the formulae included in the partially constructed full set. An ordinary formula x in B indicates that the corresponding NB-formula nb(x) cannot be included in the full set. The idea is to expand B until it forms a full set. The number of possibilities can be reduced by observing that if a formula is grounded in the rules 1:: given the partially constructed full set B-, i.e., x E Dcl(I:, B-), nb(x) cannot be included in the full set and x is added to B. The set F contains formulae x for which nb(x) is excluded from the full set to be constructed (and x should be included in B), but which are "frozen" : x E F is added to B only when the groundedness condition is satisfied, i.e., x E Dcl(I:, B-).

The function extensionsnL uses three functions

• expand (for expanding B)
• confiict (for detecting conflicts), and
• test (for testing extensions).

By changing the function test the various decision proce­ dures are obtained. For the first two functions we present minimal requirements (E1-E4, C1-C2) that the imple­ mentations of these functions have to satisfy in order to guarantee the soundness and completeness of the deci­ sion procedures. These two functions form the crucial

function extensionsnL(~, B, F, ¢) B := expand(~,B,F); if conflict(~, B, F) returns true then return false else if NAnt(~) is covered by B U F then ifF~ B then return test(Dcl(~, B-),¢) else return false endif else take some x E NAnt(~) not covered by B U F; ifextensionsDL(~,B U {nb(x)},F,¢) returns true then return true else return extensionsnL(~, B, F U {x}, ¢) end if endif

points in the algorithm where optimization techniques can be applied. In the next section such optimization methods are developed.

We first introduce the requirements on the functions expand and conflict and then explain their role in guar­ anteeing the correctness of extensionsnL· The func­ tion expand is assumed to fulfill the following conditions where Be= expand(~, B, F).

E1: B ~Be .

E2: If B is grounded in ~' then Be is grounded in ~­

• E3: If there is an extension <l of ~ such that <l agrees with B U F, then <l agrees with Be U F .
• E4: For all X E NAnt(~), X E Dcl(~,B;) implies that x is covered by Be.

The function conflict returns either true or false and satisfies the following conditions.

• C1: conflict(~, B, F) returns true iffor some nb(x) E B, X E Del(~, B-).
• C2: If conflict(~, B, F) returns true, then there exists no extension <l of ~ such that <l agrees with B U F.

The function extensionsnL starts by expanding cau­ tiously the set B. In order to ensure the correctness of the decision procedures we must insist that the ex­ pansion Be = expand(~, B, F) extends B (El) in such a way that groundedness is preserved (E2) and that no extensions agreeing with B U F are lost (E3) . To pre­ serve completeness we have to require that each formula in NAnt(~) that is grounded but not already covered by B is included in B (E4). Then a conflict test is per­ formed. Here it must be the case that all direct conflicts are detected (C1) and if a conflict is reported, then there is no extension agreeing with B U F (C2). If there are no conflicts and B U F covers every NB-formula in the premises, then the status of frozen formulae F is exam­ ined. If all of them have been included in B, B- is a full set. The corresponding extension is Del(~, B-) and extensionsnL returns what test(Dcl(~, B-),¢) returns.

If there is an NB-formula nb(x) in the premises such that x is not covered by B U F, then either x belongs to the extension to be constructed or not. The two al­ ternatives are handled by backtracking. First B is ex­ tended by nb(x) (assuming that x is not in the exten­ sion) . If extensionsnL(~, BU{nb(x)}, F, ¢)returns false, then the other alternative is examined by taking x as a frozen formula (assuming that x is in the extension). Then extensionsnL returns what extensions0L(~, B, FU {x}, ¢) returns.

Assuming that the functions expand and conflict sat­ isfy the conditions (E1- E4, Cl- C2), it can be proved by induction on the number offormulae in NAnt(~) but not covered by BUF that extensionsDL is sound (if it returns true, there is an extension of ~ agreeing with B U F for which the function test returns true) and complete (if there is an extension of~ agreeing with B U F for which test returns true, then extensions0L(~, B, F, ¢) returns true). Hence we have the following soundness and com­ pleteness theorem.

Theorem 3.1 Let~ be a set of rules . Let B be a set of formulae and NB-formulae, F a set of formulae, and B be grounded in~- Then extensionsnL(~, B, F, ¢) returns true iff there exists an extension <l of ~ which agrees with B U F and for which test(<l,¢) returns true.

The theorem implies that decision procedures for the different reasoning tasks can be obtained by (i) taking the empty set as the common part of the extensions to be constructed and (ii) choosing an appropriate test func­ tion as shown in the following corollary.

Corollary 3.2 Let ~ be a set of rules and ¢ a formula.

1. If test(<l, ¢) returns true for all <l and ¢, then extensionsnL(~, 0, 0, ¢) returns true iff~ has an ex­ tension.
2. If test(<l, ¢) returns true iff ¢ E <l, then extensionsnL(~, 0, 0, ¢) returns true iff there exists an extension of~ containing¢.
3. If test(<l, ¢) returns true iff ¢ ¢ <l, then extensionsnL(~, 0, 0, ¢) returns true iff there exists an extension of ~ not containing ¢ (and, in other words, extensionsDL(~, 0, 0, ¢) returns false iff¢ is contained in every extension of ~).

To illustrate the conditions El-E4, C1- C2 we present the following "minimal" implementation of expand and conflict satisfying E1-E4, C1- C2.

• E-10 Let expand(~, B, F) return B U {x E NAnt(~) I x not covered by B,x E Del(~, B-)}.
• C-10 Let conflict(~, B, F) return true iff there exists nb(x) E B such that x E Del(~, B-) .

Example 3.1 Although the minimal implementation is taken directly from the minimal requirements, the re­ sulting decision method is already quite powerful. Let us use the implementation to decide brave reasoning. Hence, we let test(<l, ¢) return true iff¢ E <l.

• (i) Consider whether the set of rules ~ in Exam­ ple 2.1 has an extension containing a formula b. Hence,

we examine the execution of extensionsoL(:E, 0, 0, b). Here expand(:E, 0, 0) returns { a1, ... , an} and false is returned by conflict(:E,{a1, . . . ,an},0). Because B U F = {at, ... ,an} covers NAnt(:E) = {a1, . . . ,an} and F = 0 ~ {a1, ... ,an} = B, we have found a :E­ full set s - = 0 and the corresponding extension is Dcl(:E, 0). Now test(Dcl(:E, 0), b) returns false and extensionsoL(:E, 0, 0, b) returns false. Hence the mini­ mal implementation is able to determine that :E does not have an extension containing b without backtracking.

• (ii) Consider whether b follows in the brave sense from

Hence, we examine the execution of

First expand(:E, 0, 0) returns 0 and conflict(:E, 0, 0) re­ turns false. Since NAnt(:E) = {a, b} is not covered by B U F = 0, we must choose either a or b in order to continue. Let us take a. Then

is executed and here first expand(:E, {nb(a)},0) returns {nb(a), b }. Then conflict(:E, { nb(a), b }, 0) returns true as a E Dcl(:E, {nb(a)} ). So extensionsnL(:E, {nb(a)}, 0, b) returns false and

is executed. Now expand(:E, 0, {a}) returns 0 and conflict(:E, 0, {a}) returns false. Because NAnt(:E) is not covered by B U F = {a}, we must choose b in order to continue. Then

is executed and here expand(:E, {nb(b)}, {a}) returns {nb(b),a} and then conflict(:E, {nb(b),a}, {a}) returns false. Because NAnt(:E) is covered by BUF = { nb(b), a} and F = {a} ~ {nb(b),a} = B, we have found an extension Dcl(:E,B-) = Dcl(:E,{nb(b)}) of :E and test(Dcl(:E, {nb(b)}),b) is performed but false is re­ turned. Hence

is executed. Now expand(:E, 0, {a, b}) returns 0 and conflict(:E, 0, {a, b}) returns false. Because NAnt(:E) is covered by B U F = {nb(b),a} but F = {a,b} C£. 0 = B, extensions0 L(:E,0,{a,b},b) returns false and hence extensionsoL(:E, 0, 0, b) returns false. Thus, there is no extension of :E containing b. ·

4 Optimizations

The basic algorithm divides default reasoning into two major subtasks. One is the search problem of examin­ ing all the alternatives for full sets. This is implemented using (chronological) backtracking and in the worst case the algorithm can search through 2n alternatives where n is the number of different NB-formulae in the premises. The other is the classical reasoning problem of decid­ ing whether a formula if> is in the deductive closure of a set of rules :E given some formulae (and NB-formulae)

as premises L, i.e., whether if> E Dcl(:E, L) holds. The membership in the deductive closure is needed in the functions expand and conflict.

The two difficult tasks are in accordance with the re­ cent results on the complexity of default reasoning show­ ing that default reasoning is a complete problem with respect to the second level of the polynomial time hi­ erarchy [Gottlob, 1992]. The result implies that there are two orthogonal sources of complexity in default rea­ soning, too. This suggests that we have not introduced additional sources of computational complexity in the basic algorithm.

In this section we present optimization techniques which lead to more efficient methods for solving the two subtasks. As there is quite a lot of research on classical reasoning, the emphasis is on the search problem. But before moving to it we make a couple of remarks about the classical reasoning problem.

• First, notice that the classical reasoning problem is reducible to deciding logical consequence for the un­ derlying (first-order) logic. Testing the membership in the deductive closure of a set of n rules can be implemented using at most n 2 tests for logical con­ sequence in the following way. First construct the set of rules :E 1 (2). Then apply rules in :E 1 until no new rule fires as follows.

For the resulting C, if> E Dcl(:E,L) iff if> E Th(C).

• Second, the tests for the membership in the deduc­ tive closure have a very regular pattern where the set of premises gradually grows. This pattern can be exploited.
• Third, when dealing with a large set of rules, it is important to develop methods for testing the mem­ bership in the closure in a goal-directed way so that only a relevant subset of rules is used.

Now we turn to the search problem. The poten­ tial search space is exponential and even for a set of rules with 50 different NB-formulae, its size is over 10 15 . Hence it is essential that the search space is pruned effec­ tively. In extensionsnL the functions expand and conflict handle the pruning of the search space.

Expanding B

The function expand extends the current common part B of the full sets to be constructed. The more formulae are added, the fewer choice points for backtracking are left; every new formula included to B cuts the remaining search space by half.

Although the implementation E-IO can reduce the search dramatically like in the case of Example 2.1, its basic weakness is that it cannot detect when a formula cannot be in an extension. An optimized version of the implementation should be able to detect simple case like function expand(I:, B, F) repeat

B':=B; B := B U {4> E NAnt(I:) 14> is not covered by B, 4> E Dcl(I:, B-)}; B := B U {nb(</>) 14> E NAnt(I:),</> is not covered by B, 4> ¢ Dcl(I:, nb(NAnt(I:)- (B U F)))} until B = B'; return B.

if 1: = {ao <--t a1; nb(al) <--tao; nb(b) <--t ao}, then b is in no extension of I: and nb(b) can be included in B. But also more complicated situations should be covered. For example, consider the set of rules (3) in Example 3.1 and a situation where we are looking for an extension containing a, i.e., F = {a}. It is evident that no such extension of I: contains band nb(b) could be deduced.

In [Niemela., 1994) a technique is presented for deter­ mining that a formula cannot be in an extension. An attractive feature of this approach is that only a poly­ nomial number of logical consequence tests are needed. We adopt this technique which is based on the follow­ ing idea. We use as an upper bound for the formulae included in any extension of I: agreeing with B U F the deductive closure of I: when assuming every NB­ formula not excluded by B U F, i.e., the upper bound is Dcl(I:, nb(NAnt(I:) - (B U F))). Proposition 4.1 shows that the formulae not in the upper bound cannot be in any extension of I: agreeing with B U F.

Proposition 4.1 Let ~ be an extension of I: and let B U F agree with ~. Then 4> E ~ implies 4> E Dcl(I:,nb(NAnt(I:)- (B U F))).

Proof. Let 4> E ~- Then by Proposition 2.1 4> E Dcl(I:, nb(NAnt(I:) - ~)). If X E NAnt(I:) - ~. then x ¢ B U F since ~ agrees with B U F. Hence, nb(NAnt(I:)- ~) ~ nb(NAnt(I:)- (B U F)) which im­ plies 4> E Dcl(I:, nb(NAnt(I:) - (B U F))). 0

A new implementation E-ll of expand including this technique is described in Figure 2. This implementation is able to handle also the more complicated situations and, e.g, for the set of rules I: (3), B = 0, and F ={a} this implementation returns { nb(b ), a} as the new set B. It is quite simple to prove that this implementation of expand satisfies the conditions E1-E4. A critical point is the condition E3, which can be shown by Proposition 4.1.

Proposition 4.2 The implementation E-11 of expand satisfies the conditions E 1-E,f.

Detecting Conflicts

The function conflict tries to detect conflicts, i.e., situa­ tions where there is no extension agreeing with B U F. Every time a conflict is found a part of the search space is removed and the earlier the conflict is detected the larger part is eliminated.

The conflict test in the implementation (C-10) is quite weak in detecting conflicts. Consider, e.g., a set of rules ~ = {nb(p) <--t q; p <--t q; nb(q) <--t r} and let B =

{nb(q)} and F = {p}. Then there is a conflict since any extension agreeing with B U F contains q. In [Niemela., 1994) a conflict test which detects such conflicts is pro­ posed. The idea is to exploit the frozen formulae F in detecting conflicts. The same idea can be used here: if there exists nb( 4>) E B such that 4> E Dcl(I:, B U F), there is a conflict and conflict(I:, B, F) can return true.

We can strengthen the conflict test on the basis of the following observation: there is a conflict if a frozen formula 4> E F cannot belong to any extension of the premises agreeing with B U F. Consider, e.g., a set of rules I: = { nb(p) <--t q; nb(q) <--t r} and let B = 0 and F = {p, q}. There is a conflict since no extension of I: agreeing with BUF contains q. This kind of conflicts can be detected using the aforementioned notion of an up­ per bound for extensions. The following implementation includes both optimizations for conflict detection.

C-11 Let conflict(I:, B, F) return true iff for some nb(¢) E B, ¢ E Dcl(I:,B U F) or for some¢ E F, ¢ ¢ Dcl(I:, nb(NAnt(I:) - (B u F))).

Proposition 4.3 The implementation C-11 of conflict satisfies the conditions C1-C2.

Proof. The condition C1 is clearly satisfied because Dcl(I:, B-)~ Dcl(I:, B U F).

(C2) Let~ be an extension of I: agreeing with B U F. We show that conflict(I:, B, F) cannot return true. Let nb(¢) E B. Then¢¢~= Dcl(I:,nb(~)). Since B- ~ nb(~), Dcl(I:, BUF) ~ Dcl(I:, nb(~)uB+ UF). Because B+ U F ~ ~. Dcl(I:,nb(~) Us+ U F) = Dcl(I:,nb(~)). So nb( ¢) E B implies ¢ f/. Dcl(I:, B U F).

If ¢ E F, then ¢ E ~ and by Proposition 4.1 ¢ E Dcl(I:,nb(NAnt(I:)- (BUF))). Hence, the condition C2 holds. o

5 Conclusions

In this paper we develop a decision method for default logic which solves the extension existence problem as well as the brave and cautious reasoning problems. It handles the full propositional case and the first-order subclasses of default theories with closed default rules and a de­ cidable fragment of the underlying first-order logic. The method differs from other recent approaches [Junker and Konolige, 1990; Risch and Schwind, 1994; Baader and Hollunder, 1992) to automating default logic in two ma­ jor respects: (i) in the propositional case it can be im­ plemented in polynomial space and (ii) it does not rely on solutions of subtasks which appear to be computa­ tionally harder than the original default reasoning prob­ lem. The method partitions default reasoning into two major subtasks: the search problem of examining every alternative for extensions, which is solved by backtrack­ ing search, and the classical reasoning task, which can be implemented by a theorem prover for the underlying classical logic. Special emphasis is given to the search problem. The method employs a new compact charac­ terization of extensions based on considering only the justifications of the rules. This reduces the search space for alternatives for extensions. Techniques for pruning the search space are developed. Initial experiments in­ dicate that using the implementations E-ll and C-ll of expand and conflict the search space is often kept rel­ atively small and we have been able to handle default theories with a few hundred default rules.

The method developed in this paper is closely re­ lated to that presented in [Niemela, 1994] for autoepis­ temic reasoning. The key difference is that the novel method uses the new compact characterization of ex­ tensions which leads to a smaller initial search space. We exploit the strong groundedness of default exten­ sions which implies that extensions are determined by the justifications of the default rules, while in the earlier approach [Niemela, 1994] both prerequisites and justi­ fications of the default rules are employed in the char­ acterization. Optimization techniques that prune the search space are discussed already in [Niemela, 1994]. The technique of expanding the set B (E-ll) is proposed in [Niemela, 1994] but the conflict detection method ( C-I1) is novel.

There are interesting areas for further research. The decision method in this paper uses heavily classical rea­ soning for pruning the search space. This implies that the development of efficient theorem-proving techniques for implementing the needed classical reasoning in a goal­ directed way is important. The potential search space is very large and further work is needed for developing new pruning techniques. The basic algorithm with the requirements for the functions expand and conflict offers a framework for developing these kinds of optimizations. The decision method can be used in a goal-directed man­ ner by initializing the sets B and F accordingly. For example, if we are interested in extensions containing p but not q, we can start the method with B = { nb(q)} and F = {p}. An interesting topic for further research is to develop goal-directed techniques where a default reasoning task is analyzed and divided to appropriate subtasks. In the method there is a heuristic choice when a new formula x E NAnt(L:) not covered by B U F is selected. A further area of study is the development of efficient search heuristics.