Constrained and Rational Default Logics

1 Introduction

Default logic, introduced by Reiter [1980], is one of the most extensively studied nonmonotonic systems. Sev­ eral recent research monographs offer a comprehensive presentation of theoretical and practical aspects of de­ fault logic [Besnard, 1989; Brewka, 1991b; Marek and Truszczynski, 1993]. Default logic was designed to han­ dle reasoning from incomplete information. It allows us to draw conclusions on the basis of "the lack of evidence to the contrary". This formalism assigns to a default theory a collection of theories called extensions. They describe possible belief sets of an agent reasoning with this theory.

All its desirable properties notwithstanding, there are situations where default logic of Reiter produces counterintuitive results. In particular, this logic does not handle well incomplete information given in the form of disjunctive clauses [Poole, 1989; Brewka, 1991a; Gelfand et al., 1991; Mikitiuk and Truszczynski, 1993]. To remedy this, several modifications of default logic were proposed: disjunctive default logic [Gelfand et al., 1991], cumulative default logic [Brewka, 199la], con­ strained default logic [Schaub, 1992] and rational default logic [Mikitiuk and Truszczynski, 1993]. The first system introduces a new disjunction operator to handle "effec­ tive" disjunction. The latter three take into account, in one way or another, the requirement that defaults with mutually inconsistent justifications must not be used in the construction of the same extension. Not surprisingly then, they are somewhat related.

Connections between cumulative default logic and constrained default logic are studied in [Schaub, 1992]. It is shown there that these two systems are, in a certain sense, equivalent. At the same time, they are quite differ­ ent from default logic of Reiter. Both commit to assump­ tions and have such properties as semi-monotonicity and orthogonality 1 . In addition, in each of these two logics every default theory has an extension. In the logic of Re­ iter all these properties hold for normal default theories but fail in the general case (in fact, for normal default theories, Reiter's default logic is essentially equivalent to constrained and cumulative default logics).

In this paper, we investigate connections between ra­ tional and constrained (and, consequently, also cumu­ lative) default logics. Rational default logic, similarly as the logic of Reiter, lacks many of the properties of constrained default logic. In particular, default theo­ ries may have no rational extensions and rational default logic does not have the properties of semi-monotonicity and orthogonality. The reason is that rational default logic, unlike constrained default logic, does not commit to assumptions. At the same time, connections between rational and constrained default logics are quite strong. We show that every rational extension of a default theory determines a constrained extension. Moreover, we show that rational and constrained default logics coincide for the class of seminormal default theories - a much wider class of theories than normal ones, for which all four versions of default logic mentioned here are equivalent.

We also give a useful, proof-theoretic, characterization of the operator 1, which was used in [Schaub, 1992] to define the notion of a constrained extension. Conse­ quently, we get an equivalent definition of constrained extensions. This result allows us to design an algorithm for computing constrained extensions and to establish the complexity of reasoning with constrained extensions. Since every default theory has a constrained extension, the problem of existence of a constrained extension is, clearly, in P. We show that the problem to decide, given a formula <p, whether <p is in at least one constrained extension (in all constrained extensions) of a given de­ fault theory, is I:f -complete (IIf -complete). In view of a recent result on the complexity of cumulative de­ fault logic [Gottlob and Mingyi, 1994] and our results on the complexity of rational default logic [Mikitiuk and Truszczynski, 1993], it follows that all these modes of reasoning have the same computational complexity.

1 Schaub [1992] uses the term weak orthogonality

Finally, let us note that Schaub did not allow justification-free defaults in his definition of constrained default logic. In this paper, we show how to extend con­ strained default logic to cover theories which may con­ tain justification-free defaults.

2 Preliminaries

A default is any expression of the form

where a, f3i, 1 ~ i ~ k and 1 are propositional formu­ las. Let d be a default of the form (1). The formula a is called the prerequisite of d, p( d) in symbols. The formulas f3i, 1 ~ i ~ k, are called the justifications of d. The set of justifications is denoted by j(d). Finally, the formula 1 is called the consequent of d and is denoted c(d). For a collection D of defaults by p(D), j(D) and c(D) we denote, respectively, the sets of all prerequi­ sites, justifications and consequents of the defaults in D. A default of the form o: :'t(J ( o: : M~I\"Y), resp.) is called normal (semi normal, resp.).

A default theory is a pair (D, W), where Dis a set of defaults and W is a set of propositional formulas. A de­ fault theory (D, W) is normal (seminormal, resp.) if all defaults in Dare normal (seminormal, resp.). A default theory (D, W) is finite if both D and W are finite.

For a set D of defaults we define

Given a set of inL.c:nce rules A, by CnA(·) we mean the consequence operator of the formal proof system PC+ A, consisting of propositional calculus and the rules in A

In [Mikitiuk and Truszczynski, 1993] we introduced the notions of an active set of defaults and a rational extension of a default theory.

Definition 2.1 A set A of defaults is active with respect to sets of formulas W and S if it satisfies the following conditions:

AS1 j(A) = 0, or j(A) US is consistent,

The set of all subsets of a set of defaults D which are active with respect to W and S will be denoted by A(D, W,S). o

Observe, that 0 is active with respect to every W and S. Hence, A(D, W, S) is always non-empty. An applica­ tion of the Kuratowski-Zorn Lemma gives the following result.

Proposition 2.1 ([Mikitiuk and Truszczynski, 1993]) Let (D, W) be a default theory and let S be a propo­ sitional theory. Every A E A(D, W, S) is contained in a maximal element of A( D, W, S). 0

We define MA(D, W, S) to be the set of all maximal elements in A(D, W,S).

Definition 2.2 A theory S is a rational extension for a default theory (D, W) if S = CnMon(A)(W) for some A E MA(D, W,S). o

Schaub [1992] introduced the notion of a constrained extension by means of the following definition.

Definition 2.3 ([Schaub, 1992]) Let (D, W) be a de­ fault theory and let T be a propositional theory. Then T(T) is the pair of smallest sets of formulas (S', T') such that

CE3 For any default o::'::(J ED, if a E S' and TU{f3,/} is consistent then 1 E S' and (3 1\ 1 E T'.

A pair of sets of formulas (E, C) is a constrained exten­ sion of (D, W) if T(C) = (E,C). o

If (E, C) is a constrained extension, then we will refer to E as a proper constrained extension.

The following example shows that the notions of an extension, a rational extension and a proper constrained extension are different.

Example 2.1 Let us consider the default theory (D,0) [Schaub, 1992], where

2 In [Mikitiuk and Truszczynski, 1993] we used the classical reduct of A with respect to S, denoted As, instead of Mon(A) both in AS2 and in the definition of a rational extension. If A satisfies ASl, then As = Mon(A). Since in this paper we will use a different notion of a reduct (Definition 3.2), we decided to reformulate the definitions of active sets and rational extensions to avoid confusion. These definitions are equivalent to the original ones.

This theory has one extension Cn( { c, d}), two rational extensions: S1 = Cn( { c,!}), S2 = Cn( { d, e}), and three constrained extensions: ( Cn( { e,!}), Cn( { e, ....,c, f, -,d})), (S1,Cn({c,b, f, ....,d})), (82, Cn( {d, -,b, e, -,c})). 0

Schaub [1992] does not consider justification-free de­ faults, so in this paper we do not consider them either. Hence, j(A) = 0 only if A = 0. Moreover, in both ra­ tional and constrained default logic one can replace all justifications of a default by their conjunction. Thus, we assume that every default has exactly one justification. In Section 6 we will show how Schaub's definition can be extended to cover the case of justification-free defaults.

3 Characterizations of constrained extensions

In this section we will give two useful characterizations of constrained extensions. The first of them will be based on a proof-theoretic description of the operator T(T). We will use it in the next section to derive complexity results on reasoning with constrained default logic. The characterization requires the notion of a generating de­ fault introduced in [Schaub, 1992]3.

Definition 3.1 ([Schaub, 1992]) Let (D, W) be a de­ fault theory and S and T sets of formulas. The set of generating defaults for (S, T) with respect to Dis defined as

Schaub [1992] proved the following properties of gen­ erating defaults.

Theorem 3.1 Let (S, T) be a constrained extension of a default theory ( D, W). Then

1. There is an enumeration ch, 82, ... of the defaults in GD}J·r) such that for every i = 1, 2, ... , WUc({Jl, ... ,Ji-d) f-p(Ji)· 0

This theorem implies the following useful corollary.

To present our characterization of the operator T(T), we will need two more notions.

3 The notions of a generating default and a reduct used in this paper are different from the standard ones [Reiter, 1980; Gelfond and Lifschitz, 1988]. They are tailored specifically to the needs of constrained default logic.

Definition 3.2 We define the reduct of a set of defaults D with respect to a theory T as

We define the operator C by letting

These concepts allow us to give a constructive descrip­ tion of the operator T(T).

Theorem 3.3 Let (D, W) be a default theory and letT be a propositional theory. Then

Proof. According to Definition 2.3, T(T) is the pair of smallest sets of formulas (S',T') satisfying CE1-CE3. It follows from CE3 that S' is closed under inference rules from Dr. Thus, by the definition of the operator CnA(·), S' = CnDT (W) satisfies CE1-CE3. We need to prove that T' = Cn(WUC(D, CnDT (W), T)) together with S' = CnDT(W) satisfies CE1-CE3.

We will first prove that CnDT (W) ~ Cn(W U C(D,CnDT(W),T)). Let t.p E CnDT(W). Then t.p has a proof from W in PC+ Dr, that is, there is a finite se­ quence t.p1 , ... , I.Pn = t.p such that for every i, 1 ~ i ~ n, at least one of the following conditions holds:

1. I.Pi E W or I.Pi is a substitution instance of an axiom of propositional logic.
2. For some j, k < i, I.Pi follows from I.{Jj and I.Pk by modus ponens.
3. For some j < i, the rule ~ belongs to Dr.

We will prove by induction on the length of this proof that t.p E Cn(W U C(D,CnDT(W),T)). If t.p E W or t.p is a substitution instance of an axiom of propo­ sitional logic then it is clear that t.p E Cn(W U C(D,CnDT(W),T)). If t.p follows from I.PJ and I.Pk by modus ponens then, by the inductive hypothesis, t.pj,I.{Jk E Cn(WUC(D,CnDT(W),T)). It follows that t.p E Cn(W U C(D,CnDT(W),T)). If t.p was obtained by applying an inference rule ; from Dr then '¢ E Cn DT (W). Hence, there is a default '!/!.:.!:::!..!. E D such cp that '¢ E CnDT (W) and T U {{3, t.p} If .L It follows that {31\t.p E C(D,CnDT(W),T) and, consequently, t.p E Cn(W U C(D,CnDT(W),T)). Thus, CnDT(W) ~ Cn(W U C(D, CnDT (W), T)) and CE1 holds.

The theory Cn(WUC(D,CnDT(W),T)) is closed un­ der propositional provability, so CE2 holds. To prove CE3, let us consider a default a:M{J such that a E S' = "( CnDT(W) and TU {f3,'Y} If .L. It follows from the defi­ nition of C(D,S,T) that {31\ 'Y E C(D,CnDT(W),T) ~

Cn(W U C(D,CnDr(W),T)). Hence, the pair (CnDr (W), Cn(WUC(D, CnDr (W), T))) satisfies CEI - CE3.

Let us assume now that a pair of theories (S', T') satis­ fies CEI- CE3. Then it is easy to see that CnDr (W) ~ S'. By CEI, W ~ T'. Let us consider a formula (3 /\ 1 E C(D,CnDr(W),T). Then there is a de­ fault a:':(3 E D such that a E CnDr (W) ~ S' and T U {(3, 1} I( j_, It follows from CE3 that f3 /\ 1 E T'. Hence, C(D,CnDr(W),T) ~ T'. Since, by CE2, T' = Cn(T'), then Cn(WUC(D,CnDr(W),T)) ~ T' and we are done. D

As a corollary, we get a characterization of constrained extensions.

Corollary 3.4 (S, T) is a constrained extension of a de­ fault theory (D, W) if and only if

and S = CnDr(W).

This corollary makes it explicit that constrained de­ fault logic works in two stages. In the first stage, pos­ sible sets of assumptions (constraints, as referred to in [Schaub, 1992]) are established as solutions of the fix­ point equation (2). Then, each of them uniquely deter­ mines the corresponding proper constrained extention.

The fixpoint equation (2) implies that all assumptions (theory T) needed to support a proper constrained ex­ tension S in constrained default logic must be "reprov­ able". This might be regarded as a weakness of con­ strained default logic. In all versions of default logic it is required that formulas in the extensions have justifica­ tions (in terms of proofs from W by means of applicable defaults). But it is arguable whether the same should be required of assumptions "(3 is possible" which make defaults applicable.

Corollary 3.4 allows us to strengthen a result by Schaub on pairwise maximality of constrained extensions of a default theory.

Theorem 3.5 If (S, T) and (S', T') are constrained ex­ tensions of a default theory (D, W) and T ~ T', then T = T' and S = S' (in particular, 'T-parts" of con­ strained extensions form an antichain}.

Proof. First, observe that if (S', T') is a constrained extension of (D, W), then T' is inconsistent if and only if W is inconsistent. Hence, if T' is inconsistent then T is inconsistent as well and, consequently, T = T' and S = S'. Assume then that T' is consistent.

Since (S,T) is a constrained extension of (D, W), by Corollary 3.2 we haveS = CnMon(GD;;·r>)(W). More­ over, for every default a:':(3 E GD};·T), (3 /\1 E T and, since T ~ T', f3 /\1 E T'. Since T' is consistent, it follows that Mon(GD};·T)) ~Dr'· Hence,

Schaub [1992] proved that if (S, T) and (S', T') are con­ strained extensions of a default theory and S ~ S' and T ~ T', then S = S' and T = T'. 0

Theorem 3.5 implies bounds on the number of con­ strained extensions of a default theory.

Corollary 3.6 Let D be a set consisting of n defaults. Then for every W ~ £, the default theory (D, W) has at most

constrained extensions.

Proof. Theorem 3.5 implies that the family T = {T: (S, T) is a constrained extension of (D, W)} is an antichain. By Theorem 3.1, each set T E T is deter­ mined by the set GD};·T). Since Tis an antichain, the family { G D};·T): T E T} is also an antichain. It is well known that the size of the largest antichain in the algebra of subsets of an n-element set has at most ( r nf2l ) elements. Hence, the assertion follows. 0

The second characterization of constrained extensions that we present in this section is closely related to the property of semi-monotonicity of constrained default logic. It exploits the fact that constrained extensions can be produced by processing defaults according to any well-ordering. This is very similar to the corresponding property of normal default theories in the logic of Reiter (Theorem 4.3, [Marek and Truszczynski, 1993]). In fact, our characterization of constrained default logic provides an alternative argument that for normal default theories constrained and standard default logics coincide.

We assume that the set of the atoms of our language £ is denumerable. Consequently, the set of all defaults over the language £ is denumerable.

Let (D, W) be a default theory and -< a well-ordering of D. We define an ordinal 'TJ-<. For every ordinal~ < 'TJ-< we define a set of defaults AD~ and a default d{. We also define a set of defaults AD-< . We proceed as follows: If the sets AD{, ~ < a, have been defined but 'TJ-< has not been defined then

1. If there is no default d E D \ U~ <a AD{ such that:
2. (a) WUc(U{<a AD{)Uj(U{<a AD{)Uj(d)U{c(d)} is consistent, and

then 'TJ-< =a.

1. Otherwise, define da to be the -<-least default d E D\U{<a AD~ such that the conditions (a) and (b) above hold. Then set ADa= U{<a AD{ U {da}.

When the construction terminates, put AD-< = U{<'l-< AD~, S-< = Cn(WUc(AD-<)) and T-< = Cn(WU c(AD .. ,J U j(AD-<)).

This construction has the following property.

Theorem 3.7 Let (D, W) be a default theory and~ a well-ordering of D. Then (S...,,T...,) is a constrained ex­ tension of (D, W) and AD...,= GDtg-<·L.).

Proof. It is easy to see that if W is inconsistent then AD...,= 0 and S..., = T..., = Cn(W) = £. Thus, the asser­ tion follows. Assume now that W is consistent. Then for every ~ < TJ --:, W U c(AD{) U j(ADe) is consistent. Con­ sequently, W U c(AD...,) U j(AD...,) is consistent. Thus, T-< is consistent.

Let us consider a default d = a:':;(3 E AD-<. We have {3 E j(AD...,) and 1 E c(AD...,). Thus, {{3,1} ~ T-< and, since T...., is consistent, T...., U {,B, 1} is consis­ tent. Moreover, since d E AD....,, for some ~ < TJ--:, W U c(U.>.<{ AD>.) 1- a. Consequently, a E S...,. Hence, dE GDtg-<·r-<J.

Consider now a default d = a:':;(J E D \AD..., . Then one of the conditions (a), (b) above fails ford, that is, either T...., U {,B, 1} is inconsistent or S..., If a. Hence, d~ GDtg-<·r-<). Thus, AD...,= GDtg-<·r-<).

The last equality implies that

Thus, to end the proof we need to show that S..., = Cn DT-< (W). Let us notice that the condition (b) above implies that CnMon(AD-<l(W) = Cn(WUc(AD...,)) = S...,. (S-< ,T-<)) ~·Ma Thus, S..., = CnMon(GDv (W). Let A = { 7 E D : T-< U {,8,1} If ..L}. Then Dr-< = Mon(A) and GDtg-<,r-<) ={dE A: p(d) E S...,}. Hence, GDtg-<,r-<) ~ A and

Thus, to show that S..., = CnDT-< (W), we need to prove D M (GD( 5 -<·T-<>) that Cn T-< (W) ~ Cn on v (W) . To this end, let us consider a formula cp E Cn DT-< ( W). The for­ mula cp has a proof from W in PC + Dr-< . One can prove by induction on the length of this proof that M (GD(S-< ,T-<)) <p E Cn on v (W) (due to space restrictions, we omit the details of the argument). 0

The converse result is also true.

Theorem 3.8 Let (S, T) be a constrained extension of a default theory (D, W). Then for any well- ordering~ of D such that defaults from G D~,r) precede all other defaults, AD...,= �D~,r), S-< =SandT...,= T. 0

This result will be proved in a full version of the paper .

4 Computational aspects of constrained default logic

Corollary 3.4 allows us to design an algorithm for com­ puting all constrained extensions for a finite default the­ ory (D, W). Let us consider a set of defaults A ~ D . Let S = CnMon(Al(W), B = {d E A : p(d) E S}, C = {{3 1\ T a:r:;(J E B}, T = Cn(W U C) and E = {a:M(J E D:T U {,8,1} If ..L}. It is easy to see that "' if E = A then (S, T) is a constrained extension for (D, W). Indeed, Dr = Mon(E). Thus, if E = A then Mon(A) = Dr and S = CnDT (W). Moreover, B = GDtg,rJ. Hence, C = C(D,S,T) = C(D,CnDT(W),T) and T = Cn(W U C) = Cn(W U C(D,Cn°T(W),T)). Thus, (S,T) is a constrained extension for (D, W). Con­ sidering all sets A ~ D, we will get all constrained exten­ sions of (D, W). Indeed, if (S,T) is a constrained exten­ sion then it will be found by considering A = {a:':; ,a E D: T U {,B, 1} If ..L} . Thus, we have the following algo­ rithm:

For every A ~ D

1. compute U such that Cn(U) = CnMon(A)(W) (the theory CnMon(A)(W) is infinite, however U is finite - see [Marek and Truszczyriski, 1993]),
2. compute B = {d E A : U 1- p(d)}, and let C = {{3 1\ T a:r:; (3 E B},
3. compute E = { a:':;(J E D: W U C U {,B, 1} If ..L},
4. if E = A then output ( Cn(U), Cn(W U C)) as a constrained extension of (D, W).

The complexity of the above algorithm is determined by the number of calls to a propositional consistency checking procedure. Assume that the number of defaults in Dis n. Given A~ D, we need at most n 2 calls to such a procedure to compute U, at most n calls to compute B and n calls to compute E. Hence, for every A ~ D, we need O(n 2 ) calls to a propositional consistency checking procedure, and O(n 2 2n) calls to such a procedure for the whole algorithm.

We have the following complexity result (see [Garey and Johnson, 1979] for a discussion of complexity classes).

Theorem 4.1 The following problems:

• IN-SOME Given a finite default theory (D, W) and a formula cp, decide if cp is in some constrained exten­ sion for (D, W),
• NOT-IN-ALL Given a finite default theory (D, W) and a formula rp, decide if there is a constrained extension for (D, W) not containing rp,
• are 1:f -complete. The problem

IN-ALL Given a finite default theory (D, W) and a for­ mula cp, decide if cp is in all constrained extensions of (D, W),

is IIf -complete.

Proof. To verify that a formula cp belongs to some (does not belong to all, resp.) constrained extensions of (D, W), we can nondeterministically guess a set of defaults A ~ D, verify that ( Cn(U), Cn(W U C)) is a constrained extension for (D, W) (U and C are as de­ fined in the above algorithm) and verify that U r cp (U If cp, resp.), what requires one more call to a propo­ sitional consistency checking procedure. It follows that the problems IN-SOME and NOT-IN-ALL are in ~f. Since the problem NOT-IN-ALL is in ~f, the problem IN-ALL is in IIf. Observe next that S is an extension for a normal default theory if and only if (S, S) is a con­ strained extension for this theory (see [Schaub, 1992]). Hence, the hardness of all three problems in their re­ spective complexity classes follows from the fact that the problems IN-SOME, NOT-IN-ALL and IN-ALL for extensions of normal default theories are ~f -hard and IIf-hard, respectively (see [Gottlob, 1992]). D

5 Connections between constrained and rational default logics

First, we will show that rational extensions determine constrained extensions. That is, we will show that for every rational extension Sofa default theory, there is T such that ( S, T) is a constrained extension of this theory.

Theorem 5.1 Let E be a rational extension for a de­ fault theory (D, W) and let A E MA(D, W, E) be such that E = CnMon(Al(W) (= Cn(W U c(A))). Let C = Cn(EUj(A)) (= Cn(WUc(A)Uj(A))). Then (E,C) is a constrained extension of ( D, W).

Proof. We need to show that T(C) = (E, C). We will prove first that pair (E, C) satisfies CEI- CE3 with re­ spect to C. The conditions CEI and CE2 are obviously satisfied. Now, let a default d = Ot:~(J be such that a E E and CU{,B,1} is consistent. Since CU{,B,1} is consis­ tent, then EU j(Au { d}) = EU j(A) U {,B} is consistent. Moreover, since p(A) ~ CnMon(A)(W) = E and a E E, we havep(AU{d}) = p(A)U{a} ~ E = CnMon(A)(W) ~ CnMon(Au{d}l(W). Thus, (AU {d}) E A(D, W,E). By the maximality of A, d E A. Hence, 1 E c(A) ~ E and {,8,1} ~ c(A) Uj(A) ~C. It follows that 1 E E and ,B 1\1 E Cn(C) = C and CE3 holds.

Now, we need to prove that if a pair (S, T) satis­ fies CEI- CE3 with respect to C then E ~ S and C ~ T. Let us notice that, since c(A) U j(A) ~ C, for d = 0t:~(J E A, C U {,8,1} = C. By ASI, j(A) = 0 or j(A) U E is consistent. Thus, we have either C = Cn(E U j(A)) is consistent or A= 0 (let us recall that we do not consider justification-free defaults). In both cases for d = Ot:~(J E A, C U {,B, 1} is consistent.

Thus, CE3 implies that S is closed under inference rules from Mon(A). Moreover, by CEI, W ~Sand, by CE2, S is closed under propositional provability. It follows that E = CnMon(A)(W) ~ S. We have p(A) ~ E ~ S. So, it follows from CE3 and CE2 that j(A) U c(A) ~ T. Since, by CEI, W ~ T and, by CE2, T = Cn(T), then C ~ T and we are done. 0

The converse statement is not true. Every default the­ ory has at least one constrained extension [Schaub, 1992] and there are default theories that do not have rational extensions [Mikitiuk and Truszczyriski, 1993]. We will show that for seminormal default theories an exact one­ to-one correspondence between rational and constrained extensions can be established. But first we .will prove an auxiliary result.

Theorem 5.2 Let (S, T) be a constrained extension of a default theory (D, W) . Then GD'g·r) E A(D, W, S) .

Proof. It follows from Theorem 3.1 that T = Cn(S U j(GD'g·r))). IfT is consistent then j(GD'g'Tl)uS is also consistent. If T is inconsistent then it follows from the definition of GDtg·r) that GDtg·r) = 0, so j( G Dtg·r)) = 0. Thus, in both cases A~l holds.

According to the definition of GD'g·r), p(GD'g·r)) ~ M (GD(S ,T)) s. By Corollary 3.2, s = Cn on 7 D (W) . Hence, AS2 also holds. D

Theorem 5.3 Let (S, T) be a constrained extension of a seminormal default theory ( D, W). Then S is a rational extension of(D,W) andGD'g·r) E MA(D,W,S).

Proof. By Theorem 5.2, GD'g·r) E A(D, W, S) and, by M (GD(S,T)) Corollary 3.2, S = Cn on 7 v (W). Thus, we need to prove the maximality of GD'g·r) in A(D, W, S) only. Since every default in D is seminormal, we can rewrite the definitions of GD'g·r), Dr and C(D, S, T) as

Let us denote G D'g·r) by A. Since, by Corollary 3.4, S = Cn°T(W) and T = Cn(W U C(D,Cn°T(W),T)), we get T = Cn(W U j(A)).

Let us consider now a default d = Ot : ~(J E D \A. We have either a i. S = Cn Mon(A) (W) or T U {,B} is incon­ sistent. If T U {,8} is inconsistent then W U j(A) U {,8} = WUj(AU{ d}) is inconsistent and the set AU{ d} does not satisfy ASI (since dis seminormal, j({d}) ::j; 0). If a i. CnMon(A)(W) then CnMon(Au{d})(W) = CnMon(A)(W) and p(A U {d}) = p(A) U {a} ~ CnMon(Au{d})(W), so AU{ d} does not satisfy AS2. By Proposition 4.2 from an extended version of [Mikitiuk and Truszczynski, 1993], A E MA(D, W, S) and we are done. 0

Schaub ([1992]) proved that every default theory has a constrained extension, so we have the following corollary (proved first by other methods in an extended version of [Mikitiuk and Truszczyriski, 1993]).

Corollary 5.4 Every seminormal default theory has a rational extension. 0

6 The case of justification-free defaults

We close this paper with a remark that constrained de­ fault logic can be extended to cover the case of default theories that may contain justification-free defaults. To this end, one has to replace CE3 by the following two conditions:

CE31 For any default cd::(3 E D, if a E S' and T U {;3, 'Y} is consistent then 1 E S' and {3 1\ 1 E T'.

CE32 For any default ""~ E D, if a E S' and T U b} is consistent then 1 E S'.

The definitions of GD)]·Tl, Dr and C(D,S,T) must be modified in the same way. Under such modifications all results presented in this paper, except for Theorem 5.1, remain true. Moreover, the following, slightly mod­ ified version of Theorem 5.1 holds (the assumption of consistency of a rational extension is added).

Theorem 6.1 Let E be a consistent rational extension for a default theory (D, W) and let A E MA(D, W, E) be such that E = CnMon(Al(W) (= Cn(W U c(A))). Let C = Cn(E U j(A)) (= Cn(W U c(A) U j(A))). Then (E,C) is a constrained extension of (D, W).

Proofs of these results will be included in a full version of the paper.

7 Conclusions

In this paper we showed that constrained and rational default logics are closely related. While Reiter's default logic and constrained default logic coincide on the class of normal default theories, rational and constrained de­ fault logics coincide on a much wider class of seminormal default theories.

We showed that basic problems of reasoning with con­ strained extensions are complete for the second level of the polynomial hierarchy (with the exception of the ex­ istence of an extension problem, which is trivially in P). We also proposed algorithms to compute constrained ex­ tensions.

Constrained default logic was originally introduced only for default theories without justification-free de­ faults. In the paper, we proposed a modification of the original definition of Schaub, which allows for defaults to be justification-free. Under our definition, all major properties of constrained default logic remain true.