Semantics and Complexity of Abduction from Default Theories^{∗}

Thomas Eiter^{⋆}, Georg Gottlob^{⋆}, Nicola Leone^{⋆,⋄}

⋆Christian Doppler Laboratory for Expert Systems Information Systems Department, TU Vienna, Paniglgasse 16, A-1040 Wien, Austria

                 email: (eiter|gottlob|leone)@dbai.tuwien.ac.at

⋄Istituto per la Sistemistica e l’Informatica – C.N.R. c/o DEIS – UNICAL, 87036 Rende, Italy

                         email: nik@si.deis.unical.it

Abstract

Abductive reasoning (roughly speaking, find an explanation for observations out of hypotheses), has been recognized as an important principle of common-sense reasoning. Since logical knowledge representation is commonly based on nonclassical formalisms like default logic, autoepistemic logic, or circumscription, it is necessary to perform abductive reasoning from theories (i.e. knowledge bases) of nonclassical logics. In this paper, we investigate how abduction can be performed from theories in default logic. In particular, we present a basic model of abduction from default theories. Different modes of abduction are plausible, based on credulous and skeptical default reasoning; they appear useful for different applications such as diagnosis and planning. Moreover, we thoroughly analyze the complexity of the main abductive reasoning tasks, namely finding an explanation, deciding relevance of a hypothesis, and deciding necessity of a hypothesis. These problems are intractable even in the propositional case, and we locate them into the appropriate slots of the polynomial hierarchy. However, we also present known classes of default theories for which abduction is tractable. Moreover, we also consider first-order default theories, based on domain closure and the unique names assumption. In this setting, the abduction tasks are decidable, but have exponentially higher complexity than in the propositional case.

1 Introduction

Abductive reasoning has been recognized as an important principle of common-sense reasoning having fruitful applications in a number of areas such diverse as model-based diagnosis [46, 45, 16], speech recognition [30], maintenance of database views [34], and vision [12]. Various formalizations of abductive reasoning have been proposed, among which set-covering based approaches [43, 7] and logic-based approaches [46, 45, 15, 16] are well-known. These two types basically differ in the way domain knowledge is represented. Roughly, in the set-covering approach, the domain knowledge is represented by a function e which maps subsets X of hypotheses, which are atomic entities representing all possible disorders, to subsets e(X) of manifestations, i.e. observed symptoms. The set e(X) can be seen as the explanation power of X; if X explains all manifestations M, i.e. e(X) = M, then X is an abductive explanation. On the other hand, in the logic-based approach the domain knowledge is represented by a logical theory T in some language. A subset X of hypotheses is an abductive explanation, if T augmented by X derives the manifestations M. For a more detailed comparison of these and other approaches to abduction, see [22].

∗A short and preliminary version of this paper appeared in the Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence (IJCAI-95), C. Mellish ed, pp. 870–876, AAAI Press, 1995.

Until now, mainly logical abduction from theories of classical logic has been studied. However, logical knowledge representation is commonly based on nonclassical formalisms like default logic, autoepistemic logic, or circumscription. Thus, in such situations it is necessary to perform abductive reasoning from theories (i.e. knowledge bases) of nonclassical logics; in a sense, this is orthogonal to what is known as hybrid reasoning, i.e., reasoning on a knowledge base built using different formalisms [2].

Since default logic [52] is one of the most used logical knowledge representation languages that emerged in the field of nonmonotonic reasoning (cf. [53, 18]), it is important to investigate how abduction can be performed from theories ⟨W, D⟩ in default logic. In this paper, we address this problem. We start by first considering some motivating examples; they show that abductive reasoning in default logic is needed, and lead us towards a formal model of abduction from default theories.

Example 1 Consider the following set of default rules, which represent some knowledge about Bill’s skiing habits:

D = \{ \frac{: ¬skiing(Bill)}{¬skiing(Bill)}, \frac{weekend : ¬snowing}{skiing(Bill)} , \frac{: ¬snowing}{¬snowing} \} .

The defaults intuitively state the following: Bill is usually not out for skiing; on the weekend, Bill is usually out for skiing, unless it is snowing; and usually, it is not snowing. For the certain knowledge W = { weekend } (encoding that it is Saturday or Sunday), the default theory T = ⟨W, D⟩ has one extension which contains ¬snowing and skiing(Bill).

Suppose now that we observe that Bill is not out for skiing (which is not consistent with the extension). Abduction means to find an explanation for this observation, that is, to identify a set of facts, chosen from a set of hypotheses, whose presence in the theory at hand would derive the observation ¬skiing(Bill), i.e., cause that ¬skiing(Bill) is in the extension. We find such an explanation by adopting the hypothesis snowing. Indeed, if we add snowing to W, we obtain for the default theory T′ = ⟨{ weekend, snowing }, D⟩ a single extension, which contains ¬skiing(Bill). We say that snowing is abduced from the observation ¬skiing(Bill), or that it is an abductive explanation of ¬skiing(Bill).

Observe that the description of the above situation requires the specification of some default properties that cannot be represented properly in classical logic.

Example 2 Assume that information about a computer network is represented using default logic. The default theory T = ⟨W, D⟩ described next comprises in a simplified setting knowledge

                                c b    d e  a   f

Figure 1: A computer network

about relationships between the status of a site (working or not), connections between sites, and reachability of one site from another (which can be established by a path following direct connections), together with information about connections:

W = \{ \begin{matrix}∀x. works(x) ⊃ path(x, x), \\ ∀x, y. ¬works(x) ⊃ ¬reaches(y, x), \\ conn(a, b), conn(a, f), conn(b, c), \\ conn(b, d), conn(c, e), conn(d, e), conn(e, f) \\ ∀x. conn(x, x), ∀x, y. conn(x, y) ⊃ conn(y, x) \end{matrix} \}

The first two formulas in W state that if a site works, then there is a trivial path from this site to itself, and that if a site does not work, then it can not be reached from any node. The facts conn(s_{1}, s_{2}) state direct connections between sites. For convenience, reflexivity and symmetry of the connectivity relationship is taken care of by the respective axioms.^{1} A graphical representation of these connections is depicted in Figure 1.

The default rules are as follows.

D = \{ \frac{: works(x)}{works(x)}, \frac{path(x, y) :}{reaches(x, y)}, \frac{: ¬path(x, y)}{¬reaches(x, y)}, ; \frac{path(x, y) ∧ conn(y, z) ∧ works(z) :}{path(x, z)} \}

The first rule states that a site works by default; the next two rules relate paths to reachability, by adopting that x reaches y if a path from x to y provably exists, and does not reach it otherwise. The last rules states that a path can be extended by following a direct connection, if the site at the other end is working; here, it is assumed for simplicity that the connections are reliable, i.e., no communication failures occur.

In this representation, we implicitly adopt the common domain closure axiom ∀x. x = c_{1} ∨⋯∨ x = c_{n}, where c_{1}, …, c_{n} are all the objects (resp. individuals) of the underlying domain, which are those mentioned in T (in our case, all sites), and the axiom of the unique names assumption ⋀_{i<j} c_{i} ≠ c_{j}, which expresses that all objects mentioned in T are different.

1Negated facts ¬conn(s_{1}, s_{2}), stating that there is no direct connection between sites s_{1} and s_{2}, are omitted.

If desired, they can be derived using the closed world assumption, by introducing defaults \frac{:¬conn(x,y)}{¬conn(x,y)} in D.

In this setting, the default theory T has a single extension E, in which all sites work and each site reaches any other site; notice that reaches(x, y) is derivable iff there is a path x = s_{0}, s_{1}, …, s_{n} = y in the network such that works(s_{i}) is true for all i = 0, …, n and conn(s_{j−1}, s_{j}) is true for all j = 1, …, n.

We remark that the knowledge represented in T cannot be easily represented in classical logic. Indeed, reachability between sites refers to the transitive closure of a graph; it is well-known that transitive closure can not be expressed in classical first-order logic (cf. [1]). Explicit storage in terms of e.g. ground atoms conn^{+}(s_{1}, s_{2}) has the obvious disadvantages of inflexibility and maintenance cost, if the network is extended or its topology changes. However, default logic allows for an elegant representation of transitive closure and reachability.

Suppose now we observe that site a works but site e is not reachable from it, i.e., works(a) and ¬reaches(a, e) are true (which is not the case in the extension of T). If we look for an explanation of these manifestations in terms of sites that are down (while we disallow for assertion of facts path(x, y)), we find that –as expected– ¬works(e) is an explanation; indeed, from the formula ∀.x, y ¬works(x) ⊃ ¬reaches(y, x) it follows then immediately ¬reaches(a, e), and, by the first default rule in D, works(a) is true.

Other possible explanations exist besides ¬works(e). In fact, any subset S ⊆ {b, …, f} of sites whose failure causes a network partition so that a and e lie in different partitions gives rise to an explanation, by adopting ¬works(s) for every s ∈ S. Thus, e.g. ¬works(b), ¬works(f) and ¬works(c), ¬works(d), ¬works(f) are possible explanations as well; on the other hand, ¬works(c), ¬works(d) is not an explanation.

The examples suggest a formalization of abduction from default theories in a framework similar to the one for abduction from classical theories: Given a theory T, a set of observations (or manifestations) M is to be explained, by adopting a set of formulas (an explanation) E, which are from a set of hypotheses (or abducibles) H, so that T ∪ E derives M (where, of course, T ∪ E is consistent).

In Example 1, we had M = {¬skiing(Bill)} and H = { snowing }, and in Example 2 M = { works(a), ¬reaches(a, e) } and H = {¬works(a), ⋯, ¬works(f) }.

In the above examples, the default theories have a single default extension. However, in general, a default theory may have multiple (or even no) extensions; just assume in Example 2 the information is available that either site b or site d is down, which is naturally represented by adding the formula ¬works(b) ∨ ¬works(d) to W; Then, the resulting default theory has two extensions, one containing ¬works(b) and the other containing ¬works(d).

As a consequence of multiple extensions, (deductive) inference from default theories comes in different modes; usually, credulous inference, under which a formula ϕ is inferred from a default theory T (denoted T ⊢_{c} ϕ) iff ϕ belongs to at least one extension of T, and skeptical inference, under which ϕ follows from T (T ⊢_{s} ϕ) iff ϕ belongs to all extensions of T. Accordingly, the variants of credulous abduction, where inference of the observations is based on ⊢_{c}, and skeptical abduction, which is based on ⊢_{s}, from default theories arise.

In practice, the user will choose credulous or skeptical abduction on the basis of the particular application domain. Both modes of abduction appear to be useful and relevant. To emphasize this, we argue that credulous abduction is well-suited for diagnosis, while skeptical abduction is adequate for planning (see Section 3). Notice that the applicability and use of abduction in these domains is well-known, starting from Poole’s work on abductive logic-based diagnosis [44, 45, 46] and the work of Eshghi and others on abductive planning and plan recognition, cf. [24, 42].

On the computational side, we have to ask for the complexity of abduction from default logic, in order to find suitable algorithms for abduction. Towards this, we analyze the complexity of the main abductive reasoning tasks, formulated in the context of default abduction. Informally, these tasks amount to deciding whether an explanation exists (called Consistency), whether a particular hypothesis belongs to some explanation (Relevance) and whether a particular hypothesis belongs to every explanation (Necessity).

Consistency is self-explanatory; Relevance is important to separate hypotheses that contribute to an explanation from those which do not, and thus supports focusing the reasoning process. Necessity is important for computing the core of an explanation, which consists of the intersection of all explanations.

For classical theories, the complexity of logic-based abduction has been widely studied in the propositional context [57, 6, 22]. Furthermore, the complexity of reasoning from propositional default theories has been thoroughly analyzed in [58, 35, 27, 59]. The results showed that both abduction and default reasoning are harder than classical logic, and render problems that are complete for classes of the second level of the polynomial hierarchy (in particular, for Σ_{2}^{P} and Π_{2}^{P}), while classical logic is complete for classes of the first level (in particular, NP and co-NP).

Clearly, abduction from default theories is intractable as well, since default reasoning occurs as a subtask. However, it is not immediately clear how the complexities of abduction and default reasoning combine. We answer this question by precisely determining the complexity of each default abduction task, and locate it in the appropriate slot of the polynomial hierarchy proving completeness for the suitable class. The main complexity results can be summarized as follows:

• Default abduction is at least a hard as (deductive) default reasoning. The “easiest” setting is credulous default abduction, which is complete for Σ_{2}^{P} and Π_{2}^{P}, respectively; on the other hand, the “hardest” task –Relevance in skeptical default abduction based on minimal explanations (i.e., explanations that do not contain any other explanation properly)– is complete for Σ_{4}^{P}, which is loosely speaking the “square” of Σ_{2}^{P}. Other settings yield abduction problems that are complete for well-known classes in between Σ_{2}^{P} resp. Π_{2}^{P} and Σ_{4}^{P};

• Skeptical default abduction is precisely one level harder than credulous default abduction in the polynomial hierarchy. This contrasts with usual results for nonmonotonic formalisms, where skeptical reasoning has complexity complementary to credulous reasoning (typically, Π_{2}^{P} and Σ_{2}^{P}), and is at the same level in the polynomial hierarchy;

• the Relevance problem has complexity complementary to the Necessity problem; and

• Minimality of explanations is a source of complexity for Relevance, and makes the problem harder. This contrasts with results for abduction from classical theories [22].

Since abduction from default theories is intractable, it is important to find problem restrictions under which polynomial time algorithms are possible. For default reasoning, the border between tractable and intractable fragments has been sharply marked by the excellent work of Kautz and Selman [35] and Stillman [58]. As default abduction builds on default reasoning, tractability of default abduction has to be based on a tractable fragment for default reasoning. Following this approach, we point out two classes of default theories from which abduction tasks are tractable. These are Literal-Horn default theories, where W consists of literals and D contains only so called Horn defaults, and Krom-pf-normal default theories, where W consists of Krom clauses (clauses of size ≤ 2) and D contains only prerequisite-free normal defaults that allow to conclude a conjunction of literals; see Section 5 for details.

We also discuss the complexity of abduction from first-order default theories. Of course, this is undecidable in general as first-order logic is undecidable. However, adopting the common domain closure axiom and the unique names assumption, we obtain that abduction from default theories is decidable. Here, the complexity parallels the complexity of the propositional case, increased by an exponential; this means that the abduction problems we consider are provably intractable.

The rest of this paper is organized as follows. The following Section 2 recalls the necessary concepts of default logic and complexity theory, and introduces some basic notation. Section 3 presents the framework for abduction from default theories and formally states the main abductive reasoning tasks in it. In the course of that, the use of credulous vs skeptical abduction is discussed. Section 4 describes and discusses the results of our analysis of the complexity of default abduction in the propositional context; the subsequent Section 5 addresses the issue of tackling default abduction in practice, and focuses on tractable cases. The complexity of abduction from first-order default theories is addressed in Section 6. Finally, Section 7 concludes the paper and outlines issues for further research.

In order to improve readability, the proofs of the results, except a few short, transparent proofs, have been moved to the appendix.

2 Preliminaries and notation

We assume that the reader knows about the basic concepts of default logic [52] (cf. also [38] for an extensive study of the subject).

Let L be a first-order predicate language. A default theory is a pair T = ⟨W, D⟩ of a set W of formulas from L without free variables and a set D of default rules d of form

\frac{α(x) : β_{1}(x), …, β_{m}(x)}{γ(x)}, m ≥ 1

where α(x) (the prerequisite), β_{1}(x), …, β_{m}(x) (the justifications), and γ(x) (the conclusion) are from L, and the free variables of all these formulas are among the variables in x = x_{1}, …, x_{n}. We omit α and any β_{i} if it is a tautology. If no free variables occur, the default is closed. A default theory ⟨W, D⟩ is closed if every default in D is closed.

The semantics of a closed default theory T = ⟨W, D⟩ is defined in terms of extensions. A set E ⊆ L is an extension of T iff E = ⋃_{i=0}^{∞} E_{i}, where

E_{0} = W, and for i ≥ 0

E_{i+1} = T h(E_{i}) ∪ \{γ | \frac{α:β_{1},...,β_{m}}{γ} ∈ D, E_{i} ⊢ α, ¬β_{1} ∉ E, … ¬β_{m} ∉ E\},^{2}

where ⊢ is classical inference and T h(·) denotes classical deductive closure. The extensions of a general default theory T = ⟨W, D⟩ are by definition the extensions of the closure of T, cl(T), which is the default theory cl(T) = ⟨W, { dσ | d(x) ∈ D, σ is a ground substitution for x}⟩.

A default theory may have several (or even no) extensions in general. It is well-known that different extensions E1 and E2 are incomparable, i.e., E1 ⊆ E2 implies E1 = E2, and that L is an extension of T iff W is not consistent.

Each extension of a closed default theory T = ⟨W, D⟩ can be characterized in terms of its generating defaults. Let for any set S of closed formulas denote by GD(S, T) the set of all defaults \frac{α:β_{1},...,β_{m}}{γ} ∈ D such that S ⊢ α and ¬β_{i} ∉ S, for all i = 1 …, m, and denote by concl(D′) the set of all conclusions of defaults in the set D′. Then,

Proposition 2.1 [52] Let E be an extension of the closed default theory T = ⟨W, D⟩. Then, E = T h(W ∪ concl(GD(E, T))).

On the other hand, if a deductively closed formula set S satisfies S = T h(W ∪ concl(GD(S, T))), then S is not necessarily an extension; however, it is true if T is prerequisite-free, i.e., the prerequisite of each default in D is a tautology.

A default rule is called normal if it is of form \frac{α:β}{β}. The class of normal default theories, where each default in D is normal, is considered to be one of the most important fragments of default logic. Normal default theories always have extensions; moreover, they enjoy the property of semi-monotonicity: If E is an extension of a normal default theory ⟨W, D⟩ and D′ ⊇ D contains only normal defaults, then ⟨W, D′⟩ has an extension E′ ⊇ E [52].

The standard variants of inference from a default theory T are credulous inference (denoted ⊢_{c}), under which ϕ is inferred iff ϕ belongs to at least one extension of T, and skeptical inference (⊢_{s}), under which ϕ follows iff ϕ belongs to all extensions of T.

For NP-completeness and complexity theory, cf. [31]. The classes Σ_{k}^{P} and Π_{k}^{P} of the polynomial hierarchy are defined as follows:

Σ_{0}^{P} = Π_{0}^{P} = P and for all k > 1, Σ_{k}^{P} = NP^{Σ_{k−1}^{P}}, Π_{k}^{P} = co-Σ_{k}^{P} .

In particular, NP = Σ_{1}^{P}, co-NP = Π_{1}^{P}, and Σ_{2}^{P} = NP^{NP}. Intuitively, NP^{Σ_{k−1}^{P}} models computability by a nondeterministic polynomial-time algorithm which may use an oracle (loosely speaking, a subprogram without cost) for solving a problem in Σ_{k−1}^{P}. In the context of nonmonotonic reasoning, an oracle for NP (which allows to decide classical propositional satisfiability and hence also inference ⊢) is common.

The class D_{k}^{P} is defined as the class of problems that consist of the conjunction of two (independent) problems from Σ_{k}^{P} and Π_{k}^{P}. Notice that for all k ≥ 1, clearly Σ_{k}^{P} ⊆ D_{k}^{P} ⊆ Σ_{k+1}^{P}; both inclusions are widely conjectured to be strict, since equality of the left or the right one would imply the collapse of the polynomial hierarchy. Recall that a problem A is complete for a class C iff A belongs to C and every problem in C is reducible to it by a polynomial-time transformation; intuitively, a problem complete for C is the hardest problem in C.

2We use here “E_{i} ⊢ α instead of “α ∈ E_{i}” as usual, which gives rise to the same concept.

It appeared that many computational problems in nonmonotonic reasoning are complete for classes at the lower end of the polynomial hierarchy [9, 41]. In particular, it is well-known that deciding whether a propositional default theory has an extension is Σ_{2}^{P} -complete, and that credulous reasoning and skeptical reasoning from default theories are complete for Σ_{2}^{P} and Π_{2}^{P}, respectively [27, 58]. The complexity remains unchanged if inconsistent extensions are excluded and, for the latter problems, if default theories are in addition normal [27, 59]. Cases of lower complexity and tractable fragments were identified in [35, 58]. The complexity of logic-based abduction from classical theories has been analyzed in [57, 6, 22] (cf. [7] for a comprehensive analysis of the set covering approach). Basically, abduction has the same complexity as default reasoning, and bears Σ_{2}^{P} -complete and Π_{2}^{P} -complete reasoning problems.

3 Formalizing default abduction

In this section, we describe a basic formal model for abduction from propositional default theories and state the main decisional reasoning tasks for abductive reasoning.

Our formalization of an abduction scenario is as follows.

Definition 3.1 A default abduction problem (DAP) is a quadruple ⟨H, M, W, D⟩ where H is a set of ground (i.e., variable-free) literals (called hypotheses, or abducibles), M is a set of ground literals (called observations, or manifestations), and ⟨W, D⟩ is a default theory. We say a DAP P = ⟨H, M, W, D⟩ is normal iff ⟨W, D⟩ is normal.

This definition reflects the intention that abduction explains particular observations, stated by possibly negated facts, in terms of a collection of elementary hypotheses, which are possibly negated facts. Such a setting is common in logic-based abduction, cf. [57]. In fact, it is not a shortcoming over allowing arbitrary closed formulas as hypotheses or manifestations, since for each non-literal hypothesis (resp. manifestation) ϕ a new propositional atom a_{ϕ} might be introduced, and after adding the formula a_{ϕ} ↔ ϕ to W, ϕ can equivalently be replaced by a_{ϕ}.

If all positive (resp. negative) ground literals p(t) from a predicate p are hypotheses, it is convenient to say that p (resp. ¬p) is abducible and include p (resp. ¬p) in H rather than all literals p(t) (resp. ¬p(t)). Accordingly, in Example 2 ¬works is abducible, and the set H is simply H = {¬works} instead of H = { ¬works(a), …, ¬works(f) }.

We next formally define explanations, based on credulous resp. skeptical default inference.

Definition 3.2 Let P = ⟨H, M, W, D⟩ be a DAP, and let E ⊆ H. Then, E is a credulous explanation for P iff

(i) ⟨W ∪ E, D⟩ ⊢_{c} M, and

(ii) ⟨W ∪ E, D⟩ has a consistent extension.

Similarly, E is a skeptical explanation for P iff

(i) ⟨W ∪ E, D⟩ ⊢_{s} M, and

(ii) ⟨W ∪ E, D⟩ has a consistent extension.

The existence of a consistent extension for ⟨W ∪E, D⟩ (in this case, all extensions are consistent) assures that the explanation E is consistent with the knowledge represented in ⟨W, D⟩. This requirement is analogous to the usual consistency criterion in abduction from classical theories.

It is common in abductive reasoning to prune the set of all explanations and to focus, guided by some principle of explanation preference, on a set of preferred explanations. The most important such principle is, following Occam’s principle of parsimony, to prefer nonredundant explanations, i.e., explanations which do not contain any other explanation properly (cf. [43, 57, 37]). We refer to such explanations as minimal explanations. (See [43, 7, 22] for other preferences on explanations).

Example 1 (ctd.) Suppose the certain knowledge W is extended by ∀x. broken leg(x) ⊃ ¬skiing(x) to W 1. Then, for M = { ¬skiing(Bill) } H = { snowing, broken leg }, the explanations for ⟨H, M, W 1, D⟩, under credulous as well as skeptical inference, are: E1 = {snowing}, E2 = {broken leg(Bill)}, and E3 = {snowing, broken leg(Bill) }. The minimal explanations are E1 and E2; they are clearly preferred to E3.

Example 2 (ctd.) Reconsider to explain M = { works(a), ¬reaches(a, e) } from H = { ¬works }. The explanations for ⟨H, M, W, D⟩ correspond 1-1 to the subsets of sites S ⊆ {b, …, f} whose simultaneous failure causes a and e to be in two different partitions of the network. The minimal explanations thus correspond to the minimal such sets S, which are: {e}, {b, f}, and {c, d, f}. Intuitively, they amount to the explanations a rational agent is willing to accept, namely that e is down, that b and f are down, or that c, d and f are down.

In the sequel, we will write Exp(P) for the set of explanations for the DAP P, abstracting from the chosen type of explanations (credulous, skeptical, minimal credulous, or minimal skeptical).

3.1 Credulous vs skeptical abduction

As already mentioned in Section 1, both modes of abduction –credulous and skeptical abduction– appear to be useful in practice. For example, credulous abduction is suitable for diagnosis, while skeptical planning is appropriate for planning, which we discuss next.

3.1.1 Credulous abduction: diagnosis

Consider a system represented by a default theory T = ⟨W, D⟩. If the system receives some input, reflected by adding a set A of facts to W, then each extension of T′ = ⟨W ∪ A, D⟩ is a possible evolution of the system, i.e., each extension represents a possible reaction of the system to A.

Abductive diagnosis consists, loosely speaking, in deriving from an observed system state (given by M), a suitable input A which caused this evolution (cf. [46]). Now, since each extension of ⟨W ∪ A, D⟩ is a possible evolution of the system with input A, we can assert that A is a possible input that caused F if ⟨W ∪ A, D⟩ ⊢_{c} F. Thus, diagnostic problems can be naturally represented by abductive problems with credulous inference.

In the network example above, finding an explanation for the observations works(a) and ¬reaches(a, e) is a diagnostic problem; minimal explanations correspond to the intuitive diagnoses, i.e., alternative collections of possibly broken machines. However, each of the explanations E_{i} is acceptable under both credulous and skeptical inference, since the default theory ⟨W ∪E_{i}, D⟩ has a single extension.

To show the use of credulous inference for diagnosis, we consider the scenario where the additional information is available that either b or d is down, i.e., W contains also the formula ¬works(b) ∨ ¬works(d). Then, the default theory ⟨W, D⟩ has two extensions, one in which b is down (while d is up) and another one in which d is down (while b is up). Suppose now we want to find a diagnosis for the observations (works(a), ¬reaches(a, e)) in which the actual status of b and d is open; that is, we focus on a partial, consistency-based diagnosis in terms of hypotheses from { ¬works(c), ¬works(e), ¬works(f) }, which might be extendible to a complete diagnosis, in which the status of each site is pinned down. Intuitively, the fact ¬works(f) is then an acceptable diagnosis; in fact, it allows for a complete diagnosis (in which ¬works(b) is true and thus all paths from a to e are broken). As easily checked, E = {¬works(f)} is a credulous explanation for the DAP P = ⟨H, M, W, D1⟩ where M = { works(a), ¬reaches(a, e) } and H = { ¬works(c), ¬works(e), ¬works(f) }. Note, however, that E is not a skeptical explanation, since ⟨W ∪ E, D⟩ has an extension in which reaches(a, e) is true.

Other diagnostic tasks in which credulous default abduction is appropriate arise in a slightly modified scenario; for example, if the knowledge about connections between sites is not complete. Assume it is known that f is connected to either e or b, but not to which of them, and a closed world assumption default \frac{:¬conn(x,y)}{¬conn(x,y)} is present in the default theory. Then, if we concentrate on (partial) diagnoses in terms of site failures, ¬works(b) would be acceptable for the above manifestations M. In fact, {¬works(b)} is a credulous explanation P = ⟨H, M, W, D⟩ where H = {¬works}.

3.1.2 Skeptical abduction: planning

Suppose now that we want that the system evolves into a certain state (described by a set F of facts), and we have to determine the “right” input (i.e., actions) that enforces this state of the system (planning). In this case it is not sufficient to choose an input A such that F is true in some possible evolution of the system; rather, we look for an A such that F is true in all possible evolutions, as we want be sure that the system reacts in that particular way. In other words, we look for A such that ⟨W ∪ A, D⟩ ⊢_{s} F. Hence, planning activities can be represented by abductive problems with skeptical inference.

Let us consider a simple planning problem in the network example. Suppose that a packet should be sent from site a to e. In particular, a route for sending the packet from a to b should be generated, taking into account possible knowledge that some sites might not work.

To model this, we augment the default theory as follows. First, a formula is added to W that states a packet can be sent to a single node only, yielding

W_{1} = W ∪ { ∀x, y, z. send(x, y) ∧ send(x, z) ⊃ y = z};

we augment D to

D_{1} = D ∪ \{ \begin{matrix}\frac{: ¬send(x, y)}{¬send(x, y)}, \frac{send(x, y) : ¬conn(x, y) ∨ ¬reaches(x, y)}{⊥} \\ \frac{send(x, y) : t(x, y)}{t(x, y)}, \frac{t(x, y) ∧ send(y, z) : t(x, z)}{t(x, z)} \end{matrix} \};

here, ⊥ is a symbol for contradiction and t(x, y) states that the packet is transported from x to y. The augmented default theory is T_{1} = ⟨W_{1}, D_{1}⟩.

The planning problem can be solved by finding a (skeptical) explanation for M = { t(a, e) } using H = { send } as hypotheses, i.e., ground facts send(s_{1}, s_{2}). For the original W (which describes the network in Figure 1, and no site failures are known), we then obtain three minimal explanations for ⟨H, M, W, D_{1}⟩, namely E_{1} = {send(a, b), send(b, c), send(c, e)}, E_{2} = {send(a, b), send(b, d), send(d, e)}, and E_{3} = {send(a, f), send(f, e)}; all three are in fact credulous as well as skeptical explanations. Minimality of explanations means each routing is minimal, i.e., contains no superfluous send actions; in particular, it avoids looping (e.g. E_{4} = {send(a, b), send(b, e), send(c, e), send(e, d), send(b, d)} is a nonminimal explanation that amounts to a routing in a loop). Clearly, looping could also be explicitly excluded by an axiom in W_{1} stating that each node can receive a packet from only one node.

Notice that adding the information ¬works(b) ∨ ¬works(d) to W_{1} eliminates two out of the three minimal explanations, namely E_{1} and E_{2}; only E_{3} remains as a skeptical explanation. This matches perfectly our intuitive expectations: There is an extension in which b is down, and therefore all routes for sending the packet that pass through b are not fully reliable. In particular, the routes corresponding to E_{1} and E_{2} are not fully reliable and have to be dropped.

Finally, if it known that besides ¬works(b) ∨ ¬works(d) also ¬works(f) is true, then longer a skeptical explanation exists. This perfectly matches our intuitive expectation: there is an extension in which b and f are down simultaneously, and since all paths from a to e go through either b or f, it is impossible to send in this extension the packet from a to e.

3.2 Abductive reasoning tasks

The following properties of a hypothesis in a DAP P are important with respect to computing explanations.

Definition 3.3 Let P = ⟨H, M, W, D⟩ be a DAP and h ∈ H. Then, h is relevant for P iff h ∈ E for some E ∈ Exp(P), and h is necessary for P iff h ∈ E for every E ∈ Exp(P).

The opposite of necessity is also termed dispensability (cf. [32]). In Example 1, snowing is both relevant and necessary, as E = {snowing} is the only explanation.

The main decisional problems in abductive reasoning amount to the following. Given a DAP P = ⟨H, M, W, D⟩, (Consistency): does there exist a explanation for P ?

(Relevance): is a given ground hypothesis h ∈ H relevant for P, i.e., does h contribute to some explanation of P?

(Necessity): is a given ground hypothesis h ∈ H necessary for P, i.e., is h contained in all explanations of P?

In the following section, we address the complexity of these problems in the propositional context.

4 Complexity results: propositional case

In this section, we analyze the complexity of the main abductive reasoning tasks in the propositional context.

A propositional default abduction problem (PDAP) is thus a DAP P = ⟨H, M, W, D⟩ such that H and M are sets of propositional formulas, and ⟨W, D⟩ is a propositional default theory. For solving the abductive reasoning tasks, we suppose that the input PDAP P is finite, i.e., H, M, W, and D are finite.

The main results on the complexity of abduction from general propositional default theories are summarized in Table 1. Each entry C represents completeness for the class C. In our analysis, we pay particular attention to normal PDAPs, since this class corresponds to the most important fragment of default logic. The results in Table 1, with the exception of recognizing a minimal credulous explanation, hold even if the underlying default theory ⟨W, D⟩ is normal. Thus like deduction, abduction from normal default theories is as hard as abduction from arbitrary default theories.

PDAP P = ⟨H, M, W, D⟩ arbitrary explanations minimal explanations
Problem:  credulous skeptical credulous skeptical
Consistency  Σ_{2}^{P}  Σ_{3}^{P}  Σ_{2}^{P}  Σ_{3}^{P}
Recognition: E ∈ Exp(P) ?  Σ_{2}^{P}  D_{2}^{P}  D_{2}^{P}  Π_{3}^{P}
E ∈ Exp(P) is minimal ?  Π_{2}^{P}  Π_{3}^{P}  —  —
Relevance  Σ_{2}^{P}  Σ_{3}^{P}  Σ_{3}^{P}  Σ_{4}^{P}
Necessity  Π_{2}^{P}  Π_{3}^{P}  Π_{2}^{P}  Π_{3}^{P}

Table 1: Complexity of abduction from propositional default theories (completeness results)

The results can be commented and explained as follows. The “easiest” abductive reasoning tasks have the same complexity as (deductive) inference from default theories, namely Σ_{2}^{P} and Π_{2}^{P}.

# explanations minimality  classical inference ⊢ # extensions

Figure 2: Orthogonal sources of complexity for Relevance, in skeptical abduction using minimal explanations

respectively, while the “hardest” task has complexity Σ_{4}^{P} (Relevance under minimal credulous explanations), which is, loosely speaking the “square” of Σ_{2}^{P}. The other tasks have intermediate complexity.

As argued in [9, 20], the level of the polynomial hierarchy at which a problem resides shows that the problem suffers from (at least) that many sources of inherent complexity, and they are intermingled so that, in a sense, they act “orthogonally.” For the hardest problem in Table 1 (Σ_{4}^{P} -completeness), we thus must have four such orthogonal sources of complexity. In fact, they can be identified as follows (cf. Figure 2): (1.) classical deductive inference (⊢), (2.) the number of extensions of ⟨W ∪ E, D⟩, (3.) the number of candidates E for a skeptical explanation, and (4.) the number of possible smaller explanations (i.e., minimality); here these numbers can be exponential in the problem size.

If we compare credulous abduction to skeptical abduction, we find that for the main reasoning tasks, skeptical abduction is always precisely one level harder than credulous abduction. This contrasts with the results for many nonmonotonic reasoning formalisms (default logic, autoepistemic logic, circumscription, …) obtained so far (see [9, 41]), where skeptical reasoning has complexity complementary to credulous reasoning (typically, complete for Π_{2}^{P} while credulous reasoning is complete for Σ_{2}^{P}). The reason for this interesting phenomenon is that a credulous explanation and an extension proving the explanation property can be nondeterministically generated simultaneously, which saves one level in the hierarchy over skeptical explanations (see below for a more formal account).

Minimality of extensions is a source of complexity for Relevance and causes an increase in complexity by one level in the polynomial hierarchy. However, it does not add to the complexity of Necessity due to the following simple fact.

Proposition 4.1 Let P = ⟨H, M, W, D⟩ be a finite PDAP and let h ∈ H. Then, h is necessary for P under minimal credulous (resp. skeptical) explanations iff h is necessary for P under credulous (resp. skeptical) explanations.

Therefore, we shall not deal in our analysis explicitly with Necessity in the case of minimal explanations.

The results for Relevance contrast with corresponding results for abduction from classical theories: there, minimality of explanation is not a source of complexity [22]. This discrepancy can be explained by the fact that the inference relation ⊢ underlying classical abduction is monotonic, while ⊢_{c} and ⊢_{s} are nonmonotonic; monotonicity effects that the explanation space is well-structured, so that minimality of an explanation can be decided by looking at few candidates for smaller explanations. This benign property does not apply to ⊢_{c} and ⊢_{s} inference, where still an exponential candidate space remains to be checked.

By the results in Table 1, we are able to draw some conclusions about the relationship of default abduction to other forms of nonmonotonic reasoning. First, by virtue of complexity theory, the reasoning tasks that are complete for Σ_{2}^{P} or Π_{2}^{P} can be polynomially transformed into an equivalent reasoning task in any of the classical nonmonotonic formalisms such as default logic, autoepistemic logic, circumscription, etc. Thus, theorem provers for such formalisms, e.g., the DeReS system for default logic (cf. [13]), can be fruitfully used for performing default abduction as well. Such polynomial transformations can be extracted from the proofs of the complexity results, by simply composing transformations. In many cases, however, a direct and much simpler transformation can be found. In fact, we show below how default abduction can be transformed to classical default reasoning by means of a plain transformation.

For the classes Σ_{3}^{P} and Π_{3}^{P}, not many nonmonotonic logics of this complexity have been known until recently. It was known that moderately grounded AEL has this complexity [21]; it appeared that a family of similar so called ground logics has the same complexity [19]. Moreover, the recent extension of default logic by trans-epistemic defaults [50] is complete for Σ_{3}^{P} resp. Π_{3}^{P} [51]. Thus, the default abduction tasks in Table 1 that have this complexity can be efficiently translated into this logics and vices versa; implementations lack today, however.

Finally, for the hardest reasoning task (Σ_{4}^{P} -complete), there is no well-known nonmonotonic logic of similar complexity; it landmarks a region of very hard nonmonotonic reasoning problems, and shows that intuitive reasoning tasks can grow quite complex.

Besides the quantitative account, the above completeness results have also a qualitative aspect. They tell that a simply ad hoc algorithm for solving the reasoning tasks, which exhaustively searchs an exponential candidate space for each source of complexity, can not be substantially improved with concern of solving the problem on all instances. For example, consider the straightforward algorithm in Table 2. There, it is assumed that a procedure skept-inf(W, D, ϕ) for skeptical inference of ϕ from ⟨W, D⟩ is available (cf. the DeReS system [13]), and ⊥ is any contradiction. This algorithm is exponential, even if skept-inf is seen as an zero-cost oracle; the complexity result for this problem (Σ_{4}^{P} -completeness, which loosely speaking means Σ_{2}^{P} -completeness modulo skeptical inference), however, indicates that there is basically no substantially better algorithm that avoids the costly for-loops. (Of course, the loops can be optimized, but overall still an exponential effort is needed. An algorithm that uses exponential space might be able to get away with a single for-loop, e.g. by systematic and exhaustive state-space search for extensions.)

Since all the results in Table 1 are negative with respect to efficient computation, we have to ask how to deal with the reasoning problems in practice. This will be addressed in Section 5.

4.1 Arbitrary explanations

A useful observation is that in general, the problems Relevance and Necessity can be easily reduced to Consistency and its complement, respectively, for both credulous and skeptical

Algorithm Min-Skeptical-Relevance(H, M, W, D, h)

input: A propositional DAP P = ⟨H, M, W, D⟩, h ∈ H.
output: “Yes” if h is relevant for P under minimal

skeptical explanations, “No” otherwise. (* check if E is skeptical explanation *) procedure explanation(E): boolean

begin ϕ := conjunction of all literals in M;

return skept-inf(W ∪ E, D, ϕ) and not skept-inf(W ∪ E, D, ⊥); end explanation;

begin

for each E ⊆ H s.t. h ∈ E do begin if explanation(E) then (*E is candidate for a minimal explanation *) begin minexp := true;

for each E′ ⊂ E do if explanation(E′) then minexp := false; end; if minexp = true then begin output(“Yes”); halt end;

end;

output(“No”); end Min-Skeptical-Relevance.

Table 2: Algorithm for Relevance

explanations. Indeed, the following is easily verified.

Proposition 4.2 Let P = ⟨H, M, W, D⟩ be a PDAP based on credulous or skeptical explanations, and let h ∈ H. Then, E is an explanation for the PDAP ⟨H\ {h} M, W ∪ {h} , D⟩ iff E ∪ {h} is an explanation for P.

Proof. “⇒”: all extensions of ⟨W ∪ {h} ∪ E, D⟩ are consistent and contain M, and extensions exist. Hence, E ∪ {h} is an explanation for P. “⇐”: E ∪ {h} is an explanation for P means that some consistent extension of ⟨W ∪ E ∪ {h} , D⟩ exists and that all (some) extensions contain M. Hence, E is an explanation for ⟨H\ {h} , M, W ∪ {h} , D⟩.

Corollary 4.3 Let P = ⟨H, M, W, D⟩ be a PDAP and h ∈ H. Then, (i) h is relevant for P iff ⟨H\ {h} , M, W ∪{h} , D⟩ has an explanation and (ii) h is necessary for P iff ⟨H\ {h} , M, W, D⟩ has no explanation.

Thus, if Consistency lies in complexity class C, then Relevance is also in C and Necessity is in co-C.

Our first result shows that abduction from default theories based on credulous explanations can be efficiently reduced to deductive reasoning from propositional default theories. This is somewhat unexpected and surprising, since in case of classical theories, abduction can not be efficiently reduced to deduction.

Given a PDAP P = ⟨H, M, W, D⟩, we construct a default theory T_{P} = ⟨W_{P}, D_{P}⟩ such that the credulous explanations of P correspond to the (consistent) extensions of T_{P}. Indeed, define

W_{P} = W ∪ {a_{h} ⊃ h | h ∈ H} ,
D_{P} = D ∪ \{ \frac{:¬m}{⊥} | m ∈ M\} ∪ \{ \frac{:a_{h}}{a_{h}} , \frac{:¬a_{h}}{¬a_{h}} | h ∈ H\}

where for each h ∈ H, a_{h} is a new propositional atom. Informally, the atom a_{h} means that hypothesis h is adopted. Each credulous explanation E of P is verified by a consistent extension A of ⟨W ∪ E, D⟩ that contains M. This extension A gives rise to a consistent default extension A′ of T_{P} which augments A be new formulas. The default \frac{:¬m}{⊥} prevents an augmentation of an extension A which does not contain M, while the defaults \frac{:a_{h}}{a_{h}}, \frac{:¬a_{h}}{¬a_{h}} serve to choose the explanation E, where \frac{:a_{h}}{a_{h}} (resp. \frac{:¬a_{h}}{¬a_{h}} ) is applied to include h in E (resp. exclude h from E). Note that using the defaults \frac{:h}{h}, \frac{:¬h}{¬h} instead of \frac{:a_{h}}{a_{h}}, \frac{:¬a_{h}}{¬a_{h}} does not work; in particular, applying \frac{:¬h}{¬h} would mean to include the negation of h in E, which is different from excluding h from E. More formally, the construction has the following property:

Theorem 4.4 Let P = ⟨H, M, W, D⟩ be a PDAP. Then, (i) if E is a credulous explanation for P, then there exists a consistent extension A′ of T_{P} such that E = {h ∈ H | a_{h} ∈ A′}; (ii) if A′ is a consistent extension of T_{P}, then E = {h ∈ H | a_{h} ∈ A′} is a credulous explanation for P.

Proof. (i) Let E be a credulous explanation for P. Hence, ⟨W ∪ E, D⟩ has a consistent extension A which contains M. Define A′ = T h(A ∪ {a_{h} | h ∈ E} ∪ {¬a_{h} | h ∈ H\E}). Clearly, A′ is consistent. Moreover, A′ is an extension of ⟨W_{P}, D_{P}⟩. Indeed, each default d ∈ D that can be applied in A_{i} from the sequence A_{0}, A_{1}, … for A can also be applied in A′_{i} from A′_{0}, A′_{1}, … On the other hand, if d ∈ D is applied in some A′_{i}, then it is also applied in some A_{j}. Since M ⊆ A′, no default \frac{:¬m}{⊥} can be applied. Thus, A′ = ⋃_{i=0}^{∞} A′_{i}, and hence A′ is an extension of ⟨W_{P}, D_{P}⟩. Obviously, E = {h | a_{h} ∈ A′}. This proves (i). (ii) Let A′ be a consistent extension of ⟨W_{P}, D_{P}⟩, and let E = {h | a_{h} ∈ A′}. Let A be the restriction of A′ to the language of P. Then, A is an extension of ⟨W ∪E, D⟩. Indeed, first notice that E ⊆ A. Each default d ∈ D which is applicable in A′_{i} from A′_{0}, A′_{1}, … is also applicable in A_{i} from A_{0}, A_{1}, … On the other hand, each d ∈ D which is applicable in A_{i} can be clearly applied in A′_{i+1} as well. We conclude that A = ⋃_{i=0}^{∞} A_{i}, and hence A is an extension of ⟨W ∪ E, D⟩. We show that M ⊆ A, by which (ii) is proven. But this is easy: M ⊆ A′, for otherwise a default \frac{:¬m}{⊥} would be applicable; hence, by definition of A, M ⊆ A.

Using (i) and (ii), the main decisional abductive reasoning tasks can be efficiently transformed to similar deductive reasoning tasks in default logic.

Corollary 4.5 Let P be a PDAP based on credulous explanations. Then, (i) Consistency, (ii) Relevance, and (iii) Necessity are equivalent to (i^{∗}) existence of a consistent extension of T_{P}, (ii^{∗}) membership of a_{h} in some consistent extension of T_{P}, and (iii^{∗}) membership of a_{h} in all extensions of T_{P}, respectively.

By the results on the complexity of propositional default logic [27, 59], it follows that (i) and (ii) are in Σ_{2}^{P} and that (iii) is in Π_{2}^{P}. We also obtain matching hardness by reductions from deductive default reasoning. Let T = ⟨W, D⟩ be a normal default theory such that W is a consistent set of literals (in fact, W can be even empty), and ϕ a formula. Let h, q be new propositional atoms. Then, the following facts are clear: the PDAP

⟨∅, {q} , W ∪ {ϕ ⊃ q} , D⟩ (1)

has a credulous explanation iff T ⊢_{c} ϕ; h is relevant for the PDAP

⟨{h} , {q} , W ∪ {ϕ ⊃ q} , D⟩ (2)

iff T ⊢_{c} ϕ; and h is necessary for the PDAP

⟨{h} , {q} , W ∪ {ϕ ∨ h ⊃ q} , D⟩ (3)

iff T ⊬_{c} ϕ. Since the reasoning problems for T in (1), (2) are Σ_{2}^{P} -hard and the one in (3) is Π_{2}^{P} -hard [27], we obtain the following results.

Theorem 4.6 Let P be a PDAP based on credulous explanations. The problem (i) Consistency is Σ_{2}^{P} -complete, (ii) Relevance is Σ_{2}^{P} -complete and (iii) Necessity is Π_{2}^{P} -complete, with hardness even for normal P.

Remark. The complexity result for Consistency shows that a polynomial-time reduction of credulous explanations to classical extensions of a default theory T_{P} as above, but where the default theory is normal, is not possible in general. Indeed, if W_{P} is consistent, then T_{P} has a consistent extension, and thus the PDAP would also have an explanation. This would imply an NP algorithm deciding existence of a credulous explanation, and NP = Σ_{2}^{P} would follow, which is generally believed to be false.

It is interesting to note that verifying a credulous explanation is as hard as finding one. The former problem can be easily reduced to the latter; moreover, ∅ is the only possible credulous explanation for the PDAP (1). Thus,

Theorem 4.7 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if E ⊆ H is a credulous explanation for P is Σ_{2}^{P} -complete, with hardness holding even for normal P.

Now consider abduction based on skeptical reasoning. It would be useful to have a reduction of abductive reasoning to deductive reasoning which can be computed efficiently. However, by using skeptical reasoning the abductive reasoning tasks grow more complex, by one level of the polynomial hierarchy. This strongly suggests that such an efficient reduction is not possible.

We first consider the problem of recognizing skeptical explanations. Clearly, this reduces to deciding if a certain default theory has a consistent extension (which is in Σ_{2}^{P}) and if each extension includes all manifestations (Π_{2}^{P}). Thus, the problem is a logical conjunction of a problem in Σ_{2}^{P} and a problem in Π_{2}^{P}, and hence in the class D_{2}^{P}. Moreover, it is also hard for this class.

Theorem 4.8 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if E ⊆ H is a skeptical explanation for P is D_{2}^{P}-complete.^{3}

Thus, as in the case of credulous explanations, recognizing a skeptical explanation is at the second level of the polynomial hierarchy. However, since this problem involves both a Σ_{2}^{P} and a Π_{2}^{P} -hard subtask (as opposed to only a Σ_{2}^{P} -hard one), finding a skeptical explanation resides at the third level.

Theorem 4.9 Let P be a PDAP based on skeptical explanations. The problem (i) Consistency is Σ_{3}^{P} -complete, (ii) Relevance is Σ_{3}^{P} -complete and (iii) Necessity is Π_{3}^{P} -complete, with hardness even for normal P.

How does this result compare to other nonmonotonic logics, in particular, which nonmonotonic logic has similar complexity ? We know that Konolige’s moderately grounded autoepistemic logic [36] and several other ground nonmonotonic modal logics have the same complexity [21, 19]; thus, we can use a theorem prover for such logics to perform abductive reasoning from default theories based on skeptical explanations.

4.2 Minimal explanations

As mentioned above, one is usually interested in minimal explanations for observations. The results in [22] were that the complexity of abduction from classical theories does not increase if minimal explanations are used instead of arbitrary explanations. However, this is not true for abduction from default logic. Here, checking minimality of an explanation is a source of complexity, which causes an increase in complexity by one level of the polynomial hierarchy.

Consider first credulous explanations. Checking minimality of an explanation E has complementary complexity of checking the explanation property.

Theorem 4.10 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if a credulous explanation E for P is minimal is Π_{2}^{P} -complete, with hardness even for normal P.^{4}

To see this, notice that E is not minimal iff for some h ∈ E, the PDAP ⟨E\ {h} , M, W, D⟩ has a credulous explanation; hence, it follows that the problem is in Π_{2}^{P}. On the other hand, reconsider the PDAP (3). Clearly, {h} is a credulous explanation; moreover, it is minimal iff h is necessary for P. Thus, Π_{2}^{P} -hardness follows.

Note that recognizing minimal credulous explanations, which consists in checking the explanation property and testing minimality, is in D_{2}^{P}; it is also complete for this class (Theorem A.1). Thus, this problem can be transformed into recognition of skeptical explanations for a certain PDAP and vice versa.

3For normal PDAPs, the problem is “only” Π_{2}^{P} -complete, since then deciding whether ⟨W ∪E, D⟩ has a consistent extension is in NP.

4 Strictly speaking, it is “promised” that E is an explanation; in fact, since recognizing explanations is D_{2}^{P}- complete, already recognizing correct instances would be harder than Π_{2}^{P}, unless Π_{2}^{P} = D_{2}^{P}. However, the result holds also on deciding given any E, whether no E′ ⊂ E is a credulous explanation.

Due to the complexity of minimality checking, Relevance migrates to the next level of the polynomial hierarchy.

Theorem 4.11 Let P be a PDAP based on minimal credulous explanations. Then, Relevance is Σ_{3}^{P} -complete, and hardness holds even for normal P.

Now let us consider minimal skeptical explanations. Testing minimality of a skeptical explanation is much more involved than of a credulous explanation. While the latter has roughly the same complexity as testing the explanation property, the former is harder by one level of the polynomial hierarchy. Intuitively, this can be explained as follows. Since verifying a credulous explanation E is in Σ_{2}^{P}, it has a polynomial-size “proof” which can be checked with an NP oracle in polynomial time. Thus, if we ask for a smaller explanation E′ ⊂ E, we can simultaneously guess E′ and its proof, and check the proof in polynomial time with the NP oracle. However, verifying a skeptical explanation E is Π_{2}^{P} -hard, and hence E does not have such a “proof”. Here, verification needs the full power of a Π_{2}^{P} oracle.

Theorem 4.12 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if a skeptical explanation E for P is minimal is Π_{3}^{P} -complete, with hardness holding even for normal P.^{5}

Note that recognizing minimal skeptical explanations is in Π_{3}^{P}, since the complexity of deciding minimality (Π_{3}^{P}) dominates the complexity of the explanation property (“only” D_{2}^{P}), and is also complete for this class (See Theorem A.2).

The complexity of deciding relevance of a hypothesis increases by the same amount as testing minimality if skeptical explanations are used instead of credulous explanations. In fact, the problem resides at the fourth level of the polynomial hierarchy.

Theorem 4.13 Let P be a PDAP based on minimal skeptical explanations. Then, problem Relevance is Σ_{4}^{P} -complete, with hardness even for normal P.

There is no well-known nonmonotonic logic that has similar complexity, and thus one can not take advantage of theorem provers for such logics to perform skeptical abduction from default theories.

5 Tractable cases

From the practical side, the results of the previous section are discouraging, since abduction from default theories has even higher complexity than deduction, in particular for skeptical explanations. As a consequence, an implementation that works efficiently on all inputs is not possible. But this does not mean tht it is impossible to come up with solutions that work in practice. Several methods to cope with NP-hard problems are known [41, 9], among which the following two are most popular: identifying (natural) problem restrictions that guarantee tractability and approximation methods.

5Note that here, as opposed to checking minimality of credulous explanations, recognizing correct problem instances (D_{2}^{P}) is not harder than deciding the minimality (cf. footnote 4).

Concerning approximation, two directions are viable. One is to find a notion of approximate inference that reduces complexity, in the spirit of [55, 10]. The other is to use heuristic algorithms that work well in practice; in case of the classical satisfiability problem, the greedy algorithm (GSAT) [56] has proven to be a valuable method for solving moderately-sized instances efficiently. However, GSAT and similar algorithms are designed for problems that are in NP; it is not known how to apply GSAT in order to solve problems that are hard for Σ_{2}^{P} or Π_{2}^{P} efficiently. In general, little is known about approximation of problems in the polynomial hierarchy, as well as PSPACE-complete problems [14].

For fragments of default logic from which the abductive reasoning tasks are in NP, GSAT is applicable. An example is credulous abduction from default theories where all propositional formulas are from a tractable fragment of the propositional language, e.g. Horn formulas or Krom formulas (conjunctions of clauses with at most two literals). In such a case, classical inference ⊢ vanishes as source of complexity. In particular, the Σ_{2}^{P} -complete abductive reasoning tasks fall back to NP. Therefore, after a polynomial-time transformation of the reasoning task to the classical satisfiability problem, we can apply GSAT to solve the reasoning tasks efficiently.

Identifying tractable cases in terms of suitable restrictions on the input is the “classical” way of tackling a hard problem. This approach requires that all sources of complexity are dried up; default abduction suffers from up to four such sources. In particular, the underlying default reasoning tasks (which embody the complexity of classical inference and the number of extensions) must be tractable. The excellent work of Kautz and Selman [35] and Stillman [58] gives a very detailed picture of polynomial vs. intractable cases of default reasoning. The following two classes of default theories ⟨W, D⟩ are among the many fragments of default logic they considered:

Literal-Horn [35]: W is a set of literals and each default in D is Horn, i.e., of form \frac{a_{1}∧···∧a_{k}:ℓ}{ℓ}, where the a_{i}’s are atoms and ℓ is a literal.

Krom-pf-normal [58]: W is a set of Krom formulas, and each default in D is of form \frac{:ℓ_{1}∧···∧ℓ_{k}}{ℓ_{1}∧···∧ℓ_{k}}, where all ℓ_{i}’s are literals.

For those classes, tractability of credulous inference ⟨W, D⟩ ⊢_{c} ℓ′ for a single literal ℓ′ was shown. In fact, these classes are the maximal classes in the hierarchy of default classes for which this inference task is tractable, cf. [58]. Note that Literal-Horn theories include factual knowledge bases, extended by simple default rules; however, they allow to express e.g. the close world assumption (CWA), or rules so that their application does not lead to inconsistency.

Based on generalizations of the quoted results, we obtain some tractable cases of credulous default abduction. Similar tractability results for skeptical default abduction are unlikely, since the underlying skeptical inference ⟨W, D⟩ ⊢_{s} ℓ is co-NP-complete in both cases (for Literal-Horn, cf. [35, Theorem 7.3]; for Krom-pf-normal, see Proposition B.3 in Appendix B).

The following lemma generalizes [35, Theorem 6.5], which is formulated for a single literal ℓ rather than a conjunction ℓ_{1} ∧ ⋯ ∧ ℓ_{m} of literals (see Appendix B for the proof).

Lemma 5.1 Let ⟨W, D⟩ be a Literal-Horn default theory, and let ℓ_{1}, …, ℓ_{m} be literals. Then, deciding ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is possible in O(m · n) time, where n is the length of the input.

This result is established by reducing ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧⋯∧ℓ_{m}, apart from the trivial cases where W or ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is not consistent, to a classical inference problem H ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m} where H is a Horn theory that is linear time constructible (see the proof in Appendix B); applying standard linear time algorithms for Horn satisfiability (e.g. unit resolution [40]), H ⊢ ℓ_{i} can be decided in linear time, and thus H ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is decidable in O(m · n) time.^{6} Thus, we obtain the lemma.

For Krom-pf-normal, an analogous generalization is not evident; indeed, the problem ⟨W, D⟩ ⊢_{c} ℓ_{1}∧⋯∧ℓ_{m} is NP-hard (see Proposition B.1 in Appendix B). However, a generalization is possible if the conjunction is small. In what follows, we call a set L of literals small iff |L| ≤ b for some fixed constant b.

Lemma 5.2 Let ⟨W, D⟩ be Krom-pf-normal, and let L = {ℓ_{1}, …, ℓ_{k}} be a small set of literals. Then, deciding ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{k} is possible in O(|D|^{b} · n) time, i.e., in polynomial time.

For convenience, we introduce some additional notation for the rest of this section. For any literal ℓ, we denote by ∼ℓ the literal opposite to ℓ, i.e., ∼ℓ = x if ℓ = ¬x, and ∼ℓ = x if ℓ = ¬x.

5.1 Credulous abduction from Literal-Horn default theories

For this class, the main abductive reasoning tasks are tractable.

Theorem 5.3 Let P = ⟨H, M, W, D⟩ be a PDAP based on credulous explanations, such that ⟨W, D⟩ is Literal-Horn. Then, Consistency, Relevance, and Necessity can be solved in O(|M| · n) time, where n is the length of P.

Proof. Construct a Literal-Horn T 1 = ⟨W, D1⟩, where

D1 = \{ \frac{b_{h}:h}{h}, \frac{:¬b_{h}}{¬b_{h}} , \frac{:b_{h}}{b_{h}} | h ∈ H\} ,

where each b_{h} is a new propositional atom. It is not hard to see that P has an explanation iff W is consistent and T 1 ⊢_{c} m_{1} ∧ ⋯ ∧ m_{k}, where M = {m_{1}, …, m_{k}}. T 1 can be constructed in O(n) time, and by Lemma 5.1, T 1 ⊢_{c} m_{1} ∧ ⋯ ∧ m_{k} can be decided in O(|M| · n) time. Hence, Consistency can be decided in O(|M| · n) time. By Corollary 4.3, Relevance and Necessity can be easily reduced (in fact, in linear time) to Consistency resp. its complement. Thus, they are also solvable in O(|M| · n) time.

Notice that a polynomial algorithm for finding an explanation, (even containing a given hypothesis), can be extracted from the proof of Theorem 5.3 and Lemma 5.1, which is outlined in Table 3.

6This is even possible in O((m^{−} + 1) · n) time, where m^{−} is the number of negative literals ℓ_{i} (cf. proof of Lemma 5.1); however, to our knowledge, no O(n), i.e., linear time algorithm is known. The bounds for the polynomial-time results in Section 5.1 can be sharpened accordingly, by replacing “|M|” with “|M^{−}| + 1”, where M^{−} is the set of negative literals in M.

Algorithm LH-Cred-Explanation(H, M, W, D);

input: A propositional Literal-Horn DAP P = ⟨H, M, W, D⟩.
output: A credulous explanation E for P, if one exists.

begin (* W inconsistent; no explanation *) for each ℓ ∈ W do if ∼ℓ ∈ W then stop; (* M inconsistent; no explanation *) for each ℓ ∈ M do if ∼ℓ ∈ M then stop; ϕ := conjunction of all literals in M; (* P has an explanation iff T 1 ⊢_{c} ϕ*) construct T 1 = ⟨W, D1⟩ from P; (* proof of Lemma 5.1 *) construct Horn theory H s.t. H ⊢ ϕ iff T 1 ⊢_{c} ϕ; (* no explanation exists *) if H ⊬ ϕ then stop; (* M is the least model of H *) M := {x | atom x, H ⊢ x}; C := W ∪ M ∪ {¬x | (α : ¬x/¬x) ∈ D1, M ⊧ α, M |̸= x }; (* E is an explanation *) E := {h ∈ H | h ∈ C, b_{h} ∈ C}; output(E);

end LH-Cred-Explanation.

Table 3: Algorithm for finding a credulous explanation (Literal-Horn)

Algorithm LH-Min-Cred-Explanation(H, M, W, D);

input: A propositional Literal-Horn DAP P = ⟨H, M, W, D⟩.
output: A minimal credulous explanation E for P, if one exists.

begin E := LH-Cred-Explanation(H, M, W, D); (* try to remove each h ∈ R from E *) if E is undefined then stop else R := E; (* try to remove h from E *) while R ≠ ∅ do begin select h ∈ R;

E1 := LH-Cred-Explanation(E\ {h} , M, W, D); (* h is in all explanations E′ ⊆ E *) if E1 is undefined then R := R\ {h} (* take the smaller explanation E1 *) else begin E := E1; R := E; end;

end; output(E);

end LH-Min-Cred-Explanation.

Table 4: Algorithm for finding a minimal credulous explanation (Literal-Horn)

Each step of the algorithm can be done in O(n) time, except the test H ⊢ ϕ, which is possible in O(|M| · n) time; hence, the total running time is O(|M| · n). The algorithm can also be used to solve Relevance and Necessity, utilizing Corollary 4.3, in O(|M| · n) time.

Moreover, even a minimal credulous explanation can be found in polynomial time. Indeed, it is easy to see that an explanation E for a PDAP P = ⟨H, M, W, D⟩ is minimal if and only if ⟨E\ {h} , M, W, D⟩ has no explanation for each h ∈ E. Thus, given an explanation E for P as above, one can find a minimal one by trying to subsequently eliminate hypotheses from E, as done in the algorithm in Table 4. Thus, we obtain the following result.

Theorem 5.4 Let P = ⟨H, M, W, D⟩ be a PDAP where ⟨W, D⟩ is Literal-Horn. Then, a minimal credulous explanation for P can be found in O(|H| · |M| · n) time, where n is the length of P.

However, Relevance based on minimal credulous explanations for PDAPs with Literal-Horn default theories can be shown to be NP-complete (Proposition B.4). Recall that necessity of a hypothesis h in minimal explanations coincides with necessity of h in arbitrary explanations (Proposition 4.1), and thus also Necessity is polynomial.

5.2 Credulous abduction from Krom-pf-normal default theories

Tractability of credulous inference of a literal from a Krom-pf-normal theory allows us to obtain another tractable fragment of abduction from default theories.

The following lemma on inference of a literal from a Krom theory augmented by literals is important for credulous inference of a set of literals from a Krom-pf-normal default theory.

Lemma 5.5 Let S be a (propositional) Krom theory and ℓ a literal, and let L = {ℓ_{1}, …, ℓ_{k}} be a set of literals such that (i) S ∪ L is consistent, (ii) S ∪ L ⊢ ℓ and S ⊬ ℓ. Then, S ∪ {ℓ_{i}} ⊢ ℓ for some ℓ_{i} ∈ L.

From the lemma, we obtain the following criterion for credulous inference of a literal. For convenience, let for each default d = \frac{:ℓ_{1}∧···∧ℓ_{k}}{ℓ_{1}∧···∧ℓ_{k}} denote lit(d) = \{ℓ_{1}, …, ℓ_{k}\}, and let for each set D of such defaults denote lit(D) = ⋃_{d∈D} lit(d).

Proposition 5.6 Let T = ⟨W, D⟩ be a Krom-pf-normal default theory and let L = {ℓ_{1}, …, ℓ_{m}} be a set of literals. Let L1 = {ℓ_{i} ∈ L | W ⊬ ℓ_{i}}. Then, T ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} iff (a) L1 is empty, or (b) there exists a subset D1 ⊆ D such that

(b.1) |D1| ≤ |L1|,

(b.2) W ∪ lit(D1) is consistent, and

(b.3) W ∪ lit(D1) ⊢ ℓ, for each ℓ ∈ L1.

Based on this proposition, the algorithm in Table 5 decides whether a conjunction of literals is a credulous consequence of a Krom-pf-normal default theory. The analysis of its running time yields the following result.

Theorem 5.7 Let T = ⟨W, D⟩ be a Krom-pf-normal default theory, and let L = {ℓ_{1}, …, ℓ_{m}} be a set of literals. Then, T ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} can be decided using Krom-PFN-Cred-Inf in O(|D|^{m} · m · n) time, where n is the length of the input.

Thus, in particular, if L = {ℓ_{1}, …, ℓ_{k}} is small, we obtain a polynomial bound O(|D|^{k} ·n); this proves Lemma 5.2 at the beginning of this section. Recall that tractability of credulous literal inference can most likely not be generalized to an arbitrary conjunction of literals, since this problem is NP-complete (Proposition B.1).

By a reduction to credulous default reasoning, one can show that credulous abduction from a Krom-pf-normal default theory is polynomial if the set of manifestations is small.

Algorithm Krom-PFN-Cred-Inf(W, D, ϕ);

input: A propositional Krom-pf-normal default theory ⟨W, D⟩,

a conjunction of literals ϕ = ℓ_{1} ∧ ⋯ ∧ ℓ_{m}.

output: “Yes” if ⟨W, D⟩ ⊢_{c} ϕ, “No” otherwise.

begin L1 := { ℓ_{i} | W ⊬ ℓ_{i}, 1 ≤ i ≤ m }; (* W ⊢ ϕ; thus ϕ is in any extension *) if L1 = ∅ then output(“Yes”) else for each D1 ⊆ D s.t. |D1| ≤ |L1| do

(* lit(D1) = all literals in D1; S is Krom *) begin S := W ∪ lit(D1);

(* m + 1 × linear time *) if S ⊬ ⊥ and S ⊢ ℓ_{i} for all ℓ_{i} ∈ L1 then begin output(“Yes”); stop; end;

end; output(“No”);

end Krom-PFN-Cred-Inf.

Table 5: Algorithm for credulous inference of a conjunction of literals (Krom-pf-normal)

Theorem 5.8 Let P = ⟨H, M, W, D⟩ be a PDAP based on credulous explanations such that M = {ℓ_{1}, …, ℓ_{k}} is small and ⟨W, D⟩ is Krom-pf-normal. Then, Consistency, Relevance, and Necessity can be solved in O(|D|^{b} · n) time, where n is the length of P.

Unfortunately, Theorem 5.8 can not be generalized to an arbitrary set M of literals. In fact, due to the NP-hardness of ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} for Krom-pf-normal ⟨W, D⟩, the problem is clearly NP-hard.

Like in the case of Literal-Horn default theories, a polynomial time algorithm for finding a credulous explanation can be extracted from the proof. As shown below, there are efficient and simple algorithms for finding all minimal credulous explanations of a such a PDAP. Thus, we do not further elaborate on this point.

Interestingly, the number of hypotheses in a minimal credulous explanation is bounded by the number of manifestations. Intuitively, this is explained by the fact that a manifestation can always be explained by a single hypothesis.

Proposition 5.9 Let E be any minimal credulous explanation for a PDAP P = ⟨H, M, W, D⟩ where ⟨W, D⟩ is Krom-pf-normal and M is finite. Then, |E| ≤ |M|.

In particular, for a single manifestation (M = {ℓ}), the minimal explanations consist of single hypotheses, if hypotheses are needed at all for an explanation. A consequence of this characterization is that all minimal credulous explanations can be computed by testing all subsets E ⊆ H with |E| ≤ |M| time, which is done by the algorithm in Table 6. The correctness of the algorithm follows from Proposition 5.9 and the correctness of Krom-PFN-Cred-Inf. If the set of manifestations M is small, then the algorithm runs in polynomial time, which is captured by the next theorem.

Theorem 5.10 Given a PDAP P = ⟨H, M, W, D⟩ where ⟨W, D⟩ is Krom-pf-normal and M is small, all minimal credulous explanations for P can be computed in time O(|H|^{b} · |D|^{b} · n), where n is the length of P.

Algorithm All-KPFN-Min-Cred-Exp(H, M, W, D);

input: A propositional Krom-pf-normal DAP P = ⟨H, M, W, D⟩.
output: All minimal credulous explanations E for P.

begin ϕ := conjunction of all literals in M; Min Expl := ∅; (* 2 × linear time; no explanation exists *) if W ⊢ ⊥ or ϕ ⊢ ⊥ then stop; for i := 0 to |M| do

for each E ⊆ H s.t. |E| = i do

if W ∪ E ⊬ ⊥ and E′ ∉ Min Expl, for every E′ ⊂ E then if Krom-PFN-Cred-Inf(W ∪ E, D, ϕ) = “Yes” then begin output(E);

Min Expl := Min Expl ∪ { E }; end; end All-KPFN-Min-Cred-Exp.

Table 6: Algorithm for finding all minimal credulous explanations (Krom-pf-normal)

(Standard search data structures are used to represent Min Expl.) As a consequence, also Relevance and Necessity for minimal explanations are polynomial if M is small.

6 Complexity of first-order case

In the previous sections, we considered the computational cost of abduction from propositional DAPs. However, for knowledge representation in practice, a language allowing for predicates is more relevant and realistic, as in the examples we considered above.

Since default logic subsumes first-order logic, default reasoning based on unrestricted first-order logic is undecidable in general; in fact, as shown already by Reiter, the credulous consequences are even not recursively enumerable [52]. Hence, also abduction from default logic is highly undecidable in general.

However, default logic is decidable in the common setting of the domain closure axiom (∀x. x = c_{1}∨⋯∨x = c_{n}) and the unique names assumption (⋀_{i<j} c_{i} ≠ c_{j}), where the language is functionfree. In the following, we implicitly assume this setting for first-order default logic; notice that this was intuitive for the examples we considered.

In this setting, an existential quantifier ∃xϕ(x) is equivalent to ϕ(c_{1})∨⋯∨ϕ(c_{n}), and a universal quantifier ∀xψ(x) to ψ(c_{1}) ∧ ⋯ ∧ ψ(c_{n}). Therefore, every first-order formula can be rewritten to a quantifier-free formula, which, however, is in general exponentially larger. Each default rule d with free variables x = x_{1}, …, x_{m} gives rise to an exponential number (n^{m}) of ground defaults. As a consequence, a first-order default theory T = ⟨W, D⟩ reduces to an equivalent propositional default theory T^{∗} = ⟨W^{∗}, D^{∗}⟩ that can be exponentially larger.

Intuitively, this means that the complexity of first-order default reasoning is (at most) exponentially higher than the complexity of propositional default reasoning (Σ_{2}^{P}). The appropriate class for such complexity is the exponential analogue of Σ_{2}^{P} = NP^{NP}, which is the class Σ_{2}^{E} = NEXP^{NP}, i.e. nondeterministic exponential time ( O(2^{p(n)}) ) rather than polynomial time ( O(p(n)) ) with an oracle for NP (“exponential” comes in by the reduction of T to T^{∗}, after which the algorithms for propositional DAPs can be applied.)

In fact, it is shown in [29] that credulous first-order default reasoning is complete for Σ_{2}^{E}; as a simple consequence, skeptical reasoning is complete for Π_{2}^{E} = co-Σ_{2}^{E}. The proof in [29] establishes that these results hold even if W is a universal theory and no quantifiers occur in D. Moreover, like in the propositional case, they hold if in addition the default theory is normal and W is a consistent set of literals (this is immediate from [29] and results in [8]).

The polynomial-time transformations of default reasoning to the main credulous default abduction tasks in 1–3 established the hardness parts of Theorem 4.6. Clearly, these transformations also work for first-order theories. Therefore, from the complexity results for first-order default reasoning, it follows that Consistency and Relevance are Σ_{2}^{E}-hard and Necessity is Π_{2}^{E}-hard for credulous default abduction in the first-order case. On the other hand, it is clear from the above discussion that any first-order DAP P can be reduced in exponential time to an equivalent propositional DAP P^{∗}; as a consequence, the main credulous first-order default abduction problems belong to the classes Σ_{2}^{E} and Π_{2}^{E}, respectively. Thus, we arrive at the following result.

Theorem 6.1 Let P be a first-order DAP under the domain closure axiom and unique names assumption, based on credulous explanations. Then (i) Consistency is Σ_{2}^{E}-complete, (ii) Relevance is Σ_{2}^{E}-complete, and (iii) Necessity is Π_{2}^{E}-complete.

Analogous results follow for recognizing a credulous explanation and checking minimality of a credulous explanation. Thus, the complexity of credulous abduction is exponentially higher in the first-order case than in the propositional context. Note that this definitely proves intractability, even if P = NP would be true. Indeed, EXPTIME, i.e., the class of all problems that can be decided in exponential time, is included in Σ_{2}^{E} and Π_{2}^{E}, and so all EXPTIME-complete problems. Those problems have provably exponential running time, which implies that every problem that is complete for Σ_{2}^{E} or Π_{2}^{E} has provably an exponential lower bound on its running time.

For skeptical first-order abduction and minimal explanations, an analogous exponential increase in complexity (from Σ_{k}^{P} to Σ_{k}^{E}, Π_{k}^{P} to Π_{k}^{E}, etc) strongly suggests itself. From the discussion above, it is clear that for each problem, the exponential analogue is an upper complexity bound. Matching hardness results can be obtained by applying the results on evaluating second-order predicate formulas over finite structures in [29] (see end of Appendix A for more details).

We close this section with some remarks on tractable first-order default abduction. Like the intractability results, also the polynomial-time results in Section 5 scale up from the propositional case. A –quite moderate– extension of propositional Literal-Horn and Krom-pf-normal default theories ⟨W, D⟩ to the first-order case is to allow also universally quantified Krom clauses (resp. literals) besides propositional (ground) clauses (resp. literals) in W, and to allow also nonground literals ℓ(x) in defaults besides ground literals. Unfortunately, reducing a first-order DAP P to the equivalent propositional DAP P^{∗}, on which the polynomial time algorithms in Section 5 can be applied, does not give a polynomial algorithm, since the reduction is exponential. However, no substantially better algorithms are available, since even under this restrictive setting, abduction is intractable.

To substantiate this claim, we first consider the class of first-order Literal-Horn default theories. It is easy to see that logic programs without negations (i.e., datalog programs) are a fragment of this class. Indeed, each program rule A_{0} ← A_{1}, …, A_{n}, where the A_{i} are atoms, can be equivalently represented by the Horn default \frac{A_{1}∧···∧A_{n} : A_{0}}{A_{0}} . As a consequence, credulous as well as skeptical deductive inference from a default theory of this form is EXPTIME-hard, since inference of a fact from a datalog program is known to be EXPTIME-hard (this is implicit in the work of [11, 61] and part of the folklore now). Based on this, it is easily established that the main credulous abduction tasks from a first-order Literal-Horn default theory are EXPTIME-complete problems. Again, this definitely proves intractability, since no polynomial-time algorithms for such problems are possible.

Similarly, also abduction from Krom-pf-normal default theories is intractable in the first order case. In fact, one can show that credulous inference of a single literal from such a default theory is NP-hard, even for instances of simple form (see Proposition B.5 in the Appendix B). Therefore, also credulous abduction is NP-hard (resp. co-NP-hard), even if only a single manifestation has to be explained.

Tractability as in the propositional case can be gained, however, for both classes by imposing a constant upper bound on the arity of predicates; this guarantees that a first-order DAP P reduces to P^{∗} in polynomial time. Thus, by applying the polynomial algorithms from Section 5 on P^{∗} afterwards, we have a polynomial overall algorithm.

7 Conclusion and further research

We have investigated abduction from default theories. Starting from motivating examples, we looked how abduction can be reasonably performed; this led us to a basic model of abduction from default theories. The two inference modalities of classical default reasoning, credulous and skeptical inference, give rise to two credulous and skeptical abduction; both are useful in practice. Credulous abduction appears to be useful e.g. for diagnosis, while skeptical abduction is appealing for planning. This corresponds to previous applications of abduction in diagnosis (cf. [44, 46]) and planning and plan recognition (cf. [24, 42]).

Moreover, we have analyzed the computational complexity of the abduction model, both in the propositional as well as in the predicate case. The main results on the complexity of abduction from propositional default theories are summarized Table 1. They are discouraging from the practical point, since they show that the main reasoning tasks are highly intractable, and hence polynomial time algorithms are unrealistic. In fact, the complexity ranges from the second level of the polynomial hierarchy (Σ_{2}^{P}, Π_{2}^{P}), which is the level of deductive default reasoning and abduction from classical theories, up to fourth level (Σ_{4}^{P}), the “square” of the complexity of default reasoning. Interestingly, credulous abduction is less complex than skeptical abduction, by one level in the polynomial hierarchy; thus, abductive default diagnosis is less complex than abductive default planning. A somewhat positive finding is that the least complex variant, credulous default abduction, can be shortly transformed into classical default reasoning, and thus theorem provers like the DeReS system [13] can be efficiently used to perform abduction. However, this property is lost as soon as one uses minimal explanations, which are more complex.

In the first-order case, under some common restrictions (in full first-order logic, all abduction problems are trivially undecidable) the complexity scales up by an exponential factor, and is provably intractable.

Exploring the tractability frontier, we have also shown that credulous abduction from the previously known classes of propositional Literal-Horn and Krom-pf-normal default theories [35, 58] is tractable. Unfortunately, these results do not carry over to the first-order case.

Several issues remain for future work. One is to find more applications for abduction from default theories, and to see how credulous and skeptical abduction apply therefore. It would also be interesting to see whether other modes of abduction, besides credulous and skeptical abduction, are relevant.

Further issues more on the foundational side are other concepts of abductive explanation, as well variants of classical default logic for the underlying theory. In the present paper, we focused on the most simple concepts of abduction explanation that have been considered in the literature. A number of different notions of acceptable explanations exist, cf. [43, 7, 22, 48], which are based on a preference between explanations; however, all single out minimal explanations. Most wellknown are explanations that have minimal size (cf. [43]) and explanations that have minimal cost (or weight resp. probability [48, 47]). Results for abduction from classical theories [22] suggest that abduction from default theories using explanations of smallest size or smallest cost yield problems complete for classes Δ_{k}^{P} and Δ_{k}^{P} [O(log n)] of the (refined) polynomial hierarchy [31]. In particular, these concepts are not strong enough to lower the complexity of default abduction.

On the other hand, several variants and extensions of Reiter’s default logic have been introduced, motivated by some weaknesses of the original approach, e.g., [5, 4, 49, 26, 39]. It would be interesting to investigate how abduction behaves on these formalisms. In particular, stationary default logic [4, 49] would be interesting, since there the complexity of skeptical reasoning is lower than in classical default logic [28]; as a consequence, also skeptical abduction has lower complexity.

Also on the algorithmic side, interesting issues remain for further work. One important is, of course, to find other fragments of default logic on which abduction is tractable. In particular, fragments that are not within a propositional language would be interesting. Apart from that, approximation methods that allow more efficient abductive default reasoning are needed, either on a semantical basis, cf. [55, 10, 54] or on a computational approach [56]. Anyway, the results about tractability make clear that good approximation algorithms are needed. Note that quite a bit is known about approximation of probabilistic inference problems [17, 54] as well #Pcomplete problems [60] (see also [31]). However, not much is known about approximation of problems complete for classes of the polynomial hierarchy above NP and for PSPACE-complete problems cf. [14].

Finally, it would be worthwhile to thoroughly investigate abduction from theories in knowledge representation formalisms different from default logic. In the context of logic programming, the study and use of abduction is meanwhile established, cf. [33]. Complexity results for abductive logic programming [23] that are similar to those for abduction from default theories support the view of the intimate relationship between these formalisms. Similar results for other closely related formalisms such as autoepistemic logic are plausible.

Acknowledgement

The authors would like to thank a referee for his helpful comments on this paper. In particular, they appreciate his pointers to papers on approximation of probabilistic inference and #P problems.

A Appendix: Proofs of general case complexity

The classes of the polynomial hierarchy have problems complete under polynomial-time transformations involving quantified Boolean formulas (QBFs), which we will refer to in many proofs. A QBF is an expression of the form

Q_{1}X_{1}Q_{2}X_{2} ⋯ Q_{k}X_{k} E, k ≥ 1, (4)

where E is a Boolean expression whose (propositional) variables are from pairwise disjoint nonempty sets of variables X_{1}, …, X_{k}, and the Q_{i}’s are alternating quantifiers from {∃, ∀}, for all i = 1, …, k. If Q_{1} = ∃ the we say the QBF is k-existential, otherwise it is k-universal. Validity of QBFs is defined in the obvious way by recursion to variable-free Boolean expressions. We denote by QBF_{k,∃} (resp., QBF_{k,∀}) the set of all valid k-existential (resp., k-universal) QBFs.

Deciding, given a k-existential QBF Φ (resp. a k-universal QBF Ψ), whether Φ ∈ QBF_{k,∃} (resp. Ψ ∈ QBF_{k,∀}), is a classical Σ_{k}^{P} -complete (resp. Π_{k}^{P} -complete) problem; deciding the conjunction (Φ ∈ QBF_{k,∃}) ∧ (Ψ ∈ QBF_{k,∀}) is complete for D_{k}^{P}.

We introduce some additional notation. For a set A of propositional atoms, we denote by ¬A the set {¬a | a ∈ A} and by A′ the set of atoms {a′ | a ∈ A}. Moreover, for a Boolean formula F and a set X1 ⊆ X of atoms, we denote by F_{X1}^{X} the formula obtained from F by replacing each occurrence of an atom x ∈ X1 in F by true and each occurrence of an atom x ∈ X\X1 by false; as X will be understood, we write simply F_{X1}.

Theorem 4.8 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if E ⊆ H is a skeptical explanation for P is D_{2}^{P}-complete.

Proof. As already argued, the problem is in D_{2}^{P}. To show hardness, we reduce deciding whether, given two propositional default theories T 1 = ⟨W 1, D1⟩ and T 2 = ⟨W 2, D2⟩, it holds that T 1 has a consistent extension and T 2 ⊢_{s} x to the problem; since the problems are Σ_{2}^{P} -hard and Π_{2}^{P} -hard [27], respectively, this will clearly prove D_{2}^{P}-hardness. Without loss of generality, T 1 and T 2 have different propositional atoms, x does not occur in T 1, and W 2 = ∅ (thus T 2 has only consistent extensions), cf. [27]. Define P = ⟨∅, {x} , W 1 ∪ W 2, D1 ∪ D2⟩. It is easily seen that ∅ is a skeptical explanation of P iff T 1 has a consistent extension and T 2 ⊢_{s} x; this proves the result.

Theorem 4.9 Let P be a PDAP based on skeptical explanations. The problem (i) Consistency is Σ_{3}^{P} -complete, (ii) Relevance is Σ_{3}^{P} -complete and (iii) Necessity is Π_{3}^{P} -complete, with hardness even for normal P.

Proof. Membership. A guess E for a skeptical explanation for P can be verified by two calls to Σ_{2}^{P} oracle, by checking whether ⟨W ∪ E, D⟩ has a consistent extension and and whether ⟨W ∪ E, D⟩ ⊢_{s} ϕ, where ϕ is the conjunction of all formulas in M. Hence, it is easy to see that (i), (ii), and the complement of (iii) are in Σ_{3}^{P}.

Hardness. (i) We describe here a transformation of deciding if a QBF Φ = ∃X∀Y ∃ZF is valid. Define

W = \{ f ↔ F \} , D = \{ \frac{: ¬a}{¬a}, \frac{: a}{a} | a ∈ X ∪ Y \} ∪ \{ \frac{: F}{F} \}

where f is a new atom, and P = ⟨X ∪ ¬X, {f} , W, D⟩. Note that P is a normal PDAP. We claim that P has a skeptical explanation iff Φ is valid. “⇒”: Assume E is a skeptical explanation for P. Let X1 = E ∩ X, and let Y 1 ⊆ Y be

arbitrary. Then, clearly

A = T h(W ∪ E ∪ X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1))

is an extension of the default theory ⟨W ∪ E, D\ \{\frac{:F}{F} \}⟩. By semi-monotonicity of normal default theories ([52]; see Section 2), ⟨W ∪ E, D⟩ must have an extension B such that A ⊆ B. Clearly, B must be consistent. Moreover, since E is a skeptical explanation for P, f ∈ B, and hence F ∈ B. Consequently, F_{X1∪Y 1} is satisfiable. Since Y 1 is arbitrary, it follows that ∀Y ∃ZF_{X1} is valid. Hence, Φ is valid.

“⇐”: Let X1 ⊆ X such that ∀Y ∃ZF_{X1} is valid. Define E = X1 ∪ ¬(X\X1). Clearly, W ∪ E is consistent. Hence, every extension A of ⟨E, D⟩ is consistent; an extension exists, since ⟨E, D⟩ is normal. Moreover, each such A and contains Y 1 ∪ ¬(Y \Y 1) for some Y 1 ⊆ Y. From the characterization of A in terms of its generating defaults and the hypothesis that ∀Y ∃ZF_{X1} is valid, it follows that F is consistent with A. Consequently, \frac{:F}{F} ∈ GD(A, ⟨E, D⟩), and hence F ∈ A; it follows f ∈ A. Since the extension A was arbitrary, it follows that E is a skeptical explanation for P. This proves the claim, which also concludes the proof of (i).

To show (ii), add h to the hypotheses in an instance of P in (i), and ask if h is relevant; for (iii), add h to the hypotheses, f ∨ h ⊃ q to the third component, change the manifestations to {q} and ask if h is necessary. Indeed, h is necessary iff P has no skeptical explanation.

Theorem A.1 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if E ⊆ H is a minimal credulous explanation E for P is D_{2}^{P}-complete, with hardness even for normal P.

Proof. It remains to show hardness. For that, consider PDAPs P1 = ⟨∅, {q_{1}} , W 1, D1⟩ as in (1) and P2 = ⟨{h} , {q_{2}} , W 2, D2⟩ as in (3) preceding Theorem 4.6, and assume that they are on distinct atoms. Then, {h} is a minimal credulous explanation of P3 = ⟨{h} , {q_{1}, q_{2}} , W 1 ∪ W 2, D1 ∪ D2⟩ iff P1 has a credulous explanation and h is necessary for P2. Since the latter problems are Σ_{2}^{P} -hard and Π_{2}^{P} -hard, respectively, and P3 is clearly normal, D_{2}^{P}-hardness of the problem follows.

Theorem 4.11 Let P be a PDAP based on minimal credulous explanations. Then, Relevance is Σ_{3}^{P} -complete, and hardness holds even for normal P.

Proof. Membership. A guess E for a minimal credulous explanation for P such that h ∈ E can be verified by two calls to an Π_{2}^{P} oracle (cf. Theorems 4.6 and 4.10). Hence, the problem is in Σ_{3}^{P}.

Hardness. We outline a reduction from deciding validity of a QBF Φ = ∃X∀Y ∃ZF. Let s and q be new atoms, and define

W = ∅
D = \{ \frac{:¬s}{¬s}, \frac{s∧Y:q}{q} , \frac{¬s∧¬F:q}{q} \} ∪ \{ \frac{x:x′}{x′} , \frac{¬x:x′}{x′} | x ∈ X \} ∪ \{ \frac{:¬y}{¬y} | y ∈ Y \} .

Let P = ⟨X ∪ ¬X ∪ Y ∪ {s} , X′ ∪ {q} , W, D⟩; note that P is normal. Claim: s is relevant for a minimal credulous explanation iff Φ is valid.

The following facts, which are straightforward, are useful for a proof of this claim: Fact 1: If E is a credulous explanation for P, then (i) x ∈ E or ¬x ∈ E, for each x ∈ X; (ii) if s ∈ E, then Y ⊆ E; and (iii) if s ∉ E, then ¬s belongs to each extension of ⟨W ∪ E, D⟩. Fact 2: for each X1 ⊆ X, the set E_{X1} = X1 ∪ ¬(X\X1) ∪ Y ∪ {s} is a credulous explanation for P. (Indeed, the set T h(W ∪ E_{X1} ∪ X′ ∪ {q}) is an extension of ⟨W ∪ E_{X1}, D⟩.)

We now prove the claim.

“⇒”: Relevance of s implies by Facts 1 and 2 that for some X1 ⊆ X, E_{X1} is a minimal credulous explanation. Thus, for each Y 1 ⊆ Y, the set E_{X1,Y 1} = X1 ∪ ¬(X\X1) ∪ Y 1 is not a credulous explanation. Since W ∪ E_{X1,Y_{1}} is consistent, it follows by semi-monotonicity of normal default theories that ⟨W ∪ E_{X1,Y 1}, D⟩ has a consistent extension A that contains

B = {¬s} ∪ X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1);

however, q ∉ A (otherwise, E_{X1,Y 1} would be an explanation.) Thus, from the characterization of A by its generating defaults, it follows that B ⊬ ¬F, i.e., B ∪ F is consistent. Consequently, the formula F_{X1∪Y 1} is satisfiable. It follows that ∃X∀Y ∃ZF is valid.

“⇐”: Let X1 ⊆ X such that ∀Y ∃ZF_{X1} is valid. Then, E_{X1} is a minimal credulous explanation for P. To show this, assume to the contrary that some smaller explanation E ⊂ E_{X1} exists. Then, from Fact 1 we have s ∉ E. The default theory ⟨W ∪ E, D⟩ must have an extension that contains q; by the properties of default logic, it follows that ¬F is provable from X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1), where Y 1 = Y ∩ E. It follows that ∀Y ∃ZF_{X1} is not valid. Contradiction.

This proves the claim. As P can be constructed in polynomial time, Σ_{3}^{P} -hardness of the problem follows.

Theorem 4.12 Let P = ⟨H, M, W, D⟩ be a PDAP. Deciding if a skeptical explanation E for P is minimal is Π_{3}^{P} -complete, with hardness holding even for normal P.

Proof. Membership. A guess for a smaller skeptical explanation E′ ⊂ E can be verified with two calls to a Σ_{2}^{P} oracle, and hence deciding the existence of such an E′ is in Σ_{3}^{P}. Consequently, the problem is in Π_{3}^{P}.

Hardness. We describe here a reduction from deciding whether a QBF Φ = ∀X∃Y ∀ZF is valid. Let s and q be new atoms, and define

D = \{ \frac{:¬s}{¬s}, \frac{s∧X:q}{q} , \frac{¬s:¬F ∧q}{¬F ∧q} \} ∪ \{ \frac{:¬x}{¬x} | x ∈ X \} ∪ \{ \frac{:y}{y} , \frac{:¬y}{¬y} | y ∈ Y \} .

Let P = ⟨X ∪ {s} , {q} , ∅, D⟩. Check that E = X ∪ {s} is a skeptical explanation for P. Claim: E is a minimal skeptical explanation for P iff Φ is valid.

In the proof of this claim, we use the following facts, which are easily established. Fact 3: E is the only skeptical explanation for P that contains s. Fact 4: For each X1 ⊆ X, (i) the default theory ⟨X1, D⟩ has for each Y 1 ⊆ Y an extension containing X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1) (follows from semi-monotonicity); (ii) each extension of ⟨X1, D⟩ contains ¬s.

Proof of the claim:

“⇒”: Let X1 ⊆ X. Then, by hypothesis, X1 is not a skeptical explanation. Hence, there exists some extension A of ⟨X1, D⟩ such that q ∉ A, which implies by (ii) of Fact 4 that ¬F ∧ q ∉ A. From the characterization of A in terms of its generating defaults, it follows that X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1) ⊢ F, where Y 1 = Y ∩ A. Thus, ∃Y ∀ZF_{X1} is valid. Since X1 is arbitrary, it follows that Φ is valid.

“⇐”: Assume that E is not minimal. Then, by Fact 3, some X1 ⊆ X exists which is a skeptical explanation. By (i) and (ii) of Fact 4, we conclude that for each Y 1 ⊆ Y, it holds that X1 ∪ ¬(X\X1) ∪ Y 1 ∪ ¬(Y \Y 1) is consistent with ¬F. Hence, ∀Y ∃Z¬F_{X1} is valid. This implies that Φ is not valid. Thus, by contraposition, validity of Φ implies that E is minimal.

This proves the claim. The result follows.

Theorem A.2 Given a PDAP P = ⟨H, M, W, D⟩ and a subset E ⊆ H, deciding whether E is a minimal skeptical explanation for P is Π_{3}^{P} -complete, with hardness holding even for normal P.

Proof. Membership. If E is not a minimal skeptical explanation, then either E is not a skeptical explanation, which can be checked with two calls to a Σ_{2}^{P} oracle, or there exists a guess E′ ⊂ E such that E′ is a smaller skeptical explanation, which can be checked by another two calls to a Σ_{2}^{P} oracle. Hence, it follows that deciding whether E is not a minimal skeptical explanation is in Σ_{3}^{P}; hence, deciding whether E is a minimal skeptical explanation is in Π_{3}^{P}.

Hardness. Follows immediately from the reduction in the hardness part of the proof of Theorem 4.12: take E = X ∪ {s}.

Theorem 4.13 Let P be a PDAP based on minimal skeptical explanations. Then, problem Relevance is Σ_{4}^{P} -complete, with hardness even for normal P.

Proof. Membership. A guess for a minimal skeptical explanation E for P such that h ∈ E can be verified with one call to a Σ_{3}^{P} oracle (cf. Theorem A.2).

Hardness. We outline a reduction from deciding validity of a QBF Ψ = ∃R∀X∃Y ∀ZF, which is an extension to the reduction in the proof of Theorem 4.12. Let as there be s and q new atoms, and define

D1 = D ∪ \{ \frac{r′:r∧r′′}{r∧r′′} , \frac{¬r′:¬r∧r′′}{¬r∧r′′} | r ∈ R \} ,

where D is the same set of defaults as in the proof of Theorem 4.12. Define P = ⟨H, R′′ ∪ {q} , ∅, D1⟩, where H = R′ ∪ ¬R′ ∪ X ∪ {s}. Note that P is normal; if W would be empty, then P would be identical to the PDAP in the proof of Theorem 4.12). We observe the following facts on P: Fact 5: Let E be any skeptical explanation for P. Then, either r′ ∈ E or ¬r′ ∈ E, but not both simultaneously, for each r ∈ R.

Proof: Note that the manifestation r′′ can be only explained by either r′ or ¬r′, which can not be derived by applying defaults. Clearly, it is not possible that r and ¬r are both in E. Claim: Let E1 ⊆ H and R1 ⊆ R such that E1 ∩ (R′ ∪ ¬R′) = R1′ ∪ ¬(R\R1)′. Then, E1 is a skeptical explanation for P iff E = E1\(R′ ∪ ¬R′) is a skeptical explanation for the PDAP P_{Φ} = ⟨H_{Φ}, M_{Φ}, W_{Φ}, D_{Φ}⟩ constructed for Φ = ∀X∃Y ∀ZF_{R1} in the proof of Theorem 4.12.

Proof of the claim: Let D2 be the set of defaults obtained from D1 by replacing ¬F ∧ q with ¬F_{R1} ∧ q.

“⇒”: Each extension of ⟨E1, D1⟩ must contain R1 ∪ ¬(R\R1). (Otherwise, R′′ would not be explained.) From this, it is not difficult to see that ⟨E1, D2⟩ has the same extensions as ⟨E1, D1⟩. Moreover, from the occurrences of r, r′ and r′′ in ⟨E1, D2⟩, it is clear that the extensions of ⟨E1, D2⟩ restricted to the language over the atoms X ∪Y ∪Z ∪{s, q} are precisely the extensions of ⟨E, D_{Φ}⟩. Hence, it follows that E is a skeptical explanation for P_{Φ}.

“⇐”: Assume that E is aa skeptical explanation of P_{Φ}. Let B be an arbitrary extension of ⟨E1, D1⟩. Clearly, B is consistent. To show that E1 is a skeptical explanation for P, it suffices to prove that R′′ ∪ {q} ⊆ B. We consider two cases.

(i) s ∈ E1. Then, s ∈ E; since E is a skeptical explanation for P_{Φ}, we conclude that X ⊆ E, and hence X ⊆ E1. Consequently, q ∈ B by the default \frac{s∧X:q}{q}; moreover, R′′ ⊆ B since for each r ∈ R, one of the defaults \frac{r′:r∧r′′}{r∧r′′} and \frac{¬r′:¬r∧r′′}{¬r∧r′′} is applicable. (Note that the default \frac{¬s : ¬F ∧¬q}{¬F ∧¬q} is not applicable). (ii) s ∉ E1. Then, ¬s ∈ B. Let Y 1 = B ∩ Y. Since E is a skeptical explanation for P_{Φ}, we conclude that the set

E ∪ {¬F_{Φ} ∧ q} ∪ ¬(X\E) ∪ Y 1 ∪ ¬(Y \Y 1) ∪ { ¬s }

is consistent. This can be easily established by semi-monotonicity of normal default logic: start to build an extension of ⟨E, D_{Φ}⟩ by applying the appropriate default from \frac{:y}{y}, \frac{:¬y}{¬y} for each y ∈ Y, after that all defaults \frac{:¬x}{¬x}, for x ∈ X\E, and then \frac{: ¬s}{¬s}; the default \frac{¬s:¬F_{Φ}∧q}{¬F_{Φ}∧q} must be applicable thereafter, as this is the only possibility to join q to the extension.) Consequently, also the set

C = E1 ∪ {r ∧ r′′ | r ∈ R1}∪{¬r ∧ r′′ | r ∈ R\R1} ∪ {¬F ∧ q} ∪ ¬(X\E) ∪ Y 1 ∪ ¬(Y \Y 1) ∪ { ¬s }

must be consistent. Thus, by the characterization of an extension in terms of its generating defaults, we conclude that B = T h(C). Hence, it follows that R′′ ∪ {q} ⊆ B.

It follows that E1 is a skeptical explanation for P. This proves the claim.

From Fact 5 and the claim, it follows that s is relevant for some minimal skeptical explanation for P iff for some R1 ⊆ R, the formula ∀X∃Y ∀ZF_{R1} is valid, i.e., Ψ is valid. As P is efficiently constructible from Ψ, this proves Σ_{4}^{P} -hardness. The result follows.

We close this part of the appendix with a remark on the complexity of first-order default abduction problems under domain closure and unique names assumption (cf. Section 6). Most of the hardness results from above are proved by polynomial-time transformations of evaluating particular quantified Boolean formulas that are hard for Σ_{k}^{P} resp. Π_{k}^{P}. Note that such formulas can be seen as second-order propositional formulas, since the quantifiers are on propositional atoms. It is shown in [29] that evaluating second-order formulas of predicate logic over a fixed finite relational structure (i.e., a first-order structure with finite domain for a language without functions and constants) has precisely exponentially higher complexity, and yields problems hard for the exponential analogues Σ_{k}^{E} and Π_{k}^{E} of Σ_{k}^{P} and Π_{k}^{P}, respectively.

Utilizing these results, the hardness proofs from above can be easily generalized to corresponding hardness proofs for the first-order case. In fact, a suitable replacement of QBFs by corresponding second-order predicate formulas is feasible. We show this on the example of the transformation in the proof of Theorem 4.9. Instead of the QBF Φ = ∃X∀Y ∃Z F, we have a second-order predicate formula

Ψ = ∃p_{1,1} ⋯ ∃p_{1,n_{1}}∀p_{2,1} ⋯ ∀p_{2,n_{2}}∃p_{3,1} ⋯ ∃p_{3,n_{3}}ϕ

where the p_{i,j} are predicate variables and ϕ is a closed first-order formula (in which no function and constant symbols occur).

Evaluating Ψ on a fixed finite relational structure A is Σ_{3}^{E}-hard [29]. A can be represented in default logic by the fixed first-order theory

W_{A} = {r(t) | A ⊧ r(t), r(t) is a ground atom} ∪ {¬r(t) | A |̸= r(t), r(t) is a ground atom}

(i.e., W_{A} yields the closed world assumption applied to the relations in A). Define now defaults

D = \{ \frac{: ¬p_{i,j}(x)}{¬p_{i,j}(x)}, \frac{: p_{i,j}(x)}{p_{i,j}(x)} | i = 1, 2, j = 1, …, n_{i}\} ∪ \{ \frac{: ϕ}{ϕ}\}

(here the x = x_{1}, …, x_{n} is assumed to match the arity of p_{i,j}) and a first-order DAP

P = ⟨{ p_{1,j}, ¬p_{1,j} | j = 1, …, n_{1} } , {f} , W_{A} ∪ { f ↔ ϕ } , D⟩,

where f is a new propositional atom. It holds that P has a skeptical explanation iff A ⊧ Ψ. This proves Σ_{3}^{E}-hardness of Consistency for skeptical abduction in the first-order case.

Similar generalizations are straightforward in the other proofs.

B Appendix: Proofs for tractable cases

Lemma 5.1 Let ⟨W, D⟩ be a Literal-Horn default theory, and let ℓ_{1}, …, ℓ_{m} be literals. Then, deciding ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is possible in O(m · n) time, where n is the length of the input.

Proof. If W is not consistent (which holds iff it contains a pair of opposite literals) then ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m}; if ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is not satisfiable, then ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} iff W is not consistent. Both consistency of W and satisfiability of ℓ_{1} ∧ ⋯ ∧ ℓ_{m} can be checked in linear time; in what follows, we thus assume that W is consistent and that ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is satisfiable, i.e., ℓ_{1}, …, ℓ_{m} does not contain a pair of opposite literals. Define

H = W ∪ {α ⊃ ℓ | (α : ℓ/ℓ) ∈ D and ∼ℓ ∉ W and
[ℓ ∈ {ℓ_{1}, …, ℓ_{m}} or (ℓ is positive and ℓ ∉ {∼ℓ_{1}, …, ∼ℓ_{m}}) ]} .

Note the important fact that H does not contain simultaneously clauses with opposite literal in the head, i.e., clauses β ⊃ ℓ and γ ⊃ ∼ℓ (where β and/or γ may be empty). Claim: ⟨W, D⟩ has an extension containing ℓ_{1}, …, ℓ_{m} iff H ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m}.

Note that for n = 1, i.e., a single literal ℓ_{1}, H is the Horn theory of [35, Lemma 6.4], which states the claimed property for a single literal.

H can be constructed in linear time from ⟨W, D⟩; notice that H is Horn. It is well-known that for a Horn theory T and a literal ℓ, the test T ⊢ ℓ can be decided in time linear in the length of T, e.g. by positive unit resolution, cf. [40]. Consequently, deciding H ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is possible in time linear in the length of H times m, and hence in time O(m · n). (In fact, the set of all positive literal ℓ such that T ⊢ ℓ (i.e., the least model) can computed in time linear in the length of T [40], and thus the bound could be sharpened to O((m^{−} + 1)n) where m^{−} is the number of negative literals ℓ_{i}.) Therefore, the lemma is an immediate consequence of this claim.

Prior to the proof of the claim, define subsets H_{0}, H_{1}, …, H_{i}, … of H as follows:

H_{0} = W
H_{1} = H_{0} ∪ { α ⊃ ℓ ∈ H\H_{0} | H_{0} ⊢ α }
⋮
H_{i+1} = H_{i} ∪ { α ⊃ ℓ ∈ H\H_{i} | H_{i} ⊢ α }
⋮

Note that the sequence ⟨H_{i}⟩, i ≥ 0, converges to ⋃_{i=0}^{∞} H_{i}; this set relates to H as follows. Since H is a Horn theory, it has a least model M; the following characterization of M is not difficult to establish:

(0) M = { x | α ⊃ x ∈ ⋃_{i≥0}^{∞} H_{i} } ,

i.e., the least model of H is given by the atoms x in the heads of the clauses with positive head (resp. positive facts) in H_{0}, H_{1} … Indeed, let N = { x | α ⊃ x ∈ ⋃_{i≥0} H_{i} }. Then, one can check that N is a model of H; moreover, by induction on i, one can show that M must contain all positive heads of the clauses in H_{0} ∪ ⋯ ∪ H_{i}, and hence N is contained in M.

We now prove the claim.

“⇐”: Assume that H ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m}. Define the set E by

E = T h( W ∪ M ∪ {¬x | (α : ¬x/¬x) ∈ D, M ⊧ α, M |̸= x }).

Notice that E is consistent. We claim that E is an extension of ⟨W, D⟩ such that ℓ_{i} ∈ E, for every i = 1, … n, which proves the If-direction. To prove this claim, we first verify that ℓ_{i} ∈ E, for every i = 1, …, n. If ℓ_{i} is a positive literal, then ℓ_{i} ∈ M and hence, by definition of E, clearly ℓ_{i} ∈ E; otherwise, if ℓ_{i} is a negative literal ¬x, then, since H ⊢ ℓ_{i}, there must exist a clause α ⊃ ¬x in H such that M ⊧ α (for otherwise, a model of H in which x is true exists). Thus, (α : ¬x / ¬x) ∈ D, M ⊧ α and M |̸= x all hold; by definition, ¬x ∈ E.

It remains to show that E is an extension, i.e., E = ⋃_{i=0}^{∞} E_{i}, where the sets E_{i} are those in the definition of extension. We obtain

E_{0} = W = W ∪ {x | x ∈ H_{0}}
E_{1} = T h(E_{0}) ∪ {ℓ | (α : ℓ / ℓ) ∈ D, E_{0} ⊢ α, ¬ℓ ∉ E }
= T h(E_{0}) ∪ \{ ¬x | \frac{α : ¬x}{¬x} ∈ D, E_{0} ⊢ α, x ∉ E \} ∪ \{ x | α ⊃ x ∈ H_{1} \}
⋮
E_{i+1} = T h(E_{i}) ∪ \{ ¬x | \frac{α : ¬x}{¬x} ∈ D, E_{i} ⊢ α, x ∉ E \} ∪ \{ x | α ⊃ x ∈ H_{i+1} \}
⋮

Indeed, by induction on i, it is straightforward that the set of positive literals in E_{i}, P_{i}, is { x | α ⊃ x ∈ H_{i} }.

For i = 0, this is obvious. Consider thus i′ = i + 1, and first α ⊃ x ∈ H_{i+1}. If α ⊃ x ∈ H_{i}, then by the induction hypothesis x ∈ E_{i}, and hence x ∈ E_{i+1}; otherwise, a default (α : x/x) ∈ D exists, by the induction hypothesis E_{i} ⊢ α, and since x ∈ M, ¬x ∉ E; consequently, x ∈ E_{i+1}. It follows that: (+) {x | α ⊃ x ∈ H_{i+1}} ⊆ P_{i+1}.

On the other hand, consider a positive atom x from E_{i+1}. If x ∈ T h(E_{i}), then from the induction hypothesis, it follows that x ∈ {y | α ⊃ y ∈ H_{i}}. Otherwise, there is a default (α : x/x) ∈ D, s.t. E_{i} ⊢ α and ¬x ∉ E. By the induction hypothesis, it follows that H_{i} ⊢ α, and we have ¬x ∉ W (since W ⊆ E). Since x ∈ E (as E_{i+1}) and, as shown above, ℓ_{i} ∈ E for every i = 1, …, n, it follows that either x ∈ {ℓ_{1}, …, ℓ_{m}} or x ∉ {∼ℓ_{1}, …, ∼ℓ_{m}}. Consequently, α ⊃ x ∈ H_{i+1}. It follows that (++) P_{i+1} ⊆ {x | α ⊃ x ∈ H_{i+1}}. Conditions (+) and (++) imply P_{i+1} = {x | α ⊃ x ∈ H_{i+1}}, i.e., the statement of the induction. This concludes the induction.

It follows that

⋃_{i=0}^{∞} E_{i} = T h ( W ∪ \{ x | α ⊃ x ∈ ⋃_{i=0}^{∞} H_{i} \} ∪ \{¬x | \frac{α : ¬x}{¬x} ∈ D, ⋃_{i=0}^{∞} E_{i} ⊢ α, x ∉ E \}) .

For any conjunction α of positive literals, it follows from (0) that

(1) ⋃_{i=0}^{∞} E_{i} ⊢ α ⇔ {x | α ⊃ x ∈ ⋃_{i=0}^{∞} H_{i}} ⊢ α ⇔ M ⊧ α.

Furthermore, from the definition of E, it is easily verified that

(2) x ∉ E ⇔ M |̸= x.

By (0), (1), and (2), we therefore obtain

⋃_{i=0}^{∞} E_{i} = T h( W ∪ \underbrace{\{ x | α ⊃ x ∈ ⋃_{i=0}^{∞} H_{i}\}}_{=M} ∪ \{¬x | \frac{α:¬x}{¬x} ∈ D, M ⊧ α, M |̸= x\})

= E.

Thus, E is an extension of ⟨W, D⟩. This proves the If-direction.

“⇒”: Assume that ⟨W, D⟩ has an extension E containing ℓ_{1}, …, ℓ_{m}. We have to show that H ⊢ ℓ_{i}, for every i = 1, …, n. Without loss of generality, we assume that E satisfies the following condition:

(∗) If \frac{α: x}{x} ∈ D such that E ⊢ α, and x ∉ \{∼ℓ_{1}, …, ∼ℓ_{m}\}, then ¬x ∉ E\W.

Indeed, assume that (α : x/x) is a default in D that violates (*). Since ⟨W, D⟩ is Literal-Horn, it is not hard to see that ⟨W, D⟩ has an extension E′ ⊇ T h(E\ {¬x} ∪ {x}) that contains ℓ_{1}, …, ℓ_{m} (take any extension of ⟨E\ {¬x} ∪ {x} , D⟩.) Using e.g. a (well)-ordering on the defaults D, one can single out a particular such extension. This gives rise to a monotonic operator, which takes E to an extension E′ with a larger part of positive atoms; the least fixpoint of this operator is an extension that satisfies (∗). This justifies our assumption.

Let M_{0} be the set of positive literals in E. We claim that M_{0} is the least model of H (i.e., M_{0} = M = { x | α ⊃ x ∈ ⋃_{i=0}^{∞} H_{i}}).

We proof this claim showing by induction on i ≥ 0 that

M_{0} ∩ T h(E_{i}) = {x | α ⊃ x ∈ H_{i}} ,

i.e., the positive literals in E_{i} are the positive heads of clauses in H_{i}. Since M = ⋃_{i=0}^{∞}{ x | α ⊃ x ∈ H_{i} }, the claim is an immediate consequence thereof. (Basis) For i = 0, we have E_{0} = W and H_{0} = W. Thus, the statement is clearly true. (Induction) For i′ = i + 1, we have

M_{0} ∩ T h(E_{i+1}) = M_{0} ∩ T h( T h(E_{i}) ∪ {ℓ | (α : ℓ/ℓ) ∈ D, E_{i} ⊢ α, ¬ℓ ∉ E})
= \{x | α ⊃ x ∈ H_{i}\} ∪ \underbrace{\{x | \frac{α : ¬x}{¬x} ∈ D, E_{i} ⊢ α, ¬x ∉ E\}}_{=_{def} B}

The induction hypothesis is applied to obtain the left expression on the second line.

Consider x ∈ B. Then, ¬x ∉ W and either x ∈ {ℓ_{1}, …, ℓ_{m}} or x ∉ {∼ℓ_{1}, …, ∼ℓ_{m}} (as ℓ_{i} ∈ E, x ∈ E, and E must be consistent). Since E_{i} ⊢ α, it follows from the induction hypothesis that H_{i} ⊢ α. Therefore, α ⊃ x ∈ H_{i+1}, which implies: (**) x ∈ { y | α ⊃ y ∈ H_{i+1} }.

On the other hand, consider any α ⊃ y ∈ H_{i+1}. If y ∈ {x | β ⊃ x ∈ H_{i}}, it is clear from the equation above that y ∈ M_{0} ∩ T h(E_{i+1}). Otherwise, if α ⊃ x ∈ H_{i+1}, then H_{i} ⊢ α, which by the induction hypothesis implies that E_{i} ⊢ α. Moreover, either (a) y ∈ {ℓ_{1}, …, ℓ_{m}} or (b) y ∉ {∼ℓ_{1}, …, ∼ℓ_{m}}. In case (a), y ∈ E and ¬y ∉ E, as E ⊢ ℓ_{1} ∧ ⋯ ∧ ℓ_{m}; thus y ∈ B. In case (b) we obtain from the assumption (*) on E that ¬y ∉ E\W; moreover, by the definition of H, ¬y ∉ W. Therefore, ¬y ∉ E, which implies y ∈ B. Since y ∈ B holds in both cases (a) and (b), it follows that (***) y ∈ M_{0} ∩ T h(E_{i+1}).

Now (**) and (***) imply

M_{0} ∩ T h(E_{i+1}) = { x | α ⊃ x ∈ H_{i+1}};

this proves the induction step and the claim M_{0} = M.

Eventually, we verify that H ⊢ ℓ_{i} for every i = 1, …, n. If ℓ_{i} is positive, then ℓ_{i} ∈ M_{0} = M; therefore, H ⊢ ℓ_{i}. Otherwise, ℓ_{i} is a negative literal ¬x. If ℓ_{i} ∈ W, then ℓ_{i} ∈ H and therefore H ⊢ ℓ_{i}; if ℓ_{i} ∉ W, then some \frac{α: ℓ_{i}}{ℓ_{i}} ∈ D exists such that E ⊢ α. Since ℓ_{i} ∈ E, we have ∼ ℓ_{i} ∉ W; hence, it follows α ⊃ ℓ_{i} ∈ H. Moreover, since α is a conjunction of positive literals, E ⊢ α and M_{0} = M implies M ⊧ α; consequently, H ⊢ α. Since α ⊃ ℓ_{i} ∈ H, it follows H ⊢ ℓ_{i}.

This concludes the proof of the Only-If direction and the proof of the lemma.

Proposition B.1 Given a Krom-pf-normal default theory ⟨W, D⟩ and literals ℓ_{1}, …, ℓ_{m}, deciding whether ⟨W, D⟩ ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} is NP-complete.

Proof. Concerning membership, a consistent extension E such that ℓ_{1}, …, ℓ_{m} ∈ E can be guessed and verified in polynomial time. Indeed, since ⟨W, D⟩ is prerequisite-free and normal, a guess D′ ⊆ D for GD(E, T) is proper if C = W ∪ concl(D′) is consistent, C ⊢ ℓ_{i}, for all i = 1, …, m, and no \frac{:β}{β} ∈ D\D′ exists such that C ∪ \{ β \} is consistent. Since W is Krom and all formulas in defaults are Krom, each of these tests can be done in polynomial time. (Indeed, satisfiability of a Krom theory can be decided in linear time [25, 3]). This proves membership in NP.

To show hardness, we reduce the classical satisfiability problem (SAT) to this problem as follows. For a set of propositional clauses C = {C_{1}, …, C_{m}} where C_{i} = ℓ_{i_{1}} ∨ ⋯ ∨ ℓ_{i_{n_{i}}}, define

D = \{ \frac{: ℓ_{i_{j}} ∧ c_{i}}{ℓ_{i_{j}} ∧ c_{i}} | i = 1, …, m, j = 1, …, n_{i}\} ∪ \{ \frac{: x}{x}, \frac{: ¬x}{¬x} | x occurs in C \} ,

where the c_{i}, i = 1, …, m, are new atoms. It is easy to see that ⟨∅, D⟩ ⊢_{c} c_{1} ∧ ⋯ ∧ c_{m} iff C is satisfiable. Since D is efficiently obtained from C, this proves NP-hardness.

From the proof of this proposition, the following result can be easily established.

Corollary B.2 Deciding if a given PDAP P = ⟨H, M, W, D⟩ has a credulous explanation is NPhard, even if all defaults are prerequisite-free, W = H = ∅, and M is a set of atoms.

Proposition B.3 Given a Krom-pf-normal default theory ⟨W, D⟩ and a literal ℓ, deciding whether ⟨W, D⟩ ⊢_{s} ℓ is co-NP-complete.

Proof. Membership in co-NP follows from the fact that a guess for an extension E such that ℓ ∉ E can be verified in polynomial time.

To show co-NP-hardness, we reduce the unsatisfiability problem (UNSAT) to this problem: Decide whether a given set of propositional clauses C = {C_{1}, …, C_{m}}, C_{i} = ℓ_{i_{1}} ∨ ⋯ ∨ ℓ_{i_{n_{i}}}, is not satisfiable. Define a set of defaults D by

D = \{ \frac{: c ∧ ∼ℓ_{i_{1}} ∧ ⋯ ∧ ∼ℓ_{i_{n_{i}}}}{c ∧ ∼ℓ_{i_{1}} ∧ ⋯ ∧ ∼ℓ_{i_{n_{i}}}} | i = 1, …, m \} ∪ \{ \frac{: x}{x}, \frac{: ¬x}{¬x} | x occurs in C \} .

where c is a new atom. It holds that ⟨∅, D⟩ ⊢_{s} c iff C is unsatisfiable. Since D can be constructed efficiently, this proves the result.

Proposition B.4 Relevance based on minimal credulous explanations for PDAPs P = ⟨H, M, W, D⟩ where ⟨W, D⟩ is Literal-Horn is NP-complete.

Proof. Membership. A guess for a minimal credulous explanation E such that h ∈ E can be verified in polynomial time, by testing that E is an credulous extension and that ⟨E\ {h′} , M, W, D⟩ has no credulous explanation, for every h′ ∈ E; both tests are polynomial, as follows from Lemma 5.1 and Theorem 5.3.

Hardness. The hardness part is a simple reduction of abductive reasoning from classical theories (cf. [22]): Given a definite Horn PAP ⟨V, H, M, T ⟩, decide if a certain hypothesis h is relevant in a minimal explanation. Here T is a set of definite Horn clauses a_{1} ∧ ⋯ ∧ a_{n} ⊃ a_{0} on a set of variables V, H ⊆ V, M ⊆ V, and the underlying inference is classical consequence ⊢. The constructed PDAP is P′ = ⟨H, M, W, D⟩, where W = {a ∈ V | a ∈ T } and D = \{ \frac{a_{1}∧···a_{k}:b}{b} | a_{1} ∧ ⋯ ∧ a_{k} ⊃ b ∈ T \}. Observe that the credulous explanations for P′ coincide with the skeptical ones, since ⟨W ∪ E, D⟩ has a unique extension for every E ⊆ H. It is easy to see that the credulous explanations for P′ coincide with the explanations for P. Therefore, h is relevant in a minimal credulous explanation for P′ iff h is relevant in a minimal explanation for P. Since deciding the latter is NP-hard [22], Relevance for Literal-Horn PDAPs is also NP-hard.

Lemma 5.5 Let S be a (propositional) Krom theory and ℓ a literal, and let L = {ℓ_{1}, …, ℓ_{k}} be a set of literals such that (i) S ∪ L is consistent, (ii) S ∪ L ⊢ ℓ and S ⊬ ℓ. Then, S ∪ {ℓ_{i}} ⊢ ℓ for some ℓ_{i} ∈ L.

Proof. This is obvious if ℓ ∈ L. Assume thus that ℓ ∉ L. Consider any resolution proof for ℓ from S ∪ L. (Such a proof must exist). In the last step, we have that {ℓ} is the resolvent of clauses C_{1} and C_{2} that have a resolution proof from S ∪ L. It is easy to see that a clause C of size 2 has a resolution proof from a consistent Krom theory T iff it has a resolution proof from the set T′ ⊆ T of all clauses in T of size 2. Hence, we conclude that without loss of generality C_{2} is a literal, i.e., C_{1} = {ℓ, ∼ℓ_{0}} and C_{2} = {ℓ_{0}} (for otherwise, S ⊢ ℓ would hold). Since S ∪ L is Krom, C_{1} has a resolution proof from S, and therefore S ∪ {ℓ_{0}} ⊢ ℓ. By induction on the length r of a shortest resolution proof for ℓ from S ∪ L, we conclude that ℓ_{0} ∈ L. Indeed, if r = 0, then ℓ_{0} ∈ L; if r > 0, then ℓ_{0} ∉ L; since ℓ_{0} has a shorter resolution proof than ℓ, it follows from the induction hypothesis that S ∪ {ℓ′} ⊢ ℓ_{0} where ℓ′ ∈ L; hence, S ∪ {ℓ′} ⊢ ℓ, which concludes the induction and proves the lemma.

Proposition 5.6 Let T = ⟨W, D⟩ be a Krom-pf-normal default theory and let L = {ℓ_{1}, …, ℓ_{m}} be a set of literals. Let L1 = {ℓ_{i} ∈ L | W ⊬ ℓ_{i}}. Then, T ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} iff (a) L1 is empty, or (b) there exists a subset D1 ⊆ D such that

(b.1) |D1| ≤ |L1|,

(b.2) W ∪ lit(D1) is consistent, and

(b.3) W ∪ lit(D1) ⊢ ℓ, for each ℓ ∈ L1.

Proof. “⇒”: If T ⊢_{c} ℓ, then there exists an extension E of T such that L ⊆ E. By the characterization of E in terms of its generating defaults (see Section 2), E = T h(W ∪ lit(GD(E, T))). Consider two cases. (i). E is not consistent. Then, by the well-known properties of default extensions [52], W is not consistent. Thus, from the definition, we have L1 = ∅; hence, (a) holds. (ii). E is consistent. Then W ∪ lit(GD(E, T)) is consistent. From Lemma 5.5, we infer that for each ℓ ∈ L1 there exists some μ ∈ lit(GD(E, T)) such that W ∪ {μ} ⊢ ℓ. Consequently, there exists a subset D1 ⊆ GD(E, T), and hence D1 ⊆ D, such that |D1| ≤ |L1|, W ∪ lit(D1) is consistent and W ∪ lit(D1) ⊢ ℓ, for each ℓ ∈ L1. Hence, (b) holds. This proves the Only-If direction.

“⇐”: Assume that (a) holds, i.e., L1 = ∅. This means W ⊢ ℓ for each ℓ ∈ L. Since W ⊆ E for every extension E of T and E is deductively closed, it follows that L ⊆ E for every extension of T. As T is normal, an extension exists, and hence T ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m}.

Assume now that (b) does hold, i.e. for some D1 ⊆ D we have |D1| ≤ |L1|, W ∪ lit(D1) is consistent, and W ∪ lit(D1) ⊢ ℓ for every ℓ ∈ L1. Since T is prerequisite-free and normal, it follows from semi-monotonicity that T has a consistent extension E such that W ∪ lit(D1) ⊆ E. Since E is deductively closed, L ⊆ E; it follows T ⊢_{c} ℓ. This proves the result.

Theorem 5.7 Let T = ⟨W, D⟩ be a Krom-pf-normal default theory, and let L = {ℓ_{1}, …, ℓ_{m}} be a set of literals. Then, T ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{m} can be decided using Krom-PFN-Cred-Inf in O(|D|^{m} · m · n) time, where n is the length of the input.

Proof. Correctness of the algorithm follows from Proposition 5.6. Concerning the complexity, satisfiability of a Krom theory can be decided in linear time [25, 3]. Consequently, also inference of a literal from a Krom theory can be decided in linear time. Therefore, L1 can be computed in O(m · n) time. The for-loop checks at most |D|^{|L1|} ≤ |D|^{m} sets D1; for each D1, computing S is possible in O(n) time, and the tests S ⊬ ⊥, S ⊢ ℓ_{i} take O(m · n) time. Hence, the overall running time is O(m · n + |D|^{m}(n + m · n)), which is O(|D|^{m} · m · n).

Theorem 5.8 Let P = ⟨H, M, W, D⟩ be a PDAP based on credulous explanations such that M = {ℓ_{1}, …, ℓ_{k}} is small and ⟨W, D⟩ is Krom-pf-normal. Then, Consistency, Relevance, and Necessity can be solved in O(|D|^{b} · n) time, where n is the length of P.

Proof. Construct a Krom-pf-normal default theory T 2 = ⟨W 2, D2⟩, given by

W 2 = W ∪ \{c_{h} ⊃ h | h ∈ H\} , D2 = D ∪ \{ \frac{: c_{h}}{c_{h}} , \frac{: ¬c_{h}}{¬c_{h}} | h ∈ H\}

where each c_{h} is a new propositional atom. It is not hard to see that P has an explanation iff W 2 is consistent and T 2 ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{k}. Clearly, W 2, D2, and T 2 can be constructed in O(n) time. Consistency of W 2 can be checked in linear time [25, 3] and by Lemma 5.2, T 2 ⊢_{c} ℓ_{1} ∧ ⋯ ∧ ℓ_{k} can be decided in O(|D2|^{b} · n′) time, where n′ is the length of T 2 (which is O(n) ). Hence, Consistency can be decided in O(|D|^{b} · n) time. By Corollary 4.3, Relevance and Necessity can be easily reduced to Consistency resp. its complement in O(n) time; hence, these problems are also solvable in O(|D|^{b} · n) time.

Proposition 5.9 Let E be any minimal credulous explanation for a PDAP P = ⟨H, M, W, D⟩ where ⟨W, D⟩ is Krom-pf-normal and M is finite. Then, |E| ≤ |M|.

Proof. Let E be any credulous explanation. Then, the default theory T 1 = ⟨W ∪ E, D⟩ has a consistent extension A such that M ⊆ E. By the characterization of extensions, we have A = T h(W ∪E∪L), where L = lit(GD(A, T 1)). Hence, W ∪E∪L is consistent and W ∪E∪L ⊢ ℓ, for each ℓ ∈ M. From Lemma 5.5, it follows that for each ℓ ∈ M such that W ⊬ ℓ, there exists a μ_{ℓ} ∈ E ∪ L such that W ∪ {μ_{ℓ}} ⊢ ℓ. Fix any such μ_{ℓ} for each ℓ, and let E0 ⊆ E be the set E_{0} = { μ_{ℓ} | ℓ ∈ M } ∩ E; notice that |E0| ≤ |M|. Then, E0 is a credulous explanation for P. Indeed, the default theory T 2 = ⟨W ∪ E0, D⟩ has a consistent extension which contains M: Since the set W ∪ E0 ∪ lit(GD(A, T 1)) is consistent and all defaults in D are prerequisite-free and normal, T 2 has a consistent extension E3 containing W ∪ E_{0} ∪ lit(GD(A, T 1)). Moreover, since W ∪ E0 ∪ lit(GD(A, T 1)) ⊢ ℓ for each ℓ ∈ M, we have M ⊆ E3. Thus, E0 is a credulous explanation of P.

Since E was arbitrary, it follows that for each explanation E for P, there exists an explanation E0 ⊆ E such that |E0| ≤ |M|. In particular, if E is a minimal explanation, then E = E0, and hence |E| ≤ |M|. This proves the result.

Theorem 5.10 Given a PDAP P = ⟨H, M, W, D⟩ where ⟨W, D⟩ is Krom-pf-normal and M is small, all minimal credulous explanations for P can be computed in time O(|H|^{b} · |D|^{b} · n), where n is the length of P.

Proof. Consider algorithm All-KPFN-Min-Cred-Exp. In total, at most |H|^{b} subsets E ⊆ H are considered. For each set E, the test W ∪ E ⊬ ⊥ takes O(n) time (W ∪ E is Krom); the tests E′ ∉ Min Expl can be done in O(2^{b} · log |Min Expl|) time, if Min Expl is stored in a standard search data structure (e.g., an AVL-tree) on which E0 ∉ Min Expl is checked for every subset E0 ⊂ E. The test Krom-PFN-Cred-Inf(W ∪ E, D, ϕ) takes O(|D|^{b} · n). Since |Min Expl| is bounded by |H|^{b}, this amounts to O(|H|^{b} ·(2^{b} log |H|^{b} +|D|^{b} ·n)) time. Building and maintaining the data structure for Min Expl takes in total O(|H|^{b} · log |H|^{b}) time. Since log |H|^{b} = b log |H| is O(n), it follows that total running time of the algorithm is O(|H|^{b} · |D|^{b} · n).

Proposition B.5 Given a first-order Krom-pf-normal default theory T = ⟨W, D⟩ and a ground literal ℓ, deciding whether T ⊢_{c} ℓ is NP-hard, even if all formulas in W are (universally quantified) atoms and D contains a single default.

Proof. Transform the classical satisfiability problem (SAT) into this problem as follows. Let C = {C_{1}, …, C_{m}} be a propositional clause set on atoms a_{1}, …, a_{n}, where without loss of generality no atom occurs positively and negatively in the same clause, and neither all clauses are positive or negative. For each clause C_{i} in C, put the formula ϕ_{i} = ∀x_{1} ⋯ ∀x_{n}p(t_{1}, …, t_{n}) in W, where

t_{j} = \{ \begin{matrix}0, & if a_{j} ∈ C_{j}; \\ 1, & if ¬a_{j} ∈ C_{j}; \\ x_{j}, & otherwise. \end{matrix}

In D, put the single default d = \frac{: ¬p(x_{1},...,x_{n})∧s}{¬p(x_{1},...,x_{n})∧s}, where s is a propositional atom. Intuitively, each ground atom p(t_{1}, …, t_{n}), where t_{i} ∈ {0, 1}, corresponds to a truth value assignment to the propositional atoms a_{1}, …, a_{n} such that a_{i} is true if t_{i} = 1 and a_{i} = 0 if t_{i} = 0. Each formula ϕ_{i} describes all truth assignments that do not satisfy clause C_{i}; the default d is applicable precisely if there is a truth assignment that is compatible with each clause C_{i}, i.e., if it satisfies C. Therefore, C is satisfiable if and only if ⟨W, D⟩ ⊢_{c} s. This proves NP-hardness.

References

[1] A. Aho and J. Ullman. Universality of Data Retrieval Languages. In Proc. ACM Symposium on Principles of Programming Languages, pp. 110–117, 1979.

[2] L. Aiello and D. Nardi. Perspectives in Knowledge Representation. Applied Artificial Intelligence, 5(1):29–44, 1991.

[3] B. Aspvall, M. Plass, and R. Tarjan. A linear time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, 8:121–123, 1979.

[4] C. Baral and V. Subrahmanian. Dualities Between Alternative Semantics for Logic Programming and Nonmonotonic Reasoning. Journal of Automated Reasoning, 10:299–340, 1991.

[5] G. Brewka. Nonmonotonic Reasoning: Logical Foundations of Commonsense. Number 12 in Cambridge Tracts in Theoretical Computer Science. Cambridge Univ. Press, 1991.

[6] T. Bylander. The Monotonic Abduction Problem: A Functional Characterization on the Edge of Tractability. In Proc. KR-91, pp. 70–77, 1991.

[7] T. Bylander, D. Allemang, M. Tanner, and J. Josephson. The computational complexity of abduction. Artificial Intelligence, 49:25–60, 1991.

[8] M. Cadoli, T. Eiter, and G. Gottlob. Default Logic as a Query Language. In Proc. KR-94, pp. 99-108, 1994. Full paper to appear in IEEE Transactions on Knowledge and Data Engineering.

[9] M. Cadoli and M. Schaerf. A Survey of Complexity Results for Non-monotonic Logics. Journal of Logic Programming, 17:127–160, 1993.

[10] M. Cadoli and M. Schaerf. Tractable Reasoning via Approximation. Artificial Intelligence, 74(2):249– 310, 1995.

[11] A. Chandra and D. Harel. Structure and Complexity of Relational Queries. Journal of Computer and System Sciences, 25:99–128, 1982.

[12] E. Charniak and P. McDermott. Introduction to Artificial Intelligence. Addison Wesley, Menlo Park, Ca, 1985.

[13] P. Cholewiński, W. Marek, A. Mikitiuk, and M. Truszczyński. Experimenting with Nonmonotonic Reasoning. In Proc. ICLP-95, Shonan Village Center, Japan, June 1995. MIT-Press.

[14] A. Condon. Approximate Solutions to Problems in PSPACE. SIGACT News, 26(2):4–13, June 1995.

[15] L. Console, D. Theseider Dupré, and P. Torasso. A Theory of Diagnosis for Incomplete Causal Models. In Proceedings IJCAI-89, pages 1311–1317, 1989.

[16] L. Console, D. Theseider Dupré, and P. Torasso. On the Relationship Between Abduction and Deduction. Journal of Logic and Computation, 1(5):661–690, 1991.

[17] P. Dagum and M. Luby. Approximating Probabilistic Inference in Bayesian Belief Networks is NPhard. Artificial Intelligence, 60(1):141–153, 1993.

[18] F. Donini, D. Nardi, F. Pirri, and M. Schaerf. Nonmonotonic Reasoning. Artificial Intelligence Reviews, 4:163–210.

[19] F. Donini, D. Nardi, and R. Rosati. Ground Nonmonotonic Modal Logics for Knowledge Representation. In Proc. World Congress for AI (WOCFAI-95), 1995.

[20] T. Eiter and G. Gottlob. On the Complexity of Propositional Knowledge Base Revision, Updates, and Counterfactuals. Artificial Intelligence, 57(2–3):227–270, 1992.

[21] T. Eiter and G. Gottlob. Reasoning with Parsimonious and Moderately Grounded Expansions. Fundamenta Informaticae, 17(1/2):31–53, 1992.

[22] T. Eiter and G. Gottlob. The Complexity of Logic-Based Abduction. Journal of the ACM, 42(1):3–42, January 1995.

[23] T. Eiter, G. Gottlob, and N. Leone. Complexity Results for Abductive Logic Programming. In Proc. LPNMR ’95, W. Marek and A. Nerode and M. Truszczyński (eds), LNCS/LNAI 982, pp. 1–14, 1995.

[24] K. Eshghi. Abductive Planning with Event Calculus. In Proc. 5th International Conference and Symposium on Logic Programming, pp. 562–579. MIT Press, 1988.

[25] S. Even, A. Itai, and A. Shamir. On the Complexity of Timetable and Multicommodity Flow Problems. SIAM J. Comp., 5:691–703, 1976.

[26] M. Gelfond, H. Przymusinska, V. Lifschitz, and M. Truszczyński. Disjunctive Defaults. In Proc. KR-91, pp. 230–237, 1991.

[27] G. Gottlob. Complexity Results for Nonmonotonic Logics. Journal of Logic and Computation, 2(3):397–425, June 1992.

[28] G. Gottlob. The Complexity of Propositional Default Reasoning Under the Stationary Fixed Point Semantics. Information and Computation, 121(1):81–92, 1995.

[29] G. Gottlob, N. Leone, and H. Veith. Second-Order Logic and the Weak Exponential Hierarchies. In Proc. of the Conference on Mathematical Foundations of Computer Science (MFCS-95), LNCS 969, pp. 66–81, 1995. Full paper available as CD/TR 95/80, CD-Lab for Expert Systems, TU Wien.

[30] J. R. Hobbs, M. E. Stickel, P. Martin, and D. Edwards. Interpretation as Abduction. In Proc. 26th Annual Meeting of the Assoc. for Computational Linguistics, pp. 95–103, Buffalo (NY), 1988.

[31] D. S. Johnson. A Catalog of Complexity Classes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A, chapter 2. Elsevier Science Publishers B.V. (North-Holland), 1990.

[32] J. Josephson, B. Chandrasekaran, J. J. W. Smith, and M. Tanner. A Mechanism for Forming Composite Explanatory Hypotheses. IEEE Transactions on Systems, Man, and Cybernetics, SMC-17:445– 454, 1987.

[33] A. Kakas, R. Kowalski, and F. Toni. Abductive Logic Programming. Journal of Logic and Computation, 1993.

[34] A. Kakas and P. Mancarella. Database Updates Through Abduction. In Proc. VLDB-90, pp. 650–661, 1990.

[35] H. Kautz and B. Selman. Hard Problems for Simple Default Logics. Artificial Intelligence, 49:243–279, 1991.

[36] K. Konolige. On the Relationship between Default and Autoepistemic Logic. Artificial Intelligence, 35:343–382, 1988. + Errata, same journal, 41:115, 1989/90.

[37] K. Konolige. Abduction versus closure in causal theories. Artificial Intelligence, 53:255–272, 1992.

[38] W. Marek and M. Truszczyński. Nonmonotonic Logics. Springer, 1993.

[39] A. Mikitiuk and M. Truszczyński. Rational Default Logic and Disjunctive Logic Programming. In L.-M. Pereira and A. Nerode, editors, Proc. LPNMR ’93, pp. 115–131, 1993. MIT Press.

[40] M. Minoux. LTUR: a simplified linear time unit resolution for Horn formulae and computer implementation. Information Processing Letters, 29:1–12, 1988.

[41] B. Nebel. Artificial Intelligence: A Computational Perspective. To appear in “Logic and Computation in AI”, G. Brewka ed.

[42] H. T. Ng and R. J. Mooney. An efficient first-order Horn clause abduction system based on the ATMS. In Proc. AAAI-91, pp. 494–499, Anaheim, August 1991.

[43] Y. Peng and J. Reggia. Abductive Inference Models for Diagnostic Problem Solving. Springer, 1990.

[44] D. Poole. A Logical Framework for Default Reasoning. Artificial Intelligence, 36:27–47, 1988.

[45] D. Poole. Explanation and Prediction: An Architecture for Default and Abductive Reasoning. Computational Intelligence, 5(1):97–110, 1989.

[46] D. Poole. Normality and Faults in Logic Based Diagnosis. In Proc. IJCAI-89, pp. 1304–1310, 1989.

[47] D. Poole. Logic Programming, Abduction and Probability. New Generation Computing, 11:377–400, 1993.

[48] D. Poole. Probabilistic Horn Abduction and Bayesian Networks. Artificial Intelligence, 64(1):81–130, 1993.

[49] H. Przymusinska and T. Przymusinski. Stationary default extensions. Fundamenta Informaticae, 21(1/2):67–87, 1994.

[50] A. Rajasekar. Theories of Trans-Epistemic Defaults. Technical report, University of Kentucky, Lexington, KY, 1994.

[51] A. Rajasekar and M. Truszczyński. Complexity of Trans-Epistemic Defaults. Manuscript, May 1995.

[52] R. Reiter. A Logic for Default Reasoning. Artificial Intelligence, 13:81–132, 1980.

[53] R. Reiter. Nonmonotonic Reasoning. Annual Reviews of Computer Science, 2:147–186, 1987.

[54] D. Roth. On the Hardness of Approximate Reasoning. Artificial Intelligence, 82(1/2):273–302, 1996.

[55] B. Selman and H. Kautz. Knowledge Compilation Using Horn Approximations. In Proc. AAAI-91, pp. 904–909, Anaheim, August 1991.

[56] B. Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proc. AAAI-92, pp. 440–446, 1992.

[57] B. Selman and H. J. Levesque. Abductive and Default Reasoning: A Computational Core. In Proc. AAAI-90, pp. 343–348, July 1990.

[58] J. Stillman. It’s Not My Default: The Complexity of Membership Problems in Restricted Propositional Default Logic. In Proc. AAAI-90, pp. 571–579, 1990.

[59] J. Stillman. The Complexity of Propositional Default Logic. In Proc. AAAI-92, pp. 794–799, 1992.

[60] L. Stockmeyer. On Approximation Algorithms for #P. SIAM J. Comput., 14:849–861, 1985.

[61] M. Vardi. Complexity of relational query languages. In Proc. 14th STOC, pp. 137–146, San Francisco, 1982.