On the Complexity of Model Checking for Propositional Default Logics: New Results and Tractable Cases

1 Introduction and Overview of Results

The complexity of default reasoning is already well un­ derstood, however, in search of model-based represen­ tations, the complexity of the model checking problem instead of the inference problem needs to be analysed.

As Halpern and Vardi [1991) argue, model checking is a beneficial alternative simplifying reasoning tasks (for instance, in classical propositional logic, model check­ ing can be done using an easy polynomial algorithm, however reasoning is coNP-complete) and allowing for representing the agent's knowledge as a semantic struc­ ture instead of a collection of formulae and additionally, this approach introduces a kind of closed-world assump­ tion. Furthermore, the complexity of model checking is closely related to the notion of representational succinct­ ness [Gogic et al., 1995) of non-monotonic formalisms.

1.1 Complexity of Inference

Gottlob [1992) and Stillman [1992) showed that the com­ plexity of brave {cautious) reasoning, i.e. to decide, given a formula f and a default theory (D, W).P iff is in at least one (all) extension(s) of (D, W) is :E2 -complete (llf­ complete), even in case of normal and prerequisite-free default theories, and even if f is a single literal. For related results, see [Papadimitriou and Sideri, 1992].

The complexity decreases one level if disjunction-free default theories are considered, i.e. only conjunctions of literals and negated literals are allowed. Kautz and Sel­ man [1991) dealt with the inference problem for such theories: Brave reasoning (for disjunction-free formulae) is NP-complete, even in the case of normal default theo­ ries (although finding an extension is polynomial in that Georg Gottlob*

*This work was supported by the Austrian Science Fund Project N Z29-INF.

Institut fiir Informationssysteme Technische Universitat Wien A-1040 Vienna, Austria

gottlob@dbai. tuwien.ac.at

case) and even if the formula to be inferred of at least one extension is a single literal. If W is a Horn theory, NP­ completeness holds even in the case of prerequisite-free normal default theories [Stillman, 1990).

1.2 Complexity of Model Checking

An interpretation is a model of a default theory iff it sat­ isfies at least one extension of the theory. Liberatore and Schaerf [1998) show that model checking is :Ef -complete, even for semi-normal prerequisite-free default theories. In the case of normal default theories, model checking is easier than the corresponding reasoning task - they show that the problem is in .:lf and .:lf[O(log n))-hard, and coNP-complete if defaults are also prerequisite-free.

In general, model checking suffers from two sources of hardness: On the one hand there are 21°1 (with G = { d I M f= c( d)}) possible sets of generating defaults , and the other source of intractability is the hardness of propositional inference. In case of normal default theo­ ries, given a particular model, only one subset of G needs ~o b.e ~onsidered and therefore the initial guessing stage IS ehmmated. In Theorem 4.1 we show with a non-trivial membership proof that this problem is in .:lf[O(logn)J and hence due to earlier results .:lf[O(logn))-complete. To obtain this theorem we improve techniques of Gott­ lob [1995) for guessing data-structures.

If the defaults are restricted in such a way that propo­ sitional satisfiability and inference are polynomial, the other source of intractability is affected and the problem is due to the necessary guessing of generating defaults NP-complete. If such a default theory is restricted to normal defaults, complexity of model checking is even polynomial. Therefore, in Chapter 5, we introduce the class of default theories in extended Horn normal form (abbreviated as "EHNF default theories"), a class con­ taining disjunction-free default theories, for which model checking is still one level easier than for arbitrary default theories. A default theory (D, W) is in EHNF iff W and all elements of each justification are disjunctions of Horn theories, each prerequisite is a conjunction of dual Horn theories, and each consequent is a Horn theory. This is an ample class of default theories with a tractable model checking problem and hence very useful in practical ap­ plications.

1.3 Weak Model Checking and AEL

In Chapter 6 we recall the notion of weak extensions and show that weak model checking, i.e. deciding if an interpretation satisfies at least one weak extension of a default theory, is, due to the non-constructive nature of the problem, even Ef -complete for normal default theo­ ries and hence strictly harder than model checking. This issue is also connected to the fact that no modular trans­ lation from default lo&ic into autoepistemic logic (AEL) exists [Gottlob, 1995bj, since prerequisites are treated in a very different way. The objective parts of stable ex­ pansions (N -expansions) of the translated default theory correspond to weak extensions (extensions) of the de­ fault theory, therefore we obtain the complexity of model checking for AEL ( nonmonotonic logic N) in Chapter 7.

1.4 Summary

In Table 1 and Table 2 a summary of our results for model checking and weak model checking with Reiter's default logic is presented (the results already present in [Liberatore and Schaer£, 1998] are marked with*)· Ad­ ditionally, the main contributions of this paper are:

• We solve the open problem of the exact complexity of model checking for normal default theories.
• We introduce a new ample class of default theories with a tractable model checking problem.
• We show that weak model checking is Ef -complete, even if restricted to normal default theories.
• We generalize these results to Ef -completeness of model checking with AEL and N.
• Finally, in Chapter 8 the complexity results of model checking are used to draw some interesting conclu­ sions in translatability issues.

2 Basic Concepts

A propositional def'ault theory [Reiter, 1980] is a pair (D, W) where W is a finite set of propositional sentences and D is a finite set of defaults. Whenever we use the term default theory in the rest of the paper, we mean propositional default theory.

A default d is a configuration of the form p(d) :/3t, . .. ,/3n c(d) where p(d), /3i, c(d) are propositional sentences. p(d) is called the prerequisite of d, the (non-empty) set {/31, . . . , f3n} is referred to as the justification of d and de­ noted by j (d); c( d) is called the consequent of the default d. For convenience we define c(H) = {c(d) IdE H} and if j(d) is a singleton we identify it with its only element.

Since Reiter's original definition of extensions [1980] a great number of equivalent characterizations has been introduced. In this paper we normally use a finite quasi­ inductive characterization, based on the operator BD due to Marek and Truszczynski [1993].

We define cons(A) as usual as {~ I A f= ~}. Let H be a subset of D: Ho = 0, Hk+l =

As we limit ourselves to finite default theories, it can easily be seen that at latest after IDI steps a fixed point has been reached. E = cons(W 1\c(HIDI)) is an extension of (D, W) iff H = HIDI· Every extension is of the form E = cons(W U c(GD(D, E))) with GD being called the generating defaults of the extension.

In a normal default theory j(d) = c(d) for each default. A semi-normal default theory is a theory in which each j(d) is of the form f(d) 1\ c(d) where f(d) are arbitrary propositional formulae.

Definition 2.1 An interpretation {valuation) M is a model of {D, W) iff M is model of at least one (con­ sistent) extension of (D, W).

Whenever we use the term model we refer to propo­ sitional Herbrand model. The Model Checking problem for default logic is to decide, given an interpretation M and a default theory (D, W), if M f= (D, W).

Short Review of Relevant Complexity Con­ cepts: The notion of completeness we employ is based on many-one jolynomial transformability. Recall that the classes ilk , Ef and ITf of the polynomial time hi­ erarchy (PH) 1 are defined as .6.[ = E[ =IT[ = P and for all k ;?: 0, .6.f+l = pEf, Ef+l = NPEf, ITf+l = co-Ef+l. In particular, NP = Ef,coNP = ITf and .6.f = pNP (see [Papadimitriou, 1993] for details) . ~f is the class of decision problems that are solvable in poly­ nomial time on a deterministic oracle Thring machine calling an NP-oracle polynomially often.

The classes .6.f have been refined, depending of how many oracle calls are needed: Of special interest in this paper is the class .6.f[ 0 (log n)], also known as pNP[O(Iog n)] - this is the class of decision problems solv­ able with a logarithmic number of calls to an NP-oracle.

A survey on already known complexity results for sev­ eral non-monotonic logics can be found in [Cadoli and Schaer£, 1992].

1 We always implicitly assume that P '# NP and that the PH does not collapse.

3 Some Useful Tools

Due to lack of space, some proofs in the following chap­ ters are sketched or omitted.

Lemma 3.1 Let (D, W) be a normal default theory. If W 1\ c(D) is consistent, then there are no mutually in­ compatible defaults and thus only one generating set.

Lemma 3.2 Let (R, W) be a monotonic rule-system (or a normal or justification-free default theory) where W and the consequents bi of R = { ~, ... t} are jointly consistent. Then the statement: "At least k rules do not fire" is equivalent to "It is possible to choose a set B ~ R with IBI = k and k interpretations I1, ... Ik in such a way that 'v'j(1 ~ j ~ k): I; f= W, 'v'j 'v'b E R\B: I; F= b, 'Ia E B 3j : I; Pf: a."

The following proposition formalizes a technique (bi­ nary search) that is well known in the literature [Wagner, 1990; Papadimitriou, 1993].

Proposition 3.3 Let a(I1, . .. , In) be a function of n instances of a problem and a(I1, ... , In) be polynomially bounded inn, i.e. a{Il, . .. ,In) ~p(n) . Iftheproblem of deciding a(h, . . . ,In)~ r (or a~ r) is in NP, then the computation ofa(Il , ... ,In) is in ~f[O(logn)J .

Proposition 3.4 M is a model of a default theory (D, W) iff there exists an extension of (D, W) gener­ ated by a subset G1 ~ G where G ={dIM f= c(d)}. In a normal default theory at most one extension E such that M f= E exists.

Proposition 3.5 Let E be an extension of the default theory (G, W) and G ~D. Then, E is an extension of (D, W) iff for each default in D\G it holds that W 1\ c(GD(G,E)) Pf: p(d) or W 1\ c(GD(G,E)) f= -,f3i for at least one i with f3i E j (d) .

4 Model Checking for Normal Default Theories is 6.f[O(logn)]-complete

Theorem 4.1 Let M be an interpretation and (D, W) be a normal d~ault theory. Deciding whether M f= (D, W) is in ~2 [O(logn)J .

Proof. We describe a Turing machine M which decides this problem in polynomial time using an NP-oracle for only O(log n) times where n is the number of defaults. M works in four steps.

Step 1: M rejects if M Pf: W. Let G ~ D be the set of all defaults d with M f= c( d). This step determines G by sorting out all unwanted ("bad") defaults B = D\G. None of the defaults of B shall fire or M is not a model of this extension (Proposition 3.4). Checking if M f= W and constructing G can be achieved in polynomial time. In the following, let m be the cardinality of G.

Step 2: M computes the cardinality of the set G1 of generating defaults of the extension, i.e. those defaults in G which are applicable because their prerequisites can be inferred; due to Lemma 3.1, G1 is unique. M assumes that E = cons(W U c(Gl)) is an extension, and in step 3 and 4 M will verify if no "bad" defaults have to be used. To compute the cardinality of G1 , M determines the number IG2I = IG\G1I of defaults that do not fire. We can identify (D, W) with a monotonic rule-system (R, W) in which all consequents are jointly consistent.

Claim The problem to decide if at least r rules of a monotonic rule-system (in n rules) do not fire is in NP.

Proof of Claim: Machine M guesses a data-structure (�~,{Ill· · ·,Ir}) with I�~I = r . �~ is a set of de­ faults (rules), the I;(1 ~ j ~ r) are interpretations, and proves in polynomial time (using the monotonic rule system syntax of Lemma 3.2): 'v'j : Ij f= W , 'v'j 'v'b E R\�~ : Ij f= b, 'v'a E �~ 3j : Ij Pf: a. Due to Lemma 3.2, this is equivalent to the question if at least r rules do not fire, i.e. if IG2I ~ r . 0

From Proposition 3.3 the number t of defaults which do not fire can be computed in polynomial time using O(logm) calls to an NP-oracle. After concluding this step M knows IG2I = t, hence IG1I = m- t.

Step 9: If it can be shown that WUc(G1 ) f= p(d) and W 1\c(Gl)/\j(d) is consistent for at least one dE B, then G1 is not a set of generating defaults and the given inter­ pretation M is not a model for (D, W) (Proposition 3.5) . Two types of "bad" defaults need to be distinguished: B1 is consisting of defaults in which the prerequisites are not applicable, formally B1 = {dEB I W U c(Gl) Pf: p(d)} ; and B2 = B\B1. M determines the exact number u of defaults in B1 and in the fourth step will check for each default in B2, if the justifications are consistent with W 1\ c(G1) (after guessing the right G1 and Bl).

Claim The problem to decide, given IG1I, if the number of defaults in B1 is at least s, is in NP.

Proof of Claim: For a given s, M guesses a data­ structure (G1 ~ G, {N1, ... ,Nt}, B~ ~ B, {01, . . . , Os}) with IG1I = m- t, IBU =sand Ne and Oy are inter­ pretations. Now M proves:

• 'v'd E G2 3Ne(1 ~ e ~ t) : Ne Pf: p(d) , 'v'e : Ne F W 1\ c(Gl) (In step 2 M was provided with the in­ formation of the cardinality of G1 , therefore M now just has to guess a G1 of suitable cardinality and check if it is the right one.).
• 'v'd E B~ 30y(1 ~ y ~ s) : Oy Pf: p(d) , 'v'y : Oy F= W 1\ c(G1). If it is possible to choose the Oy this way, then there are at least s not applicable prereq­ uisites of defaults, hence IB11 ~ s (This statement is equivalent to Vd E B~ : W U c(Gl) Pf: p(d) .).

Both steps can be concluded in polynomial time and are due to the initial guess in NP. 0

Hence, u = IB1I can be computed with flog(n- m)l oracle calls (Proposition 3.3).

Step 4: In the previous steps M has determined the cardinality of B1 and G1 . Now M finally has to check that W 1\c(Gl) 1\j(d) is inconsistent for all defaults dE B2 (if yes, then G1 is a generating set). To this aim, let us show that the converse problem is in NP and introduce a machine N solving it.

Claim The problem to decide if W 1\ c( G) 1\ j (d) is con­ sistent for at least one d E B 2 , given the cardinality of G1 and B1, is in NP.

Proof of Claim: Machine N guesses a data-structure (G1 ~ G, {N1, ... ,M}, B1 ~ B, {P1, ... , Pu}, Q) with IG1I = m - t and IB1I = u. Now N tests in polynomial time:

• Vd E G2 3Ne(1 ~ e ~ t) : Ne Pf: p(d), Ve : Ne F W A c(G1).
• Vd E B1 3Pz(1 ~ Z ~ u) : Pz Pf: p(d), Vz : Pz F W A c(G1).
• Now N just needs to prove that 3d E B2 : Q I= W Ac(GI)Ac(d) (with c(d) = j(d)). This states the fact that there is a default which is consistent with cons(W U c(GI)).

All steps can be concluded in polynomial time and are due to the initial guess in NP. 0

This means that the output yes of machine N is achieved iff there exist defaults of B2 which fire (with guessing the only suitable G1 and B1 , and Q). The converse problem therefore needs merely one (negative) oracle call.

Hence, step 1 to 4 are feasible in polynomial time with !log( m( n - 1)) l + 1 = O(log n) calls to three different oracles in NP. With standard techniques these three oracles can be replaced with a single oracle. 0

5 EHNF Default Theories

A default theory (D, W) is disjunction-free, if W, all p( d), all elements of each j (d), and all consequents c( d) are conjunctions of (negated and not negated) literals. A Horn clause is a disjunction of literals with at most one positive literal. A Horn theory is a conjunction of Horn clauses. A dual Horn clause is a conjunction of literals containing at most one negative literal. A dual Horn theory is a disjunction of dual Horn clauses.

Definition 5.1 A default theory (D, W) is in extended Horn normal form (EHNF) iff W and all elements of each j(d) are disjunctions of Horn theories, each p(d) is a conjunction of dual Horn theories, and each conse­ quent c(d) is a Horn theory. If (D, W) is normal, then, trivially, the only element of each j(d) is only a Horn theory, too.

This is an ample class of default theories contain­ ing many restricted cases with an intractable reason­ ing problem even for normal default theories. However, model checking turns out to be tractable for normal EHNF default theories.

Theorem 5.2 Let M be an interpretation and (D, W) an EHNF default theory. Deciding whether M I= (D, W) is in NP.

Proof. (Sketch) Guess G ~ D, compute GIDI, show that G = GIDI and M I= W A c(G). All satisfiability checks are of the form sat(W A c(G) A f3i) and due to the deduction theorem, the inference checks are equiv­ alent to F ..., W V ·c( G k) V p( d). All these checks are polynomial, because satisfiability of a Horn theory and tautology checking of a dual Horn theory are tractable;

furthermore, the question sat(h V ... V fm) is equiva­ lent to sat(h) or ... or sat(fm) and taut(h A .. . A fm) is equivalent to taut(h) and ... and taut(fm); there­ fore each check can be splitted to a quadratic number of checks in the number of disjunctions of W and p( d) resp. j(d) (However, if we would have allowed the con­ sequents to be disjunctions of Horn theories, too, the number of disjunctions would be exponential in the in­ put length, even if only a logarithmic number of defaults would be allowed to have this form.). o

Theorem 5.3 Let M be an interpretation and (D, W) be an EHNF default theory. Deciding whether M F (D, W) is NP-hard, even if (D, W) is prerequisite-free, semi-normal, disjunction-free and all consequents are single literals.

Proof. (Sketch) Use a reduction of 3SAT. Transform F(tl, 0 0 °, tm) = FlA. 0 .AFiA. 0 .AFn with Fi =Xi! VXi2 v x · into (D W) with W = 0 D = U { : usl\~t. =t·l\~u. }U 13 ) ' k ~tic ' -,Uk U . { : f(zil)l\~y. :f(z··)l\~y. : f(zis)l\~y. Jli} with f(x .. ) = l ...,tli ' ...,y, ' ...,Yi ' Yi "1 ·tk AUk if Xij = ·tk and f(xii) = ·uk A tk if Xij = tk. Intuitively, the new atoms uk are introduced because the empty set shall be a model regardless to which evaluation of (t1, ... , tm) satisfies F. Each extension has to contain, for each i, either 'Yi or Yi; iff F is satisfiable it can contain all 'Yi, i.e. F is satisfiable iff 0 F (D, W). 0

Instead of using a prerequisite-free default theory, in the above proof an "almost" normal default theory with prerequisites could be used, however the first set of de­ faults of the above proof cannot be presented as nor­ mal defaults unless using weak extensions (Chapter 6) or disjunctive default logic of Gelfand et al. [1991] (with Vk: ·uki'tk)·

We show that in the case of normal EHNF default the­ ories, model checking is tractable, and moreover belongs to the hardest problems in P w.r.t. logspace-reductions.

Theorem 5.4 Let M be an interpretation and (D, W) be an EHNF normal default theory. Deciding whether M I= (D, W) is in P.

Proof. We describe the algorithm given in Figure 1: In the while loop, each default of the set G is tested and G1 is created. To this aim, the check F ·WV·c(GI)Vp(d), where W = W1 V ... VWk V ... VWdw (each Wk is a Horn theory, hence the negation a dual Horn theory) and each p(d) = Pl(d)A ... Ap1(d)A ... Apdp(d)(d), is splitted to dwx dp tautology checks of dual Horn theories, which is poly­ nomial (the boolean functions taut( dualH orntheory) and sat( H orntheory) are assumed to be given). If x = dw x dp, then each check was successful and the de­ fault is added to G1 . After at most n steps, all defaults with applicable prerequisites w.r.t. G have been added to the generating set G1 of (G, W). To show, that this is a generating set of (D, W), check that no default of D\G is applicable, i.e. either the prerequisite cannot be inferred or the justification (which is in case of normal EHNF default theories only a singleton and only a Horn

Input: M, an EHNF normal default theory (D, W) . Result: "Accept" if M f= (D, W); "Reject" otherwise. begin G := {dl M f= c(d)}; G1 := 0; n := IGI; B := D\G; dw :=number of disj . of Horn theories in W; i := 0; while i $ n do i := i + 1; for each d E G do dp :=no. of cnj. of dual Horn th. inp(d); x := 0; fork := 1 to dw for l := 1 to dp iftav.t(-,W.~: V ...,c(Gl) V p,(d)) then x := x + 1; rof; rof; if x = dw x dp then G1 := G1 U {d} and G := G\{d}; od; od; for each d E B do dp :=no. of cnj . of dual Horn th. inp(d); x := 0; y := 0; for k := 1 to dw for l := 1 to dp if tav.t(-,Wk V -,c(Gl) V Pl{d)) then x := x + 1; rof; if sat(Wk I\ c(Gl) I\ j(d)) then y := 1; rof; if x = dw x dp and y = 1 then reject and halt; od; accept; end.

theory) is not consistent, which is implemented in the for each d E B loop. If x = dw x dp (expressing that the prerequisite is inferred) and y = 1 (expressing that sat(W 1\ c( G 1) 1\ j (d)), because one disjunction is satisfi­ able, i.e. the justification is consistent with Gt), then at least one of the "bad" defaults has to be used and M is not a model. 0

Theorem 5.5 Let M be an interpretation and (D, W) be an EHNF normal default theory. Deciding whether M F= (D, W) is P-hard, even if (D, W) is either disjunction-free or prerequisite-free.

Proof. In the case of disjunction-free default theories use a reduction of the P-complete problem of reasoning in propositional not-free logic pi~gramming [Dantsin et al., 1997]. Let (D, W) be the default theory where each clause b f-- a1 1\ ... 1\ an of P is translated into a normal default a,A ... Aan :b and the default !2/l. is added which is b ~g feasible in logarithmic space since only one new default is added. Then Mfull f= (D, W) iff g is in the sta­ ble model of P. In the case of prerequisite-free EHNF default theories use a reduction of the (essentially the same) P-complete problem if a Horn theory is satisfi­ able and use the default theory (0, W) with W being a Horn theory. 0

If a normal default-theory is disjunction-free and prerequisite-free the problem no longer remains P-hard and can be shown to be in non-deterministic logspace.

6 Complexity of Weak Model Checking

Let (D, W) be a default theory and H, J ~ D . J = {dEDI WUc(H) f= p(d), V/3i E j(d) Wuc(H) ~ ...... f3i}. E = cons(W 1\c(H)) is called a weak extension of (D, W) iff H = J (see, e.g. [Marek and Truszczynski, 1993]) and H is the weak generating set of this weak extension.

In prerequisite-free default theories extensions and weak extensions coincide. M is a weak model of (D, W) iff M is a model of at least one (consistent) weak ex­ tension. Every extension is a weak extension, therefore every model is a weak model. However, the converse does not hold, since not every extension is a subset of a weak extension.

Theorem 6.1 Let M be an interpretation and (D, W) be a default theory. Deciding if M is a weak model of (D, W) is ~f -complete, even if (D, W) is semi-normal and prerequisite-free.

Lemma 3.1 does not hold for weak generating sets, and for normal default theories it is neither sufficient to look at the largest weak generating set nor at the smallest w.r.t. G, hence an exponential number of subsets needs to be considered:

Theorem 6.2 Let M be an interpretation and (D, W) be a normal default theory. · Then the problem to decide if M is a weak model of (D, W) is ~f -complete.

Proof. (Sketch) We use a transformation from the ~f­ complete problem QBF 2,3 , i.e. the problem of checking whether there exists an evaluation of the Pi E P , such that for each evaluation of the qj E Q F(P, Q) is true, into (D, W) with W = 0, D =

with w and v being new atoms. In the full paper we show that 0 f= (D, W) iff FE QBF2,3 · o

Theorem 6.3 Let M be an interpretation and (D, W) be a normal prerequisite-free default theory. Then the problem to decide if M is a weak model of (D, W) is coNP -complete.

Theorem 6.4 Let M be an interpretation and (D, W) be an EHNF default theory. Then the problem to decide if M is a weak model of (D, W) is NP -complete even if the theory is disjunction-free and either semi-normal and prerequisite-free or normal, and P-complete if the theory is prerequisite-free and normal.

7 Complexity of Model Checking with AEL and N

An interpretation M in the language .C is a propositional AEL (N)-model of a set of premises in .Cm (.C extended with a modal operator) iff M satisfies an objective part of at least one stable expansion (N-expansion) .

Theorem 7.1 Let ~ be a set of premises in .Cm and M be an interpretation in .C. Deciding if M is a proposi­ tional AEL (N)-model is ~f -complete.

Proof. Hardness: Weak extensions (extensions) of a default theory correspond to objective parts of stable ex­ pansions (N -expansions) of the translated theory [Marek and Truszczynski, 1989; 1993].

Membership: In [Gottlob, 1992] it is shown that de­ ciding if a formula is not occuring in all extensions is in ~f (using the finitary characterization of Niemela [1991] with modal subformulae) . Consider the propositional language { a1 , . . . , an} and any model M containing some of these atoms. Then M FE iff E ~ l1 V ... V ln with l; = --.a; if a; E M and li = ai if ai ¢ M. 0

8 Translatability Issues

A pfm-function f : A 1--t B is a function embedding for­ malism A into formalism B fulfilling the additional crite­ ria of polynomiality, faithfulness (extensions/expansions coincide in some way) and modularity (a propositional subtheory can independently be translated) [Janhunen, 1998; Gottlob, 1995b].

We refer to [Eiter and Gottlob, 1995] for details of disjunctive logic programming (DLP) (reasoning is as hard as in default logic) and to [Inoue and Sakama, 1993] for results that DLP can be pfm-embedded into default logic.

Theorem 8.1 Unless the PH collapses, there exists no pfm-function embedding default logic, normal default logic or disjunction-free default logic into DLP.

Proof. Assume the existence of a pfm-function embed­ ding default logic into disjunctive logic progr_amming; then a given default theory would admit the same mod­ els as a pfm-translation into a corresponding disjunctive program. However, as model checking with disjunctive logic programming is only coNP-complete, this implies that ~f = coNP. Contradiction. 0

9 Future Research

We plan to investigate the complexity of model checking for further interesting variants of default logic and other nonmonotonic logics. We hope that this will allow us to clarify a number of translatability issues, akin the result of Chapter 8.

Acknowledgments

The authors are grateful to C. D. Koutras and R. Rosati for reading an earlier version of this paper and suggesting improvements, and to the referees for several comments.