Theoretical Computer Science, 189(1-2): 129–177, 1998

Abduction from Logic Programs: Semantics and Complexity^{∗}

Thomas Eiter^{†} Georg Gottlob Nicola Leone^{‡}

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

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

Abstract

Abduction– from observations and a theory, find using hypotheses an explanation for the observations – gained increasing interest during the last years. This form of reasoning has wide applicability in different areas of computer science; in particular, it has been recognized as an important principle of common-sense reasoning.

In this paper, we define a general abduction model for logic programming, where the inference operator (i.e., the semantics to be applied on programs), can be specified by the user. Advanced forms of logic programming have been proposed as valuable tools for knowledge representation and reasoning. We show that logic programming semantics can be more meaningful for abductive reasoning than classical inference by providing examples from the area of knowledge representation and reasoning. The main part of the paper is devoted to an extensive study of the computational complexity of the principal problems in abductive reasoning, which are: Given an instance of an abduction problem

(1) does the problem have solution (i.e., an explanation); (2) does a given hypothesis belong to some explanation; and (3) does a given hypothesis belong to all explanations.

This problems are analyzed for different underlying logic programming semantics, namely, the well-founded semantics, the stable model semantics and the minimal model semantics, paying attention to normal and disjunctive logic programs for the case of propositional as well as function-free first order programs. The main results are that the above abductive reasoning tasks on propositional logic programs populate the classes at the lower end of the polynomial hierarchy up to Σ_{4}^{P}, and provide complete problems for a number of classes over the first four levels of the hierarchy. Similar results are obtained in the first-order case. This proves abduction from logic programs as a rich source of problems of varying complexity.

∗A preliminary extended abstract of this paper appeared in the Proceedings of the Third International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR ’95), W. Marek, A. Nerode, and M. Truszczyński, editors, pp. 1–14, LNCS 982, 1995.

†Part of this author’s work has been carried out while visiting Stanford University.

‡This author was partially supported by the Istituto per la Sistemistica e l’Informatica of the Italian National Research Council (ISI-CNR)

Contents

1 Introduction 1

2 Preliminaries and Notation 7

2.1 Logic Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.1 Stable model semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.2 Well-founded semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.1.3 Stratified programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.2 Complexity Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Abduction Model 10 3.1 Logic Programming Abduction Problems . . . . . . . . . . . . . . . . . . . . 11 3.2 Generic Transformations Between Related Problems . . . . . . . . . . . . . . 13

3.2.1 Solution verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2.2 Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2.3 Relevance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2.4 Necessity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.5 Relevance and necessity under ⊆-solutions . . . . . . . . . . . . . . . . 14

4 Complexity Results 15

4.1 Well-Founded Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.1.1 No preference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.1.2 ⊆-preference with ⊧_{wf} . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.1.3 ≤-preference with ⊧_{wf} . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

4.2 Stable Cautious Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.2.1 No preference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.2.2 ⊆-preference with ⊧_{st}^{c} . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.2.3 ≤-preference with ⊧_{st}^{c} . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.3 Stable Brave Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

5 Abduction from Disjunctive Logic Programs 25 5.1 Disjunctive Logic Programming . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 Complexity Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

5.2.1 Disjunctive stable cautious reasoning . . . . . . . . . . . . . . . . . . . 28 5.2.2 Disjunctive stable brave reasoning . . . . . . . . . . . . . . . . . . . . 30 5.2.3 Minimal model semantics . . . . . . . . . . . . . . . . . . . . . . . . . 32

6 Abduction from Function-free First Order Programs 33

7 Related Work 37

8 Conclusion 39

1 Introduction

Logic programming is well-known as a powerful approach to declarative programming. Advanced semantics for negation and the capability of disjunction make logic programming yet more appealing for expressing problems in a variety of domains [4, 45].

The use of logic for representing knowledge was suggested by McCarthy in 1959 [51], and several researchers from various fields of computer science have then shown merits of logic for this purpose. However, the inadequacy of classical logic for representing commonsense knowledge is nowadays well understood, as its monotonicity (adding new information will never invalidate old conclusions) contrasts to the non-monotonic nature of commonsense reasoning. Thus, a number of logical formalisms, aimed at modeling commonsense reasoning, has been devised, among them modal logics [53, 55], default logic [63], and circumscription [52] (cf. also [50, 46]).

Logic programming with negation [44] and/or disjunction [45] shares with those formalisms the property of being non-monotonic. Its formalism is simple and natural, and its semantics has rigorous mathematical foundations; moreover, despite its simplicity, logic programming can express a wide range of problems even of high computational complexity [21, 66]. Thus, the use of logic programming as a valuable tool for knowledge representation and common-sense reasoning has been recently advocated [26, 45, 4].

So far, research on logic programming was mainly concerned with aspects of deduction from logic programs, in particular inference of (possibly negated) facts that are implicit by the meaning of the program. Besides deduction, abduction is another important kind of reasoning (though not completely disconnected), which has been first studied in depth by Peirce [57]. Given the observation of some facts, abduction aims at concluding the presence of other facts, from which, together with an underlying theory, the observed facts can be explained, i.e., deductively derived. Thus, roughly speaking, abduction amounts to an inverse of modus ponens.

For example, medical diagnosis is a typical abductive reasoning process: From the symptoms and the medical knowledge, a diagnosis about a possible disease is abduced. Notice that this form of reasoning is not sound (a diagnosis may turn out false), and that in general several abductive explanations (i.e., diagnoses) for observations may be possible.

During the last years, there has been increasing interest in abduction in different areas of computer science. It has been recognized that abduction is an important principle of common-sense reasoning, and that abduction has fruitful applications in a number of areas such diverse as model-based diagnosis [60], speech recognition [28], maintenance of database views [36], and vision [12].

In the past, most research on abduction concerned abduction from classical logic theories. However, we argue that the use of logic programming to perform abductive reasoning can be more appropriate in several applicative domains.

Example 1 For instance, consider the following scenario. Assume that it is Saturday and is known that Joe goes fishing on Saturdays if it’s not raining. This may be represented by the following theory T:

go fishing ← is saturday ∧ ¬rains ; is saturday ←

Now you observe that Joe is not out for fishing. Intuitively, from this observation we conclude that it rains (i.e, we abduce rains), for otherwise Joe would be out for fishing. Nevertheless, under classical inference, the fact rains is not an explanation of ¬go fishing, as T ∪ {rains} |̸= ¬go fishing (neither can one find any explanation). On the contrary, if we adopt the semantics of logic programming, then, according with the intuition, we obtain that rains is an explanation of ¬go fishing, as it is entailed by T ∪ {rains}.

Notice that in the above example, the same result would be obtained under abduction using classical inference if we considered the Clark completion [13] of the theory; this approach has been investigated for acyclic theories in [14]. As will be shown next, there are simple and relevant examples where abduction yields different results when using logic programming compared to classical inference from the Clark completion.

Example 2 Consider the logic program below, which describes possible movements of a robot in a certain area. Initially, the robot is at position a; he can reach a certain position Y, if he either is at Y or moves straight from a reachable position X to it, provided that the straight way is viable.

\begin{matrix}r_{1} : & at(a) ← \\ r_{2} : & reach(Y) ← at(X) \\ r_{3} : & reach(Y) ← viable straight(X, Y) ∧ reach(X) ∧ move(X, Y) \end{matrix}

Combined with facts about which straight moves are possible exist and which moves are planned, the program tells us which positions b can potentially be reached by the robot and which not; the reachable are those for which reach(b) is true. We stress that this knowledge can not be represented by applying the Clark completion on the theory, nor by any classical first order theory. This follow from the well-known fact that the transitive closure of a graph is not first-order definable [1].

Applying abduction on this program, one can plan the movements of the robot. Suppose the robot is requested to move from a to b, and passing through c is forbidden. Let LP = {r_{1}, r_{2}, r_{3}} ∪ B, where B is a set of facts with predicate viable straight which encode the viable straight ways. Then, each minimal set A of moves that entails reach(b), ¬reach(c), i.e., reach(b) and ¬reach(c) are deducible from LP ∪ A, represents a path for the robot from a to b that does not pass c. In other words, each minimal abductive explanation of the manifestations reach(b), ¬reach(c) is a possible such path for the robot. (The natural condition of minimality on explanations is discussed below.) However, abduction from this program under classical inference –even from its completion– does not yield the same result. This is verified e.g. by the scenario in which the viable straight ways constitute the following graph:

bc a

Then, under logic programming semantics, there is the unique minimal abductive explanation { move(a, b) }. This corresponds exactly to the only possible path, which directly leads from a to b. However, no abductive explanation (minimal or not) exists under classical inference, as ¬reach(c) can not be deduced, even from the completion of the program.

Further scenarios highlighting the difference between abduction under logic programming and classical inference from a program (resp. its completion) are described in Example 3 below and in Example 10 (Section 6).

In the context of logic programming, abduction has been first proposed by Kakas and Mancarella [37] and, during the recent years, common interest in the subject has been growing rapidly [14, 41, 37, 34, 17, 16, 68], also for the observation that, compared to deduction, this kind of reasoning has some advantages for dealing with incomplete information [16, 4]. A suggestive application of abduction from logic programs to data dictionary design is presented in [59].

The logic programs from above enjoy the property of being stratifiable [2], and thus has a generally accepted clear semantics. However, the declarative semantics of a logic program with negation is in general not immediately clear; different proposals for such a semantics exist. Thus, abductive reasoning on logic programs is affected by the particular semantics assigned to the program. Two dominant proposals for the semantics of logic programs with negation are the well-founded semantics [77] and the stable model semantics [25].

The well-founded semantics, differently from the previous proposals [2, 61], assigns a meaning to every logic program. The meaning of a program is a unique and always existing (possibly partial) model, which is called well-founded model. Intuitively, this semantics follows a “pessimistic” approach declaring false only atoms whose truth can be surely not derived from the program [18]. Inference of a literal from a general logic program under the wellfounded semantics is polynomial; hence, this semantics can express only polynomial time database queries [77].

The stable model semantics is closely related to classical non-monotonic logics. Indeed, the semantics of a program is defined by the set of its stable models, where a model is stable if it “regenerates itself” (like the stable expansions of an autoepistemic theory [55]). Since a program has in general several stable models, two inference modalities arise: brave inference (a literal is true if it is true in some stable model), and cautious inference (a literal is true if it is true in every stable model).

Even if stable model semantics increases the expressivity of well-founded semantics allowing to express NP-hard problems [66], several common situations require the possibility of explicitly encoding disjunctive information, cf. [45]. This observation lead to extend logic programs by permitting disjunction in the consequents (disjunctive logic programs). A number of different proposals for the semantics of disjunctive logic programs exist to date [45], among them the minimal model semantics [54], the (disjunctive) stable model semantics [62, 26], and the well-founded semantics [64, 3]. Besides the minimal model semantics (which has been designed for negation-free programs), the stable model semantics is the most commonly acknowledged approach; such semantics allow to express also problems whose complexity lies at the second level of the polynomial hierarchy [21].

Thus, making abduction from logic programs, one should agree on which semantics has to be considered (e.g., well-founded or stable model semantics); moreover, if a “multiple model” (e.g. stable model) semantics is adopted, one should also specify whether the cautious or brave version is chosen.

In this paper, we define a general abduction model for logic programming, where the inference operator (i.e., the semantics to be applied on the program) is not fixed a priori but can be specified by the user. In our opinion, this endows our model with a great flexibility, as the appropriate semantics can be chosen for each application domain. For instance, abduction with brave inference seems more appropriate for diagnosis, while the cautious inference operator appears well suited for planning (see Section 3).

Roughly speaking, we describe abduction from logic programs as follows: Given a logic program LP formalizing a particular application domain, a set M of literals describing some manifestations, a set H of atoms containing possible individual hypotheses, and an inference operator ⊧ defining the semantics of the program, find an explanation (or solution) for M, i.e., a suitable set S ⊆ H such that LP ∪ S ⊧ M.

For instance, the scenario in Example 1 (Joe’s Saturday business) can be represented as an abductive problem where LP = { go fishing ← is saturday ∧ ¬rains, is saturday ← }, M = {¬go fishing}, H = {rains}, and the inference operator is ⊧_{wf} (entailment under well-founded semantics). It is immediately recognized that S = {rains} is a solution. Let us consider another example.

Example 3 Imagine an electrical circuit consisting of a simple stove with two hot-plates wired in parallel and a control light, which is on if at least one of the plates is on operation. Each plate has a fuse, and it is known that one of them can not stand much current and will melt if the current gets high, but it is not known which one. Consider the following program P:

\begin{matrix}melted fuse_{1} ∨ melted fuse_{2} ← & high current \\ light off ← & melted fuse_{1} ∧ melted fuse_{2} \\ light off ← & power failure \\ light off ← & broken bulb \\ burns plate_{1} ← & ¬melted fuse_{1} ∧ ¬power failure \\ burns plate_{2} ← & ¬melted fuse_{2} ∧ ¬power failure \end{matrix}

The first rule states that on high current, a fuse will melt. The second through fourth rule describe situations under which the control light is off, namely, if both fuses are melted, if the power fails, and if the bulb is broken. The last two rules state that a hot-plate burns if there is no power failure and the fuse is not melted.^{1}

For example, given the observation light off , under the stable model semantics we can abduce power failure as an explanation under both brave and cautious inference operators, i.e., S = {power failure} is a solution for both the abductive problems P = ⟨H, M, P, ⊧_{st}^{b}⟩ and P′ = ⟨H, M, P, ⊧_{st}^{c}⟩ where H = {power failure, broken bulb, high current}, M = {light off }, and ⊧_{st}^{b} and ⊧_{st}^{c} denotes the brave and cautious inference operator, respectively.

1To keep the example simple, we refrain from modeling switches for the hot-plates.

Indeed, P ∪ {power failure} has the single stable model M_{1} = {power failure, light off }. Similarly, also broken bulb is an explanation of light off , while high current is not.

Given the additional observation ¬burns plate_{1} (i.e., considering the manifestation M′ = {light off , ¬burns plate_{1} }), we still have power failure as an explanation, but no longer broken bulb. Under brave inference, however, we get that S′ = {broken bulb, high current} is an explanation (i.e., S′ is a solution for ⟨H, M′, P, ⊧_{st}^{b}⟩); this is reasonable in some sense. Notice that under classical inference, power failure is not an explanation, since P ∪ {power failure} |̸= ¬burns plate_{1}; however, it is an explanation on the completion of P.^{2}

Finally, assume the observations light off , burns plate_{1}, and burns plate_{2} are made. The only explanation for that is bulb broken (under cautious as well as brave inference), which is intuitive. Under classical inference, no explanation exists, even from the completed program (notice that abducible atoms should not be completed [14]).

Usually, different abductive solutions may be regarded not as equally appealing. Following Occam’s principle of parsimony, one is often willing to prefer as simplest solutions as possible. In particular, solutions should be nonredundant, i.e., an acceptable solution must not contain another solution properly. The property of subset-minimality is the most commonly applied criterion for acceptable abductive solutions, cf. [58, 74, 9, 41]. For example, for the observation light off in the above example, {bulb broken, power failure} would be a solution (under both variants of inference). The simpler solution bulb broken (or power failure as well) is clearly preferable. Besides subset-minimality, smallest size of solutions is a commonly applied criterion for acceptable solutions, cf. [58]. We will deal with both criteria.

In the context of abduction, three main decision problems arise: (1) to determine whether an explanation for the given manifestations exists at all; (2) to determine whether an individual hypothesis h ∈ H is relevant, i.e., whether it is part of at least one acceptable explanation;

(3) to determine whether an individual hypothesis is necessary, i.e., whether it occurs in all acceptable explanations. For instance, in the circuit example we have: (1) there exists a solution for the manifestation light off , (2) the atoms bulb broken and power failure are relevant for some solution, (3) none of them (as well as any other hypothesis) is necessary. The complexity of the three decision problems above will be carefully analyzed in the paper.

The contribution of the present paper to abductive logic programming is twofold. First, we formally define a general abductive model for logic programs (informally presented above), in which also some previously proposed abductive framework can be easily modeled. Second, we precisely determine the computational complexity of abductive problems under: (1) the well-founded semantics for normal logic programs [77], (2) the stable model semantics for normal logic programs [25], (3) the stable model semantics for disjunctive logic programs [62], and (4) the minimal model semantics for disjunctive logic programs [54]. For each semantics we shall analyze the complexity of relevance, necessity and existence of abductive solutions, by considering also the case where solutions must satisfy some minimality criterion.

2Although the completion has been defined in [13] only for nondisjunctive logic programs, it is clear how to complete this particular program in the spirit of [13].

This constitutes the main part of the present paper, and provides many new and interesting results:

1. Even if stable-brave deduction is harder than well-founded deduction (the former is NP-complete while the latter is polynomial), the complexity of stable-brave abduction is essentially the same as of well-founded abduction (the various abductive problems under these semantics have a complexity ranging from P to Σ_{2}^{P}).

2. While the complexities of stable-brave and stable-cautious deduction lie at the same level in the polynomial hierarchy, the complexity of stable-cautious abduction is located one level higher than the one of stable-brave abduction, and thus most likely strictly harder.

3. Allowing disjunction in the rule heads further increases the complexity of the abductive problems. As for normal logic programs, cautious reasoning reveals to be harder than brave reasoning. Moreover, abduction under minimal model and stable model semantics have the same computational complexity.

4. The complexities of the various abductive reasoning tasks under the considered semantics range over the first four levels of the polynomial hierarchy. Most complexity classes from there, including the classes Σ_{k}^{P}, Π_{k}^{P}, D_{k}^{P}, and Δ_{k}^{P} [O(log n)] have abductive reasoning tasks complete for them. Thus, our analysis exhibits practical problems complete even for complexity classes for which few complete problems are known to date (e.g., the complexity class Σ_{4}^{P}).

The complexity results above refer to abductive problems on propositional logic programs. For function-free first order logic programs, the data-complexity of abduction (i.e., the program except for ground facts is fixed) coincides with the complexity of abduction from propositional logic programs. (In the nonfixed case, the complexity is expected to be exponentially higher.)

We first present our model for abduction from propositional logic programs and determine its complexity; after that, we provide a generalization of this model to allow for abduction from function-free first order logic programs and address the resulting complexity. Notice that, extending our work, complexity results for abduction from logic programs in the presence of functions appear in [47].

Our results impact on other work on logic programming as follows. For example, from the complexity classification, we know whether an efficient (i.e., polynomial time) transformation from an abduction problem to another reasoning problem whose complexity is known is possible or not. In particular, it tells us whether abduction can be efficiently transformed to deduction in logic programming, and thus whether a search for an efficient embedding of abductive logic programming into deductive logic programming is reasonable. Moreover, by the level of the hierarchy, we know how many sources of complexity an abduction problem bears, and which kind of backtracking algorithm for solving it will be suitable. (See also Section 8.)

The sequel of the paper is organized as follows. Section 2 contains some preliminaries on both logic programming and complexity theory. Section 3 formally defines our abduction model in the propositional case. The complexity of the various abductive problems for normal logic programs is determined in Section 4. Section 5 deals with the extension of the abduction model by allowing for disjunctive logic programs. Section 6 generalizes the abductive model to the case of function-free first-order logic programs and discusses the data-complexity. Section 7 overviews some related works. Finally, Section 8 gives our conclusions and summarizes the complexity results determined in the paper.

2 Preliminaries and Notation

2.1 Logic Programming

The section recalls the basic concepts of (propositional) logic programming. The syntax of logic programs is given first; then stable and well-founded semantics [25, 77] are provided. Stratified programs [2] and their properties are finally presented.

Let a set V of propositional variables be given. A positive literal (atom) is an element a ∈ V; a negative literal is the negation ¬a of an atom. A program clause (or rule) r is

a ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬b_{k+1} ∧ ⋯ ∧ ¬b_{m}, m ≥ 0

where a, b_{1}, ⋯, b_{k} are positive literals and ¬b_{k+1}, ⋯, ¬b_{m} are negative literals. The atom a is called the head of r, while the conjunction b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬b_{k+1} ∧ ⋯ ∧ ¬b_{m} is its body. A (propositional) logic program is a finite set LP of program clauses; it is positive (or ¬-free), if no negative literal occurs in it. As usual, it is tacitly assumed that V is, unless specified otherwise, the set of atoms occurring in LP.

A (total) interpretation is a subset of V. A positive literal a (resp. a negative literal ¬a) is true with respect to an interpretation I if a ∈ I (resp. a ∉ I); otherwise it is false. A rule is satisfied (or is true) w.r.t. I if its head is true or its body is false w.r.t. I. An interpretation I is a model for a logic program LP if it satisfies all rules in LP.

2.1.1 Stable model semantics

Given a logic program LP and an interpretation I, the Gelfond-Lifschitz transform of LP with respect to I is the logic program LP^{I} consisting of all rules a ← b_{1} ∧ ⋯ ∧ b_{k} such that

(1) a ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬b_{k+1} ∧ ⋯ ∧ ¬b_{m} ∈ LP and (2) b_{i} ∉ I, for all k < i ≤ m.

Notice that ¬ does not occur in LP^{I}, i.e., it is a Horn program. Each Horn program P has a least model (i.e., a model included in every model), denoted by lm(P). An interpretation I is called a stable model of LP [25] iff I = lm(LP^{I}). The collection of all stable models of LP is denoted by STM(LP) (i.e., STM(LP) = {I | I = lm(LP^{I})}).

Example 4 Consider the following program LP:

a ← ¬b  b ← ¬a  c ← a  c ← b

The stable models of LP are M_{1} = {a, c} and M_{2} = {b, c}. Indeed, by definition of Gelfond-Lifschitz transform, LP^{M_{1}} = { a ←, c ← a, c ← b } and LP^{M_{2}} = { b ←, c ← a, c ← b }; thus, it is immediately recognized that lm(LP^{M_{1}}) = M_{1} and lm(LP^{M_{2}}) = M_{2}.

The example shows that a logic program may have several stable models (there can also be none). The modalities of brave and cautious reasoning are used to handle this.

Brave reasoning (or credulous reasoning) infers that a literal Q is true in LP (denoted LP ⊧_{st}^{b} Q) iff Q is true with respect to M for some M ∈ STM(LP).

Cautious reasoning (or skeptical reasoning) infers that a literal Q is true in LP (denoted LP ⊧_{st}^{c} Q) iff (1) Q is true with respect to M for all M ∈ STM(LP) and (2) STM(LP) ≠ ∅.^{3}

The inference relations ⊧_{st}^{b} and ⊧_{st}^{c} extend to sets of literals as usual.

Example 5 For the program LP of Example 4, a, b and c are brave inferences (LP ⊧_{st}^{b} {a, b, c}); the only cautious inference is c (LP ⊧_{st}^{c} c).

2.1.2 Well-founded semantics

A partial (3-valued) interpretation I is a consistent set of literals over V. Each atom a is considered to be true in I if a ∈ I, false in I if ¬a ∈ I, and undefined in I otherwise.

Let LP be a program and I be a (partial) interpretation. A set N of atoms is an unfounded set of LP w.r.t. I if each atom a in N satisfies the following condition: For each rule r ∈ LP whose head is a at least one of the following holds: (1) some literal in the body of r is false w.r.t. I, or (2) some positive literal of the body of r belongs to N. Unfounded sets are closed under unions; the union of all unfounded sets w.r.t. I is called the Greatest Unfounded Set for LP with respect to I and denoted by GUS_{LP} (I).

The well-founded model of LP is defined as the least fixed point of an operator which infers truth of atoms by classical immediate consequence and falsity using the Greatest Unfounded Set. Formally, define for program LP and interpretation I the following transformations:

1. T_{LP} (I) = {Q | ∃r ∈ LP s.t. Q is the head of r and the body of r is true w.r.t. I}

2. W_{LP} (I) = T_{LP} (I) ∪ {¬y | y ∈ GUS_{LP} (I)}

Consider the sequence W_{0} = ∅, W_{n} = W_{LP} (W_{n−1}). The sequence finitely converges to a limit W_{λ}. W_{λ} is called the well-founded model of LP [77], which is denoted by W F (LP). Observe that, since the positive inferences of W_{LP} are done by using the immediate consequence operator T_{LP}, the well-founded model is supported, i.e., a positive literal Q is in W F (LP) only if there is a rule with head Q whose body is true w.r.t. W F (LP). The well-founded model has the following important property.

Proposition 1 [77] Given a logic program LP, the well-founded model W F (LP) can be computed in polynomial time.

3Note that (2), i.e., consistency of LP under stable semantics, is usually not requested in the definition of cautious consequence; we denote this version of cautious consequence by ⊧_{st}^{cls}. As shown in the next section, however, consistency is needed for abduction.

Example 6 Consider the following program LP:

p ← q ∧ ¬r  q ← ¬p  s ← r

We have (W_{0} = ∅):

\begin{matrix}T_{LP} (W_{0}) = ∅; & GUS_{LP} (W_{0}) = \{r, s\}; & W_{1} = W_{LP} (W_{0}) = \{ ¬r , ¬s \}; \\ T_{LP} (W_{1}) = ∅; & GUS_{LP} (W_{1}) = \{r, s\}; & W_{2} = W_{LP} (W_{1}) = \{ ¬r , ¬s \}; \end{matrix}

and hence W_{λ} = W_{2} = { ¬r , ¬s } is the well-founded model of LP. Thus, r and s are false in the well-founded semantics, while p and q are undefined. Indeed, while it is intuitive that r and s should be false, it is unclear which value should be assigned to p and q. On this program the well-founded semantics behaves better than the stable one which says nothing about the truth valuation of the literals as the program has no stable model. On the contrary, on program LP of Example 4 the well-founded model is empty and, differently from the stable semantics, does not entail truth of c; however, several researchers have claimed that c should be entailed from LP [5, 3].

The well-founded semantics regards W F (LP) as the intended meaning of the program LP. Accordingly, it infers that a literal Q is true in LP, denoted LP ⊧_{wf} Q, iff it is true in the well-founded model (i.e., Q ∈ W F (LP)). This extends to inference of a set of literals as usual.

2.1.3 Stratified programs

Although stable and well-founded semantics are different in general, they coincide on the important class of stratified logic programs [2].

A logic program LP is stratified iff it is possible to partition the set of its atoms into strata ⟨S_{1}, …, S_{r}⟩, such that for every rule a ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬c_{1} ∧ ⋯ ∧ ¬c_{m} in LP the following holds, where Strat(x) = i iff x ∈ S_{i}:

Strat(b_{j}) ≤ Strat(a), for all 1 ≤ j ≤ k, and Strat(c_{l}) < Strat(a), for all 1 ≤ l ≤ m.

Proposition 2 [77] Let LP be a stratified logic program. Then, the well-founded model of LP is total, and it coincides with the unique stable model of LP.

As a consequence, ⊧_{wf}, ⊧_{st}^{b}, and ⊧_{st}^{c} are all equivalent on stratified programs.

2.2 Complexity Theory

For NP-completeness and complexity theory, cf. [56]. The classes Σ_{k}^{P} , Π_{k}^{P} and Δ_{k}^{P} of the Polynomial Hierarchy (PH) (cf. [75]) are defined as follows:

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

In particular, NP = Σ_{1}^{P}, co-NP = Π_{1}^{P}, and Δ_{2}^{P} = P^{NP}. Here P^{C} and NP^{C} denote the classes of problems that are solvable in polynomial time on a deterministic (resp. nondeterministic)

Turing machine with an oracle for any problem π in the class C. The oracle replies to a query in unit time, and thus, roughly speaking, models a call to a subroutine for π that is evaluated in unit time. If C has complete problems, then instances of any problem π′ in C can be solved in polynomial time using an oracle for any C-complete problem π, by transforming them into instances of π; we refer to this by stating that an oracle for C is used. Notice that all classes C considered here have complete problems.

The classes Δ_{k}^{P}, k ≥ 2, have been refined by the class Δ_{k}^{P} [O(log n)], in which the number of calls to the oracle is in each computation bounded by O(log n), where n is the size of the input. The class D_{k}^{P}, which is defined as the class of problems that consist of the conjunction of two (independent) problems from Σ_{k}^{P} and Π_{k}^{P}, respectively, is considered to be further restricted in computational power. Notice that for all k ≥ 1,

Σ_{k}^{P} ⊆ D_{k}^{P} ⊆ Δ_{k+1}^{P}[O(log n)] ⊆ Δ_{k+1}^{P} ⊆ Σ_{k+1}^{P} ⊆ PSPACE;

each inclusion is widely conjectured to be strict. Note that, by the rightmost inclusion, all these classes contain only problems that are solvable in polynomial space. They allow, however, a finer grained distinction between NP-hard problems that are in PSPACE.

The above complexity classes have complete problems under polynomial-time transformations involving quantified Boolean formulas (QBFs). A QBF is an expression of the form

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

where E is a Boolean expression whose atoms 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 (1).

Given a k-existential QBF Φ (resp. a k-universal QBF Ψ), deciding 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}. Deciding, given an arbitrary number of QBFs of form (1), whether the number of valid QBFs among them is odd is complete for Δ_{k+1}^{P}[O(log n)]. The problems remain as hard under the following restrictions:

(1) E in (1) is in conjunctive normal form and each clause contains three literals (3CNF) if Q_{k} = ∃, and (2) E is in disjunctive normal form and each monom contains three literals (3DNF) if Q_{k} = ∀ [76].

3 Abduction Model

In this section, we describe our formal model for abduction from logic programs and state the main decisional reasoning tasks for abductive reasoning. The abduction model is defined here for propositional programs; the generalization to logic programs with variables is given in Section 6.

3.1 Logic Programming Abduction Problems

Definition 1 Let V be a set of propositional atoms. A logic programming abduction problem (LPAP) P over V consists of a tuple ⟨H, M, LP, ⊧⟩, where H ⊆ V is a finite set of hypotheses, M ⊆ V ∪ {¬v | v ∈ V } is a finite set of manifestations, LP is a propositional logic program on V, and ⊧ is an inference operator.

For simplicity, we suppose throughout the rest of the paper that V is implicitly defined as the set of propositional atoms appearing in P, which we denote by V_{P}, and omit the phrase “over V ”.

Remark: This model does not include specification of constraints on the logic program. However, the most used form of constraint ← a_{1} ∧ … ∧ a_{n} which means that a_{1}, …, a_{n} may not be true simultaneously, can be easily simulated in our model, by adding a rule abs ← a_{1} ∧ … ∧ a_{n} to the logic program, where abs is a new propositional atom, and adding ¬abs to the manifestations.

Definition 2 Let P = ⟨H, M, LP, ⊧⟩ be a LPAP, and let S ⊆ H. Then, S is a solution (or explanation) to P iff LP ∪ S ⊧ M.

The set of all solutions to P is denoted by Sol(P).

In this paper we consider abductive problems for the inference operators ⊧_{wf}, ⊧_{st}^{b}, and ⊧_{st}^{c}. Note that, in the definition of cautious abduction, we have not used the classical skeptical operator (a literal is true if it is true in all stable models), but we have adopted the inference operator ⊧_{st}^{c} which requires additionally that the program has (at least) one stable model. The reason for that is the need to guarantee that LP ∪ S is “consistent”; otherwise, any set of atoms S making the logic program inconsistent would be an explanation of all possible manifestations.

Example 7 Consider the LPAP P = ⟨{d, b}, {c}, LP, ⊧_{st}^{cls}⟩, where LP = {a ← b∧¬a , c ← d } and ⊧_{st}^{cls} is classical stable cautious inference. One reasonably expects that the observation of c abduces the atom d. Nevertheless, since LP ∪{b} has no stable model and, as a consequence, LP ∪ {b} ⊧_{st}^{cls} c, the set {b} is a solution to P. On the contrary, the problem does not arise with the inference operator ⊧_{st}^{c}. Indeed, if we consider the LPAP P′ = ⟨{d, b}, {c}, LP, ⊧_{st}^{c}⟩, then {b} is not a solution to P′, as this operator requires the existence of a stable model (ensuring the consistency of the program).

The explicit introduction of the inference operator in the definition of abduction problem endows our abduction model with a great flexibility, since the appropriate semantics can be adopted on each application domain. This is particularly important in logic programming, as no semantics is generally accepted as the best one for all logic programs; rather, it is acknowledged that the right semantics must be chosen on the particular domain. It is interesting to briefly discuss on the applicability on different domains of brave and cautious reasoning, respectively. We argue that brave inference is well suited for diagnosis, while cautious inference is adequate for planning. In fact, consider a system represented by a logic program LP with stable model semantics. If the system is solicited by some input, represented by adding a set A of atoms to LP, then each stable model of LP ∪ A is a possible evolution of the system, i.e., each stable model represents a possible reaction of the system to A.

Diagnosis consists, loosely speaking, in deriving from an observed system state (characterized by the truth of a set F of facts), a suitable input A which caused this evolution. Now, since each stable model of LP ∪ A is a possible evolution of the system with input A, we can assert that A is a possible input that caused F if LP ∪ A ⊧_{st}^{b} F. Thus, diagnostic problems can be naturally represented by abductive problems with brave inferences.

Suppose now that we want that the system is in a certain state (described by a set F of facts), and we have to determine the “right” input 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 input 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 LP ∪ A ⊧_{st}^{c} F. Hence, planning activities can be represented by abductive problems with cautious inferences.

The next section shows that abduction under cautious inference has most likely a higher complexity than abduction under brave modality; thus, from the above point of view, planning is most likely harder than diagnosis.

The following properties of a hypothesis in a LPAP P are of natural interest with respect to computing abductive solutions.

Definition 3 Let P = ⟨H, M, LP, ⊧⟩ be a LPAP and h ∈ H. Then, h is relevant for P iff h ∈ S for some S ∈ Sol(P), and h is necessary for P iff h ∈ S for every S ∈ Sol(P).

We refer to the property opposite to necessity also as dispensability (cf. [33]). Now, the main decisional problems in abductive reasoning are as follows: Given a LPAP P = ⟨H, M, LP, ⊧⟩,

1. does there exist a solution for P ? (Consistency)

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

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

It is common in abductive reasoning to prune the set of all solutions and to focus, guided by some principle of solution preference, on a set of preferred solutions. Two important notions of preferred solutions are irredundant solutions, i.e., solutions which do not contain any other solution properly (cf. [58, 74, 41]), and solutions of smallest cardinality (cf. [58]). We refer to the former solutions of a LPAP P as ⊆-solutions and to the latter as ≤-solutions, and denote their collection by Sol_{⊆}(P) and Sol_{≤}(P), respectively.

The properties of relevance and necessity of a hypothesis for a LPAP P with respect to Sol_{⊆}(P) (resp. Sol_{≤}(P)) rather than Sol(P), are referred to as ⊆-relevance and ⊆-necessity (resp. ≤-relevance and ≤-necessity).

The complexity of the problems consistency, relevance, and necessity under inference operators ⊧_{wf}, ⊧_{st}^{b}, and ⊧_{st}^{c}, combined with ⊆-solutions and ≤-solutions, is studied in Section 4.

3.2 Generic Transformations Between Related Problems

Prior to the analysis of abduction problems under particular semantics, we note some general reducibilities among abduction problems and deductive inference problems. One the one hand, the reducibilities show us how different reasoning tasks are related; in fact, the relationship is close in some cases. On the other hand, they help to simplify the proofs of several complexity results. Moreover, we point out relationships between abduction using arbitrary and ⊆-solutions.

3.2.1 Solution verification

It is clear that entailment of a conjunction of literals and solution verification are equivalent. We state this for later reference.

Proposition 3 (Equivalence of solution verification and entailment) Deciding, given a LPAP P = ⟨H, M, LP, ⊧⟩ and a set S ⊆ H, whether S ∈ Sol(P) is w.r.t. polynomial-time transformation equivalent to the entailment problem LP 1 ⊧ γ, where LP 1 is a logic program and γ is a conjunction of literals.

3.2.2 Consistency

Deductive entailment is a subtask inherent to abduction. This problem can be reduced to consistency by means of a simple generic transformation, which gives us the following result.

Proposition 4 (Entailment reduces to consistency) Entailment of a conjunction γ of literals from a logic program LP, LP ⊧ γ, reduces in polynomial time to consistency under ⊧.

Proof. Suppose we want to decide whether LP ⊧ γ, where γ = q_{1} ∧ ⋯ ∧ q_{k} and the q_{i} are literals. Then we consider the LPAP P = ⟨∅, {q_{1}, …, q_{k}}, LP, ⊧⟩. The only possible solution to P is ∅. Obviously, ∅ ∈ Sol(P) if an only if LP ⊧ γ.

Thus, the complexity of entailment is a –naturally expected– lower complexity bound for consistency. As will be seen, it will be complemented in some cases by a matching upper bound.

Notice that, as an immediate corollary to Propositions 3 and 4, solution verification easily reduces to consistency in polynomial time.

3.2.3 Relevance

It turns out that the complexities of consistency and relevance always coincide. In fact, this can be established by means of generic reductions between the problems.

Proposition 5 (Equivalence of consistency and relevance) Problems consistency and relevance are equivalent w.r.t. polynomial-time transformation.

Proof. Consistency can be reduced to relevance. Let P = ⟨H, M, LP, ⊧⟩ be an LPAP. Suppose we want to decide whether Sol(P) ≠ ∅. Then we consider P′ = ⟨H ∪ {q}, M, LP, ⊧⟩ where q is a fresh atom. Now, S ∈ Sol(P) if and only if S ∪ {q} ∈ Sol(P′), for every S ⊆ H. Hence, P is consistent if and only if q is relevant for P′.

Relevance can be reduced to consistency. Let P = ⟨H, M, LP, ⊧⟩ be an LPAP and h ∈ H. Suppose we want to decide whether there is some S ∈ Sol(P) such that h ∈ S. Then we consider P′ = ⟨H, M, LP ∪ {h}, ⊧⟩. Now, h is relevant for P if and only if P′ is consistent. To see this, suppose first that h is relevant for P. Hence, there exists an S ⊆ H such that h ∈ S and LP ∪ S ⊧ M. Clearly, LP ∪ {h} ∪ S ⊧ M, and therefore S ∈ Sol(P′). Thus, P′ is consistent. Conversely, suppose that P′ is consistent, i.e., there is some S ∈ Sol(P′). Since LP ∪ {h} ∪ S ⊧ M, we have S ∪ {h} ∈ Sol(P), which means that h is relevant for P.

This relationship allows to derive complexity results for relevance immediately from complexity results for consistency.

3.2.4 Necessity

Necessity is related to consistency similarly as relevance. In fact, necessity turns out to be equivalent to inconsistency, the complement of consistency.

Proposition 6 (Equivalence of inconsistency and necessity) Problems inconsistency and relevance are equivalent w.r.t. polynomial-time transformation.

Proof. Inconsistency can be reduced to necessity Let P = ⟨H, M, LP, ⊧⟩ be an LPAP. Suppose we want to decide whether Sol(P) = ∅. Then we consider as above P′ = ⟨H ∪ {q}, M, LP, ⊧⟩ where q is a fresh atom. Now, q is necessary, i.e., q occurs in every solution S ∈ Sol(P) if and only if Sol(P) = ∅, i.e., P is inconsistent.

Necessity can be reduced to inconsistency. Let P = ⟨H, M, LP, ⊧⟩ be an LPAP and h ∈ H. Suppose we want to decide whether h ∈ S for all S ∈ Sol(P). Then we consider P′ = ⟨H \ {h}, M, LP, ⊧⟩. Now, for every inference relation ⊧ from ⊧_{wf}, ⊧_{st}^{b}, and ⊧_{st}^{c}, we clearly have that P′ is inconsistent if and only if h is necessary for P.

Note that the two reductions obviously hold for every “reasonable” inference relation; thus, inconsistency and necessity are equivalent in any reasonable inference setting.

3.2.5 Relevance and necessity under ⊆-solutions

Using minimal solutions (i.e., ⊆-solutions) instead of arbitrary solutions has different effects to relevance and necessity. For the former problem, we note the following proposition.

Proposition 7 Suppose that consistency for a class of LPAPs is in the complexity class C. Then, ⊆-relevance is in NP^{C}.

Proof. That a hypothesis h ∈ H is ⊆-relevant for P = ⟨H, M, LP, ⊧⟩ can be nondeterministically proved as follows. Guess a minimal solution S so that h ∈ S. (That is, guess S′ ⊆ H and consider S = S′ ∪ {h}.) The guess is verified by testing (1) S ∈ Sol(P) and (2) there is no S′ ⊂ S such that S′ ∈ Sol(P). Since solution verification reduces efficiently to consistency (cf. Propositions 3 and 4), it follows from the hypothesis that (1) can be decided in polynomial time with a call to an oracle for consistency. Test (2) can be decided with checking whether for each h′ ∈ S, the LPAP ⟨S \ {h′}, M, LP, ⊧⟩ is inconsistent. By hypothesis, each such test is polynomial with an oracle for consistency. Therefore, (1) and (2) can be decided in polynomial time with an oracle for consistency. It follows that ⊆-relevance is in NP^{C}.

There is a simple relationship between necessity on arbitrary and ⊆-solutions, respectively.

Proposition 8 Let P = ⟨H, M, LP, ⊧⟩ be a LPAP and let h ∈ H. Then, h is ⊆-necessary for P iff h is necessary for P.

From this observation, we do not deal with ⊆-necessity explicitly in our analysis.

4 Complexity Results

In this section, we determine the complexity of the main reasoning tasks on the abduction model from the previous section. In particular, we study the complexity of abduction under well-founded, stable cautious, and stable brave semantics in the specified order. For each semantics each abductive problem is first analyzed in the case of no preference criterion and then under both the subset-minimality and the smallest-cardinality preference principle.

Several hardness results will be derived by reductions of validity testing for QBFs. The reduction will often use the rewriting of a boolean expression E in CNF or DNF into a set of propositional programming rules. Before starting the complexity analysis, we fix some helpful notation.

For a Boolean formula E in CNF (resp. DNF), we denote by \overline{E} the DNF (resp. CNF) expression obtained by applying De Morgan’s rule to ¬E and cancelling all double negations. For instance, given E = (x_{1}∨¬x_{2})∧x_{3}, \overline{E} = (¬x_{1}∧x_{2})∨¬x_{3}. Note that \overline{\overline{E}} = E. Furthermore, given a Boolean expression E in CNF, we define transf(E) as follows:

\begin{aligned}transf(E) = \{ & abs ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬a_{1} ∧ ⋯ ∧ ¬a_{l} | \\ & a_{1} ∨ ⋯ ∨ a_{l} ∨ ¬b_{1} ∨ ⋯ ∨ ¬b_{k} ∈ E (k, l ≥ 0) \} \end{aligned}

Moreover, given a set Y of propositional variables, we shall denote by Y′ the set {y′ | y ∈ Y }.

Let X be the set of propositional atoms appearing in E. Each truth assignment I to the atoms in X can be naturally seen as the subset X_{I} ⊆ X of the atoms true w.r.t. I (i.e., X_{I} = {x ∈ X | I(x) = true}). Observe that for each X1 ⊆ X, the program transf(E) ∪ X1 is stratified; thus, by Proposition 2, it has a total well-founded model which coincides with its unique stable model.

In transf(E), abs (standing for “absurd”) represents falsity: given a truth assignment I for the atoms in a CNF expression E, a clause

a_{1} ∨ ⋯ ∨ a_{l} ∨ ¬b_{1} ∨ ⋯ ∨ ¬b_{k} ∈ E

is satisfied by I iff abs is not derivable from the corresponding rule

abs ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬a_{1} ∧ ⋯ ∧ ¬a_{l} ∈ transf(E) ∪ X_{I}

(under well-founded or stable semantics). Thus, I is a model of E if and only if abs is not deducible from X_{I} ∪transf(E). (Note that since the program is stratified, deducibility under well-founded, stable brave, and stable cautious semantics coincide).

For instance, consider the simple CNF expression E = z_{1} ∨ z_{2} ∨ ¬z_{3}. Then,

transf(E) = {abs ← z_{3} ∧ ¬z_{1} ∧ ¬z_{2} }

It is immediately recognized that a truth assignment I to the atoms from Z = {z_{1}, z_{2}, z_{3}} satisfies E if and only if transf(E) ∪ Z_{I} ⊧_{wf} ¬abs (equivalently, transf(E) ∪ Z_{I} ⊧_{st}^{b} ¬abs, or transf(E) ∪ Z_{I} ⊧_{st}^{c} ¬abs). Thus, the above stated correspondence can be profitably used to check the validity of QBFs. For instance, the formula ∃ZE is valid (i.e., it is in QBF_{1,∃}) iff there exists Z1 ⊆ Z such that transf(E) ∪ Z1 ⊧_{wf} ¬abs (equivalently, transf(E) ∪ Z1 ⊧_{st}^{b} ¬abs, or transf(E) ∪ Z1 ⊧_{st}^{c} ¬abs).

4.1 Well-Founded Semantics

4.1.1 No preference

From Proposition 1 it is immediate that checking whether a set S is a solution to a LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is possible in polynomial time. On the other hand, this problem contains inference of an atom from a negation-free logic program (i.e., a Horn program) as a subproblem, which is well-known to be logspace-hard for P (cf. [78, 56]). Thus, by Proposition 3, we conclude

Proposition 9 Let P = ⟨H, M, LP, ⊧_{wf}⟩ be a LPAP. Deciding if S ⊆ H fulfills S ∈ Sol(P) is logspace-complete for P.

While this is a positive result, checking the consistency of a LPAP is most likely intractable.

Theorem 1 To decide if Sol(P) ≠ ∅ for a given LPAP P = ⟨H, M, LP ⊧_{wf}⟩ is NP-complete. NP-hardness holds even if LP is a stratified logic program.

Proof. NP-Membership. A guess S ⊆ V_{P} can be verified in polynomial (Proposition 9). NP-Hardness. We transform deciding ∃XE ∈ QBF_{1,∃}, where E is in 3CNF, into checking Sol(P) ≠ ∅ for a LPAP P.

Consider the LPAP P = ⟨X, {¬abs}, LP, ⊧_{wf}⟩, where LP = transf(E).

Recall that, for each X1 ⊆ X, LP ∪X1 is stratified; hence, by Proposition 2 it has a total well-founded model. As a consequence, given X1 ⊆ X, each x_{i} ∈ X is either true or false w.r.t. W F (LP ∪ X1). Now, consider the set of logic programs L = {LP ∪ X1 | X1 ⊆ X}. Because of the specific form of LP, there is a 1-1 correspondence between the possible truth assignments to the atoms in X, and the set of well-founded models of the programs in L (the image of a truth assignment I is W F (LP ∪ X_{I})). Furthermore, it is easy to see that E is satisfied by an assignment I if and only if W F (LP ∪X_{I}) ⊧ ¬abs (recall that the well-founded model is supported). Hence, there exists an assignment I satisfying E iff there exists X1 ⊆ X such that W F (LP ∪ X1) ⊧ ¬abs. In other words, ∃XE is valid iff Sol(P) ≠ ∅. Checking if Φ = ∃XE ∈ QBF_{1,∃} is NP-hard, thus deciding Sol(P) ≠ ∅ is NP-hard as well. Moreover, since LP is stratified, we have also shown that NP-hardness holds even if the logic program LP from P is stratified.

As shown in Section 3.2, problem relevance has the same complexity as consistency.

Theorem 2 Deciding if a given hypothesis is relevant for a given LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is NP-complete. NP-hardness holds even if LP is a stratified logic program.

Proof. The result for the general case is immediate from Proposition 5 and Theorem 1. Hardness for stratified logic program holds as consistency is already NP-hard in that case, and the reduction from consistency to relevance in the proof of Proposition 5 maps a stratified logic program to a stratified logic program.

Finally, we state the result for necessity, which has complementary complexity of consistency.

Theorem 3 Deciding if a given hypothesis is necessary for a given LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is co-NP-complete. co-NP-hardness holds even if LP is a stratified logic program.

4.1.2 ⊆-preference with ⊧_{wf}

Now we determine the complexity of the main reasoning tasks if acceptable solutions must be irredundant, i.e., minimal with respect to ordinary set inclusion. Intuitively, this requirement makes solution verification harder, since, given a candidate S for a solution, current methods will have to inspect an exponential number of subsets in the worst case to prove that no solution properly included in S exists.

Theorem 4 Deciding if a given hypothesis is ⊆-relevant for a LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is Σ_{2}^{P} -complete. Σ_{2}^{P} -hardness holds even if LP is a stratified logic program.

Proof. Σ_{2}^{P} -Membership. By Proposition 7, it follows that ⊆-relevance is in NP^{NP} = Σ_{2}^{P}. Σ_{2}^{P} -Hardness. We transform deciding that a QBF Φ = ∃X∀Y E is in QBF_{2,∃}, where E is in 3DNF, into deciding ⊆-relevance.

Let X = {x_{1}, …, x_{m}} and Y = {y_{1}, …, y_{n}}, and consider the following LPAP P = ⟨H, Q ∪ {p}, LP, ⊧_{wf}⟩, where H = X ∪ X′ ∪ Y ∪ {w}; the logic program LP is as follows:

LP = transf(\overline{E}) ∪ \{ p ← ¬abs , p ← y_{1} ∧ ⋯ ∧ y_{n} ∧ w \} ∪
{p ← x_{i} ∧ x′_{i} , q_{i} ← x_{i} , q_{i} ← x′_{i} | i = 1 …, m}

Observe that for each S ⊆ H, LP ∪ S is stratified.

Since each q_{i} can be explained only by x_{i} or x′_{i}, it is easily seen that each solution of P must contain x_{i} or x′_{i} for i = 1, …, m. On the other hand, if a set S ⊆ H with the latter property contains both x_{i} and x′_{i} for some i, or it contains y_{1}, …, y_{n} and w, then S is a solution to P.

We claim that Φ is valid iff w is ⊆-relevant for P. ⇒. Let X1 ⊆ X such that ∀Y E is valid on X1 (that is, ∀Y E is a logical consequence of X1 ∪ { ¬x′_{i} | x_{i} ∈ X \ X1 }). As observed above, the set S_{X1} = X1 ∪ (X − X1)′ ∪ Y ∪ {w} is a solution to P. Moreover, S_{X1} is a ⊆-solution of P. To show this, assume that S ⊂ S_{X1} is a smaller solution for P. It is easily seen that without loss of generality, w ∉ S (for, the only rule in LP ∪ S in which w occurs can not be applied); moreover, S coincides on X ∪ X′ with S_{X1}. Since LP ∪ S ⊧_{wf} p, some rule must derive p. Clearly, the only one which can do so is p ← ¬abs . Hence, LP ∪ S ⊧_{wf} ¬abs, which means that the body of each rule in transf(\overline{E}) is false. Since the well-founded model M of LP ∪ S is total (as the program is stratified), it thus follows that on X1 and the valuation of the atoms in Y given by M, formula E is not true. Thus, ∀Y E is not valid on X1, which is a contradiction. Hence, an S as hypothesized does not exist, and S_{X1} is a ⊆-solution of P. Consequently, w is ⊆-relevant. ⇐. Let S be a ⊆-solution to P such that w ∈ S. Then, S contains clearly exactly one of x_{i} and x′_{i}, for each i = 1, …, m, and Y ⊆ S. Since for each Y 1 ⊆ Y, the set S_{Y 1} = (S ∩(X ∪X′)∪Y 1 is not a solution, we have that LP ∪ S_{Y 1} ⊧ ¬p, and hence LP ∪ S_{Y 1} ⊧ abs. Thus, on the set X1 = X ∩ S, the formula ∀Y E is valid, and thus Φ is valid. This proves the claim.

The result follows.

4.1.3 ≤-preference with ⊧_{wf}

Next, we consider the abductive reasoning tasks based on well-founded inference where the solutions of smallest size are acceptable. A straightforward approach for solving the reasoning problems is to calculate the size s of the smallest solutions, and then to proceed as in case there is no preference, but admitting only solutions of the size s. While this procedure is simple, the following complexity results suggest that there is hardly a substantially more efficient algorithm.

Theorem 5 Deciding if a given hypothesis is ≤-relevant for a LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is Δ_{2}^{P} [O(log n)]-complete. Δ_{2}^{P} [O(log n)]-hardness holds even if LP is stratified.

Proof. Δ_{2}^{P} [O(log n)]-Membership. Using an NP oracle, ≤-relevance of h ∈ H can be decided as follows: (1) compute the size s of a wf-≤-solution S by binary search on [0, …, n] using the oracle. (Query the oracle whether there exists an S ∈ Sol(P) such that |S| ≤ k, starting with k = n/2; this problem is in NP, cf. proof of Theorem 1.) (2) Check whether there exists an S ∈ Sol(P) such that |S| = s and h ∈ S using the oracle (again, this problem is in NP). Step (1) takes O(log |H|) oracle calls, and step (2) a single oracle call. Hence, membership in Δ_{2}^{P} [O(log n)] follows. Δ_{2}^{P} [O(log n)]-Hardness. We choose a simple reduction of the corresponding abduction problem under cautious classical inference (⊧_{cl}^{c}), i.e., inference from all models where a model must exist. As follows immediately from [19, Theorem 5.9], deciding whether h ∈ H is relevant for the ≤-solutions of an abduction problem ⟨H, M, LP, ⊧_{cl}^{c}⟩, where LP consists of definite Horn clauses (i.e. rules of the form a ← b_{1} ∧ ⋯ ∧ b_{n} , where a, b_{1}, …, b_{n} are atoms), is Δ_{2}^{P} [O(log n)]-hard.

Notice that for each S ⊆ H, LP ∪S is negation-free; therefore, the unique minimal model N_{LP ∪S} of LP ∪ S, is the well-founded model of LP ∪ S. On the other hand, since LP ∪ S is definite Horn, LP ∪ S ⊧_{cl}^{c} M iff N_{LP ∪S} ⊧ M, i.e., LP ∪ S ⊧_{wf} M. It follows that S is a solution to ⟨H, M, LP, ⊧_{cl}^{c}⟩ iff it is a solution of ⟨H, M, LP, ⊧_{wf}⟩. Consequently, deciding if h is ≤-relevant for ⟨H, M, LP, ⊧_{wf}⟩ is Δ_{2}^{P} [O(log n)]-hard.

For deciding necessity of a hypothesis, we obtain by a similar proof the same complexity result. Notice that the classes Δ_{k}^{P} [O(log n)] are closed under complement.

Theorem 6 Deciding if a given hypothesis is ≤-necessary for a LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ is Δ_{2}^{P} [O(log n)]-complete. Δ_{2}^{P} [O(log n)]-hardness holds even if LP is a stratified logic program.

We conclude this section with a remark on how the derived results can be sharpened. We focused on stratified programs for the hardness results; with proper modifications of the constructions, the same lower bounds can be derived also for positive programs, with the exception of ⊆-relevance.

Theorem 7 On the class of LPAPs P = ⟨H, M, LP, ⊧_{wf}⟩ where LP is a positive logic program, the problems (1) consistency and relevance are NP-hard; (2) necessity is co-NP-hard; and (3) ≤-relevance and ≤-necessity are Δ_{2}^{P} [O(log n)]-hard.

Proof. The program in the proof of Theorem 5 is already negation-free; this proves (3). To show (1) and (2), modify the program LP in the proof of Theorem 1 as follows: replace each occurrence of a negative literal, ¬z, in the logic program LP by z′; add rules w_{z} ← z′ , w_{z} ← z , f ← z ∧ z′ to the program; add both z and z′ to the hypotheses; and, add w_{z}, ¬f to the manifestations. It is easy to see that the solutions of the resulting LPAP P′, each of which contains exactly one of z and z′, correspond 1-1 to the solutions of P. Since the reductions from (in)consistency to necessity and relevance in Section 3.2 preserve positive programs, (1) and (2) follow.

For positive programs, ⊆-relevance is easier than for arbitrary stratified programs, since checking whether a solution S is ⊆-minimal is polynomial. This is immediate from Proposition 9 and the following fact, which is not hard to see.

Proposition 10 Let P = ⟨H, M, LP, ⊧_{wf}⟩ where LP is positive, and let S ∈ Sol(P). Then, no S′ ⊆ S exists such that S′ ∈ Sol(P) iff for every h ∈ S, S \ {h} ∉ Sol(P).

Thus, the following is derived.

Theorem 8 Deciding if a given hypothesis is ⊆-relevant for a LPAP P = ⟨H, M, LP, ⊧_{wf}⟩ where LP is positive, is NP-complete.

Proof. Membership in NP is shown along the line of proof of Proposition 7. Problem (1) there, solution verification, is polynomial by Proposition 9, and problem (2), no S′ ⊂ S exists such that S′ ∈ Sol(P), is also polynomial by Propositions 9 and 10. It follows that ⊆-relevance is in NP.

On the other hand, since consistency is by Theorem 7 NP-hard for positive programs, clearly ⊆-relevance is NP-hard for positive programs. The result follows.

4.2 Stable Cautious Reasoning

The computational complexity of the abductive problems under stable cautious reasoning will be shown to be higher than the computational complexity of the abductive problems under well-founded inference. Our proofs of the hardness results involve in general more complex translations; in particular, since stratified logic programs have a unique stable model, we will have to use unstratified programs.

Given a set Z = {z_{1}, …, z_{n}} of propositional atoms we define clos(Z) to be the following set of rules:

clos(Z) = {z_{i} ← ¬z′_{i} , z′_{i} ← ¬z_{i} | i = 1, …, n}

Let E be a Boolean CNF expression whose atoms include Z, and consider LP (E, Z) = transf(E) ∪ clos(Z). Note that LP (E, Z) is not stratified.

Intuitively, z′_{i} represents the complement of z_{i}: z_{i} is true in a stable model M of LP iff z′_{i} is false in M, and conversely. The rules in clos(Z) “give support” to the atoms in Z.

For instance, given the expression E = z_{1} ∨z_{2} ∨¬z_{3} ← from the beginning of the section, the logic program LP (E, Z) = clos({z_{1}, z_{2}, z_{3}}) ∪ transf({ z_{1} ∨ z_{2} ∨ ¬z_{3} }) is:

z_{i} ← ¬z′_{i}  (1 ≤ i ≤ 3)
z′_{i} ← ¬z_{i}  (1 ≤ i ≤ 3)
abs ← z_{3} ∧ ¬z_{1} ∧ ¬z_{2}

It is immediately recognized that there is a 1-1 correspondence between the interpretations of E and the stable models of LP, where the models of E correspond to the stable models of LP in which abs is false. The latter are: M_{1} = {z_{3}, z_{1}, z_{2}}, M_{2} = {z_{3}, z′_{1}, z_{2}}, M_{3} = {z_{3}, z_{1}, z′_{2}}, M_{4} = {z′_{3}, z_{1}, z_{2}}, M_{5} = {z′_{3}, z′_{1}, z′_{2}}, M_{6} = {z′_{3}, z′_{1}, z_{2}}, M_{7} = {z′_{3}, z_{1}, z′_{2}}. Such a correspondence can be profitably used to check the validity of QBFs. For instance, the formula ∃z_{1}∃z_{2}∃z_{3}E is valid (i.e., it is in QBF_{1,∃}) iff LP ⊧_{st}^{b} ¬abs. The formula ∀ZE is valid (i.e., it is in QBF_{1,∀} iff LP (E, Z) ⊧_{st}^{c} ¬abs.

4.2.1 No preference

Now, let us consider solution verification for LPAP s that use inference ⊧_{st}^{c}. In the light of the results from [66], it is clear that this problem is most likely not polynomial.

Proposition 11 Let P = ⟨H, M, LP, ⊧_{st}^{c}⟩ be a LPAP. Deciding if S ⊆ H fulfills S ∈ Sol(P) is D_{1}^{P}-complete.

Proof. By Proposition 3, solution verification is polynomial-time equivalent to inference of a conjunction of literals. As shown in [66], given a propositional logic program LP and atom q, deciding whether LP ⊧_{st}^{c} q is D_{1}^{P}-complete. Clearly, D_{1}^{P} is also an upper bound for cautious inference of a conjunction of literals (apart from a simple computational argument, this follows easily from the fact that D_{1}^{P} is closed under conjunction). The result follows.

Next, we consider consistency checking for LPAPs. Due to the higher complexity of solution verification, the problem resides for ⊧_{st}^{c} one level higher up in the polynomial hierarchy compared to ⊧_{wf}.

Theorem 9 To decide if Sol(P) ≠ ∅ for a given LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{2}^{P} -complete.

Proof. Σ_{2}^{P} -Membership. We guess S ⊆ H. Then, by virtue of Proposition 11, we can verify that S ∈ Sol(P) in polynomial time with two calls to an oracle for NP. Hence, the problem is in Σ_{2}^{P}. Σ_{2}^{P} -Hardness. We give a transformation from deciding Φ ∈ QBF_{2,∃}, where Φ = ∃X∀Y E, X = {x_{1}, …, x_{n}}, Y = {y_{1}, …, y_{m}}, and E is in 3DNF.

Consider the LPAP P = ⟨X, \{abs\}, LP, ⊧_{st}^{c}⟩, where LP = transf(\overline{E}) ∪ clos(Y).

For each X1 ⊆ X, there is a 1-1 correspondence between the stable models of LP ∪ X1 and the possible truth assignments for y_{1}, ⋯, y_{m} (the truth value of each x_{i} in the stable models is determined by membership in X1). A truth assignment to Y satisfies E iff abs is true in the corresponding stable model. Thus, the formula ∀Y E is valid dependent on X1, iff for each N ∈ STM(LP ∪ X1), N ⊧ abs, i.e., LP ∪ X1 ⊧_{st}^{c} abs. On the other hand, Φ is valid iff there exists an X1 ⊆ X such that ∀Y E is valid dependent on X1. Therefore, Φ is valid iff there exists an X1 ⊆ X such that LP ∪ X1 ⊧_{st}^{c} abs. In other words, Φ is valid iff there exists X1 ∈ Sol(P), i.e., Sol(P) ≠ ∅ if and only if Φ is valid.

Whence, to decide if Sol(P) ≠ ∅ for a given LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{2}^{P} -hard.

For deciding relevance, we obtain by Proposition 5 the same complexity result, and for deciding necessity, by Proposition 6 a complementary complexity result.

Theorem 10 Deciding if a given hypothesis is relevant for a LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{2}^{P} -complete.

Theorem 11 Deciding if a given hypothesis is necessary for a given LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Π_{2}^{P} -complete.

4.2.2 ⊆-preference with ⊧_{st}^{c}

Now let us determine the effect of restricting solutions to those minimal under inclusion.

As in the case of well-founded inference, we face for the relevance test an increase in complexity, which is intuitive from the more difficult problem of solution verification. In fact, we encounter a problem complete for a class of the third level of the polynomial hierarchy,

Theorem 12 Deciding if a given hypothesis is ⊆-relevant for a LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{3}^{P} -complete.

Proof. Σ_{3}^{P} -Membership. By Theorem 9, consistency is in Σ_{2}^{P}. Hence, by Proposition 7, ⊆-relevance is in NP^{Σ_{2}^{P}} = Σ_{3}^{P}. Σ_{3}^{P} -Hardness. We describe a transformation from deciding if a QBF Φ = ∃X∀Y ∃ZE, where E is in 3CNF, belongs to QBF_{3,∃}.

Let X = {x_{1}, …, x_{n_{x}}}, Y = {y_{1}, …, y_{n_{y}}}, and Z = {z_{1}, …, z_{n_{z}}}. Take atoms X′ = {x′_{1}, …, x′_{n_{x}}}, Q = {q_{1}, …, q_{n_{x}}} and w, and define a logic program LP as follows:

LP = transf(E) ∪ clos(Z) ∪ {abs ← y_{1} ∧ ⋯ ∧ y_{n_{y}} ∧ w } ∪
{abs ← x_{i} ∧ x′_{i} , q_{i} ← x_{i} , q_{i} ← x′_{i} | i = 1 …, n_{x}}.

Consider the LPAP P = ⟨H, Q ∪ {abs}, LP, ⊧_{st}^{c}⟩, where H = X ∪ X′ ∪ Y ∪ {w}.

Since each q_{i} can be explained only by x_{i} or x′_{i}, it is easily seen that each solution of P must contain x_{i} or x′_{i} for i = 1, …, n_{x}. On the other hand, each subset S ⊆ H with the latter property that contains {w, y_{1}, …, y_{n_{y}}} or {x_{i}, x′_{i}}, for some i, is a solution to P. However, a minimal solution contains either {w, y_{1}, …, y_{n_{y}}} or {x_{i}, x′_{i}} for some i, but it can not contain both.

We claim that Φ is valid iff w is ⊆-relevant for P.

Prior to the proof of the claim, suppose for the moment that n_{x} = 0. Then P would be of the form P′ = ⟨Y ∪ {w}, {abs}, LP′, ⊧_{st}^{c}⟩, where LP′ = transf(E) ∪ clos(Z) ∪ { abs ← y_{1} ∧ ⋯ ∧ y_{n_{y}} ∧ w \} is the logic program for ∃Y ∀Z\overline{E} according to the transformation in the proof of Theorem 9, augmented by the rule abs ← y_{1} ∧ ⋯ ∧ y_{n_{y}} ∧ w . Clearly, Y ∪ {w} is a solution to P′. Since ⟨Y, {abs}, transf(E) ∪ clos(Z), ⊧_{st}^{c}⟩ has, as shown in the proof of Theorem 9, a solution iff ∃Y ∀Z\overline{E} is valid, it follows that Y ∪ \{w\} is the only solution of P iff ∃Y ∀Z\overline{E} is false.

Utilizing these observations, we now proof the claim. (⇒). Let X1 ⊆ X such that ∀Y ∃ZE is valid on X1, i.e., ∃Y ∀Z\overline{E} is false. By the above consideration, S = X1 ∪ (X − X1)′ ∪ Y ∪ {w} is a solution to P. Moreover, it holds that Y ∪ {w} is the only solution of the LPAP ⟨Y ∪ {w}, {abs}, LP′ ∪ X1 ∪ (X − X1)′, ⊧_{st}^{c}⟩. Consequently, S is a ⊆-minimal solution of P, which means that w is ⊆-relevant. (⇐). Let S ∈ Sol_{⊆}(P) such that w ∈ S, and let X1 = X ∩S. Clearly, Y ⊆ S. Thus, it follows that each subset Y 1 ⊆ Y is not a solution of the LPAP ⟨Y ∪{w}, {abs}, LP′ ∪X1, ⊧_{st}^{c}⟩. Thus, ∃Y ∀Z\overline{E} is false on X1, i.e., ∀Y ∃ZE is valid on X1. This means that Φ is valid. The claim is proved.

Clearly, P is constructible in polynomial time from Φ. Thus, the result follows.

4.2.3 ≤-preference with ⊧_{st}^{c}

In the setting with inference ⊧_{wf}, we have seen that the straightforward algorithm to decide relevance and necessity, respectively, is by computing the size s of a smallest solution and proceed then as under no preference, but admitting only solutions of size s. The following results show that with respect to worst best complexity, there is most likely no significantly more efficient algorithm.

Theorem 13 Deciding if a given hypothesis is ≤-relevant for a LPAP P = ⟨H, M, LP, ⊧_{st}^{b}⟩ is Δ_{3}^{P} [O(log n)]-complete.

Proof. Δ_{3}^{P} [O(log n)]-Membership. The proof is similar to the membership part for Theorem 5, where the NP oracle for querying solutions is replaced by a Σ_{2}^{P} oracle. Δ_{3}^{P} [O(log n)]-Hardness. We show hardness by a reduction from the corresponding abduction problem under classical semantics. Theorem 4.6 in [19] states that deciding, given a set of propositional clauses T, sets H, M of propositional atoms and an atom h ∈ H, whether h belongs to any smallest (w.r.t. size) subset S ⊆ H such that T ∪ S ⊧_{P} M and T ∪ S is consistent (where ⊧_{P} is classical propositional consequence), is Δ_{3}^{P} [O(log n)]-hard. If we view T as a CNF expression and assume that abs is a logical constant for falsity, this means that, in our terminology, deciding whether a hypothesis h ∈ H is ≤-relevant for an LPAP P = ⟨H, M, transf(T), ⊧_{P} ⟩, is Δ_{3}^{P} [O(log n)]-hard, where transf(·) is the transformation from the beginning of Section 4.

Now let X = V_{P} \ {abs} be the atoms occurring in T and define

LP = transf(T) ∪ {x ← ¬x′ , x′ ← ¬x | x ∈ X} ∪ {b ← abs ∧ ¬b }

where X ∩ X′ = ∅ and b is a fresh atom. Then, the following is easily checked: For each S ⊆ H, if N is a stable model of LP ∪ S, then N ∩ V_{P} is a model of T ∪ S; note that in each stable model of LP ∪ S, both abs and b must be false. Conversely, if N is a model of T ∪ S, then N ∪ (X − N)′ is a stable model of LP. Thus, it follows that S is a solution of P′ = ⟨H, M, LP, ⊧_{st}^{c}⟩ iff S is a solution of P. Consequently, h is ≤-relevant for P iff it is ≤-relevant for P′. It follows that ≤-relevance under ⊧_{st}^{b} is Δ_{3}^{P} [O(log n)]-hard.

As in the case of inference ⊧_{wf}, we obtain the same result for necessity. (Recall that Δ_{3}^{P} [O(log n)] is closed under complement.)

Theorem 14 Deciding if a given hypothesis is ≤-necessary for a LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Δ_{3}^{P} [O(log n)]-complete.

4.3 Stable Brave Reasoning

In this section we analyze the complexity of the main abductive reasoning tasks on LPAP s that use inference ⊧_{st}^{b}. Interestingly, the complexity coincides with the one for inference ⊧_{wf}, excepting the problem of solution verification; in contrast to abduction, deduction under the brave variant of the stable model semantics is harder than well-founded deduction.

All hardness results but one will be shown as consequences of the theorems stated in Section 4.1 on well-founded semantics, by using that: (1) well-founded and stable deduction coincide on stratified programs, and (2) all hardness results for the well-founded semantics have been proven for stratified programs.

From (1), we obtain the following proposition on the equivalence of abduction using wellfounded semantics and abduction using stable brave semantics.

Proposition 12 Let P = ⟨H, M, LP, ⊧_{wf}⟩ and P′ = ⟨H, M, LP, ⊧_{st}^{b}⟩ be two LPAPs, where LP is a stratified logic program. Then, S ∈ Sol(P′) if and only if S ∈ Sol(P).

Proof. Being LP stratified, for each S ⊆ H, LP ∪ S is stratified as well, since the rules in S can not violate the stratification condition (see Section 2.1.3) as they have an empty body. As a consequence, by Proposition 2 LP ∪ S has a unique stable model, which coincides with the total well-founded model. Therefore, LP ∪ S ⊧_{st}^{b} M iff LP ∪ S ⊧_{wf} M. Whence, S ∈ Sol(P′) if and only if S ∈ Sol(P).

This relation, together with the results from Section 4.1, allows us to conclude the following.

Lemma 1 For each of the considered abductive reasoning tasks, the hardness result for LPAPs that use well-founded reasoning (cf. Section 4.1) provides a lower bound for the LPAPs that use brave stable reasoning.

For solution verification, we get higher complexity for stable brave reasoning, which is inherited from deciding stable model existence.

Proposition 13 Let P = ⟨H, M, LP, ⊧_{st}^{b}⟩ be a LPAP and S ⊆ H. Given P and S, deciding if S ∈ Sol(P) is NP-complete.

Proof. By Proposition 3, solution verification is polynomial-time equivalent to brave stable inference of a conjunction of literals from a logic program. From the results in [6, 49, 48, 72], we have that deciding whether LP ⊧_{st}^{b} q where LP is a logic program and q a literal, is NP-complete. Clearly, NP is an upper bound for brave stable inference of a conjunction of literals. This proves the result.

We observe that solution verification under inference ⊧_{st}^{b} (cf. proof above) and ⊧_{wf} differs merely by the fact that in the former case, a (stable) model N proving the solution property is guessed, while in the latter case this model (the well-founded model) is computed in polynomial time. Thus, each of the nondeterministic algorithms in the membership parts of the proofs of the complexity results for abductive reasoning tasks under ⊧_{wf} can be easily modified to a similar algorithm for ⊧_{st}^{b}, by adding to the guess of a solution S a guess for N. Since the stable model property of N can be decided in polynomial time, we obtain nondeterministic algorithms proving the same membership results for each reasoning task under ⊧_{st}^{b} as under ⊧_{wf}. Together with Lemma 1 and results in [49, 72], we thus have the following results.

Theorem 15 Let P = ⟨H, M, LP, ⊧_{st}^{b}⟩ be a given LPAP. Then,

(1) Deciding if Sol(P) ≠ ∅ is NP-complete (this follows from results of [49, 72]);

(2) Deciding if a given hypothesis is relevant for P is NP-complete;

(3) Deciding if a given hypothesis is necessary for P is co-NP-complete;

(4) Deciding if a given hypothesis is ⊆-relevant for P is Σ_{2}^{P} -complete;

(5) Deciding if a given hypothesis is ⊆-necessary for P is co-NP-complete;

(6) Deciding if a given hypothesis is ≤-relevant for P is Δ_{2}^{P} [O(log n)]-complete; and

(7) Deciding if a given hypothesis is ≤-necessary for P is Δ_{2}^{P} [O(log n)]-complete.

Proof. We provide here only membership proofs for (1), (4), and (6). For the other clauses, the claim follows from the results above. The same applies to the hardness parts. In particular, NP-hardness in part (1) follows from Proposition 4.

(1) NP-Membership. We can guess S ⊆ V_{P} and N ⊆ V_{P}, and verify in polynomial time that N is a stable model of LP ∪ S and N ⊧ M.

(4) Σ_{2}^{P} -Membership. By Proposition 13 and part (1), solution verification and consistency are in NP. Hence, by Proposition 7, ⊆-relevance is in NP^{NP} = Σ_{2}^{P}.

(6) Δ_{2}^{P} [O(log n)]-Membership. The proof is similar to the membership part of Theorem 5; we use the NP oracle to query existence of solutions S, restricted to size |S| ≤ k and |S| = s, respectively, under inference ⊧_{st}^{b} instead of ⊧_{wf}; clearly, these queries are in NP (cf. part 1).

5 Abduction from Disjunctive Logic Programs

5.1 Disjunctive Logic Programming

In this section we provide a short overview of minimal model and stable model semantics for (propositional) disjunctive logic programs [54, 62]. A comprehensive treatment of disjunctive logic programming is given in [45], to which the reader is referred for unexplained concepts.

A disjunctive logic program (DLP) is a logic program where disjunction is allowed in the head of the rules. Thus, a disjunctive logic program clause (simply clause or rule) is a formula

a_{1} ∨ ⋯ ∨ a_{n} ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬b_{k+1} ∧ ⋯ ∧ ¬b_{m}, n ≥ 1, m ≥ 0.

Total interpretations and models are defined as for (normal) logic programming (see Section 2.1), where satisfiability of the rules is extended in the obvious way.

The first semantics proposed for disjunctive logic programs has been the minimal model semantics, presented by Minker for positive (i.e., ¬-free) disjunctive logic programs [54].

A model M is minimal for a disjunctive logic program LP if no strict subset of M is a model for LP. The set of all minimal models for LP, denoted by MM(LP), has been adopted in [54] as the intended meaning of LP.

Example 8 Let P = {a ∨ b}. It is easy to verify that {a} and {b} are the minimal models of P (MM(P) = {{a}, {b}}). {a, b} is the only minimal model of the program P = {a ∨ b, b ← a, a ← b}.

Other semantics for disjunctive logic programs have been recently proposed, cf. [45]. A generally acknowledged proposal is the extension of the stable model semantics [25] to disjunctive logic programs [62].

Given a DLP LP and an interpretation I, the Gelfond-Lifschitz transform of LP with respect to I, LP^{I}, is the DLP consisting of all clauses a_{1} ∨ ⋯ ∨ a_{n} ← b_{1} ∧ ⋯ ∧ b_{k} such that

(1) a_{1} ∨ ⋯ ∨ a_{n} ← b_{1} ∧ ⋯ ∧ b_{k} ∧ ¬b_{k+1} ∧ ⋯ ∧ ¬b_{m} ∈ LP and
(2) b_{i} ∉ I, for all k < i ≤ m.

An interpretation I is called a (disjunctive) stable model of LP iff I ∈ MM(LP^{I}) [62]. The set of all stable models of LP is denoted by STM(LP).

Example 9 Let

P = a ∨ b ← c b ← ¬a ∧ ¬c a ∨ c ← ¬b.

Consider I = {b}. Then,

P^{I} = a ∨ b ← c b ← .

Check that I is a minimal model of P^{I}; thus, I is a stable model of P.

Notice that LP^{I} is ¬-free, and that LP^{I} coincides with LP if LP is ¬-free. Thus,

Proposition 14 If LP is a positive (¬-free) DLP, then STM(LP) = MM(LP), i.e. minimal and stable model semantics of LP coincide.

Both minimal model and stable model semantics provide in general a set of models as the intended meaning of a disjunctive logic program. Thus, brave and cautious reasoning are immediately extended to both semantics for DLPs. As for normal logic programs, we denote by ⊧_{st}^{b} and ⊧_{st}^{c} the inference operators of brave and cautious reasoning of stable semantics, respectively. Similarly, ⊧_{mm}^{b} and ⊧_{mm}^{c} will denote the corresponding operators for minimal model semantics.

The definition of LPAP is extended by allowing in ⟨H, M, LP, ⊧⟩ that LP is a disjunctive logic program and ⊧ an inference operator for DLP; we refer to this extended notion as disjunctive LPAP.

We conclude this section by recalling some results on the complexity of stable model semantics that will be used in the next section.

Proposition 15 ([21, 20]) Let LP be a propositional disjunctive logic program. Then,

(1) Given LP and a model M of LP, deciding whether M ∈ STM(LP) is co-NP-complete;

(2) Given LP, deciding whether it has a stable model is Σ_{2}^{P} -complete;

(3) Given LP and literals q_{1}, …, q_{k}, deciding whether LP ⊧_{st}^{b} q_{1} ∧ ⋯ ∧ q_{k} is Σ_{2}^{P} -complete (hard already for k = 1); and

(4) Given LP and literals q_{1}, …, q_{k}, deciding whether LP ⊧_{st}^{cls} q_{1} ∧ ⋯ ∧ q_{k} is Π_{2}^{P} -complete (hard already for k = 1).

5.2 Complexity Results

In the present section we study, for abduction from disjunctive logic programs, the complexity of the problems of consistency, relevance, and necessity under inference operators ⊧_{st}^{b}, ⊧_{st}^{c}, ⊧_{mm}^{b}, and ⊧_{mm}^{c}, combined with ⊆-solutions.

Several hardness results will be proven by reductions from QBFs into abduction problems; the programs of the disjunctive LPAPs will be suitable adaptations and extensions of the disjunctive program reported next (which has been first described in [20]).

Let Φ be a formula of form ∃X∀Y E, where E is a Boolean expression in 3DNF, i.e., E = D_{1} ∨ ⋯ ∨ D_{r} and each D_{i} = L_{i,1} ∧ L_{i,2} ∧ L_{i,3} is a conjunction of literals L_{i,j}; we allow here that atoms not in X = {x_{1}, …, x_{n}} and Y = {y_{1}, …, y_{m}} may occur in E. Define the following DLP LP (Φ):

x_{i} ∨ x′_{i} ←  for each i = 1, …, n
y_{j} ∨ y′_{j} ←  y_{j} ← w  y′_{j} ← w  for each j = 1, …, m
w ← y_{j} ∧ y′_{j}  for each j = 1, …, m
w ← σ(L_{k,1}) ∧ σ(L_{k,2}) ∧ σ(L_{k,3})  for each k = 1, …, r

where σ maps literals to atoms as follows:

σ(L) = \{ \begin{matrix}x′_{i} & if L = ¬x_{i} for some i = 1, …, n \\ y′_{j} & if L = ¬y_{j} for some j = 1, …, m \\ L & otherwise \end{matrix}

Intuitively, x′_{i} corresponds to ¬x_{i} and y′_{j} corresponds to ¬y_{j}.

Lemma 2 Let Φ = ∃X∀Y E be a QBF and LP (Φ) the disjunctive logic program defined above. Then, (1) STM(LP (Φ)) ≠ ∅, and (2) Φ is valid iff LP (Φ) ⊧_{st}^{b} w.

Proof. Since Φ is a QBF, all atoms in E are from X ∪ Y, and hence LP (Φ) is a positive program. Therefore, (1) follows from Proposition 14. For part (2), we outline a condensed proof that emerges from the proofs of Theorems 3.3 and 3.5 of [20].

The following facts are easy to see: Fact 1: For every model M of LP (Φ), it holds that w ∈ M iff Y ∪ Y′ ⊆ M. Fact 2: For every set X1 ⊆ X, the set M_{X1} = X1 ∪ (X \ X1)′ ∪ Y ∪ Y′ ∪ {w} is a model of LP (Φ). Fact 3: Every minimal model M of LP (Φ) satisfies M = X1∪(X \X1)′ ∪A for some X1 ⊆ X and A ⊆ Y ∪ Y′ ∪ {w}.

Now if Φ is valid, there is a subset X1 ⊆ X such that ∀Y E is valid on X1. Hence, it follows that M_{X1} is a minimal model of LP (Φ), and thus LP (Φ) ⊧_{st}^{b} w. Conversely, if LP (Φ) ⊧_{st}^{b} w, then a minimal model M exists such that w ∈ M. By Facts 1–3, it is immediate that M = M_{X1} for some X1 ⊆ X. As a consequence, ∀Y E is valid on X1, and hence Φ is valid.

Part (2) on brave reasoning and the fact that LP (Φ) is positive imply the following on cautious reasoning.

Corollary 1 The QBF Φ = ∃X∀Y E is not valid iff LP (Φ) ⊧_{st}^{c} ¬w.

Note that LP (Φ) is constructible from Φ in polynomial time. We also utilize, like in the case of nondisjunctive logic programs, generic reductions between abduction and entailment problems. It is immediate that all reductions and results in Section 3.2 hold also on disjunctive LPAPs, where nondisjunctive programs are replaced by disjunctive programs. In the sequel, when we refer to results from Section 3.2, we actually mean the generalization to disjunctive LPAPs.

5.2.1 Disjunctive stable cautious reasoning

First, we explore the complexity of solution verification. Since the complexity of inference from the stable models of a logic program increases by one level in the polynomial hierarchy if disjunctive rules are permitted, we obtain a corresponding increase in complexity for abductive solution verification.

Proposition 16 Let P = ⟨H, M, LP, ⊧_{st}^{c}⟩ be a disjunctive LPAP. Deciding if S ⊆ H fulfills S ∈ Sol(P) is D_{2}^{P}-complete.

Proof. By Proposition 3, solution verification is polynomial-time equivalent to inference LP 1 ⊧_{st}^{c} γ, where γ is a conjunction of literals. We show that deciding LP 1 ⊧_{st}^{c} γ is D_{2}^{P}- complete, which proves the result. The problem reduces to deciding whether (1) LP 1 has a stable model and (2) LP 1 ⊧_{st}^{cls} γ, which is by Proposition 15 in Σ_{2}^{P} and Π_{2}^{P}, respectively. It follows that LP 1 ⊧_{st}^{c} γ is in D_{2}^{P}. On the other hand, from Proposition 15 and Corollary 1, it is immediate that, given disjunctive logic programs LP 1 and LP 2, where LP 2 is positive, and a conjunction γ of literals, deciding whether simultaneously (1) LP 1 has a stable model and (2) LP 2 ⊧_{st}^{cls} γ is D_{2}^{P}-hard. Suppose w.l.o.g. that LP 1 has no variable in common with LP 2 and γ, and let LP = LP 1 ∪ LP 2. Then, LP ⊧_{st}^{c} γ iff (1) and (2) are true. This proves D_{2}^{P}-hardness.

Similarly, the complexity of consistency checking migrates one level up in the polynomial hierarchy.

Theorem 16 To decide if Sol(P) ≠ ∅ for a given disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{3}^{P} -complete.

Proof. Σ_{3}^{P} -Membership. We guess S ⊆ H, and verify that S ∈ Sol(P). From Proposition 16, the check that S ∈ Sol(P) can be done in polynomial time with two calls to an oracle for Σ_{2}^{P}. Hence, the problem is in Σ_{3}^{P}. Σ_{3}^{P} -Hardness. We show that the complementary problem, i.e., deciding whether Sol(P) = ∅, is hard for Π_{3}^{P}. We give a transformation from checking if a QBF Φ = ∀Z∃X∀Y E is in QBF_{3,∃} into deciding whether Sol(P) = ∅, where Z = {z_{1}, …, z_{o}}, X = {x_{1}, …, x_{n}}, and Y = {y_{1}, …, y_{m}}. Without loss of generality, we assume that E is in 3DNF, E = D_{1}∨⋯∨D_{r} and each D_{i} = L_{i,1} ∧ L_{i,2} ∧ L_{i,3} is a conjunction of literals L_{i,j} over atoms from Z ∪ X ∪ Y. Consider the disjunctive LPAP P = ⟨Z, {¬w}, LP_{1}, ⊧_{st}^{c}⟩, where LP_{1} is the disjunctive logic program LP (∃X∀Y E). Note that the rules w ← σ(L_{k,1}) ∧ σ(L_{k,2}) ∧ σ(L_{k,3}) may contain also negative literals of the form ¬z_{i}.

We will prove that Φ is valid if and only if Sol(P) = ∅.

Let Z1 ⊆ Z. Each stable model M of LP_{1} ∪ Z1 contains all and only the z_{i}’s occurring in Z1. Thus, as usual, we can identify Z1 with the truth assignment to Z which maps into true all and only the elements from Z1. From Corollary 1, it follows that Φ′ = ∃X∀Y E is false on Z1 if and only if ¬w is true in every stable model of LP_{1} ∪ Z1 (LP_{1} ∪ Z1 ⊧_{st}^{c} ¬w). Since Φ = ∀ZΦ′, we have that Φ is valid iff there does not exist Z1 ⊆ Z such that LP_{1} ∪Z1 ⊧_{st}^{c} ¬w (i.e., no Z1 is in Sol(P)). Thus, Φ is valid iff Sol(P) = ∅. As deciding if such a Φ is valid is Π_{3}^{P} -hard, deciding if Sol(P) = ∅ is Π_{3}^{P} -hard as well. As a consequence, deciding if Sol(P) ≠ ∅ is hard for the dual class Σ_{3}^{P}.

As for normal logic programs, by Proposition 5 relevance has the same complexity as consistency checking, and by Proposition 6, necessity has complementary complexity.

Theorem 17 Deciding if a given hypothesis is relevant for a disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{3}^{P} -complete.

Theorem 18 Deciding if a given hypothesis is necessary for a given disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Π_{3}^{P} -complete.

Adopting minimality with respect to inclusion as the criterion for acceptability led to an increase of the complexity of relevance testing for normal logic programs by one level of the polynomial hierarchy. The same happens in the case of disjunctive logic programs, and we end up with a problem complete for a class of the fourth level of the polynomial hierarchy.

Theorem 19 Deciding if a given hypothesis is ⊆-relevant for a disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{c}⟩ is Σ_{4}^{P} -complete.

Proof. Σ_{4}^{P} -Membership. By Theorem 16, consistency is in Σ_{3}^{P}. Hence, by Proposition 7, ⊆-relevance is in NP^{Σ_{3}^{P}} = Σ_{4}^{P}. Σ_{4}^{P} -Hardness. We describe a transformation from checking if a QBF Φ = ∃T ∀Z∃X∀Y E is in QBF_{4,∃} into deciding ⊆-relevance, where T = {t_{1}, …, t_{l}}, Z = {z_{1}, …, z_{o}}, X = {x_{1}, …, x_{n}}, and Y = {y_{1}, …, y_{m}}. We assume that E is in 3DNF, i.e., E = D_{1} ∨ ⋯ ∨ D_{r} and each D_{i} = L_{i,1} ∧ L_{i,2} ∧ L_{i,3} is a conjunction of literals L_{i,j} over atoms from T ∪ Z ∪ X ∪ Y. Consider the following logic program LP_{2}:

(g0) q ← s ∧ z_{1} ∧ … ∧ z_{o}  q ← ¬w
(g1) abs ← t_{i} ∧ t′_{i} q_{i} ← t  q_{i} ← t′_{i}  for each i = 1, …, l
(g2) x_{i} ∨ x′_{i} ←  for each i = 1, …, n
(g3) y_{j} ∨ y′_{j} ←  y_{j} ← w  y′_{j} ← w  for each j = 1, …, m
(g4) w ← y_{j} ∧ y′_{j}  for each j = 1, …, m
(g5) w ← σ(L_{k,1}) ∧ σ(L_{k,2}) ∧ σ(L_{k,3})  for each k = 1, …, r

where the rules (g2) − (g5) constitute the program LP (∃X∀Y E). Consider the disjunctive LPAP

P = ⟨Z ∪ T ∪ T′ ∪ {s}, {q, ¬abs} ∪ Q, LP_{2}, ⊧_{st}^{c}⟩,

where T′ = {t′_{1}, …, t′_{l}} and Q = {q_{1}, …, q_{l}}. We will prove that Φ is valid if and only if s is ⊆-relevant for P. (⇒). Observe first that each set S ⊆ H containing {s} ∪ Z, and such that, for each 1 ≤ i ≤ l, exactly one element from {t_{i}, t′_{i}} is in S, is a solution to P. Moreover, if S and S′ are two solutions to P, then neither S ∩ (T ∪ T′) ⊂ S′ ∩ (T ∪ T′) nor S′ ∩ (T ∪ T′) ⊂ S ∩ (T ∪ T′) holds. Since Φ is valid, there exists T 1 ⊆ T such that Φ′ = ∀Z∃X∀Y E is valid on T 1. Let S = T 1∪(T −T 1)′∪Z∪{s}. From the above observation, S is a solution to P. Moreover, since Φ′ is valid on T 1, there exists no solution to the disjunctive LPAP P′ = ⟨Z, ¬w, LP_{1}, ⊧_{st}^{c}⟩, where LP_{1} consists of the rules (g2)−(g5) (clearly, the t_{i} atoms in the rules (g5) are replaced by their truth values in T 1); this is shown by a proof similar to the one of Theorem 16. Therefore, S is a ⊆-minimal solution of P, as having T 1∪(T −T 1)′ fixed, {s}∪Z is necessary to derive q, and, from the above observations, every other solution to P necessarily differs from S on T ∪ T′. (⇐). Let S ∈ Sol_{⊆}(P) such that s ∈ S, and let T 1 = T ∩ S. Z must be contained in S, otherwise S − {s} ∈ Sol(P) which contradicts the minimality of S. Thus, it follows that each subset Z1 ⊆ Z, is not a solution of the disjunctive LPAP P′ = ⟨Z, ¬w, LP_{1}, ⊧_{st}^{c}⟩, where LP_{1} consists of the rules (g2) − (g5) (see above). Thus, from the proof of Theorem 16, Φ′ = ∀Z∃X∀Y E is valid on T 1. As a consequence, Φ is valid.

Since P is constructible in polynomial time from Φ, Σ_{4}^{P} -hardness of deciding ⊆-relevance under inference ⊧_{st}^{c} follows.

5.2.2 Disjunctive stable brave reasoning

In the case of abduction from normal logic programs, we found that the complexity under the brave variant of the stable semantics is the same as under the well-founded semantics (with one exception), and we established the results by relationships between these semantics. In the case of disjunctive programs, we can not take profit of such results. However, in all cases disjunctive rules lead for the brave variant to the same increase in complexity as for the cautious variant, namely one level up in the polynomial hierarchy.

We start by establishing this for solution verification.

Proposition 17 Let P = ⟨H, M, LP, ⊧_{st}^{b}⟩ be a disjunctive LPAP and S ⊆ H. Given P and S, deciding if S ∈ Sol(P) is Σ_{2}^{P} -complete.

Proof. By Proposition 3, solution verification is polynomial-time equivalent to inference. Thus, the result immediately follows from Proposition 15.3.

One can show that consistency checking is precisely as complex as solution verification analogously as done in the case of normal logic programs in Section 4.3.

Theorem 20 To decide if Sol(P) ≠ ∅ for a given disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{b}⟩ is Σ_{2}^{P} -complete.

Proof. Σ_{2}^{P} -Membership: Guess S ⊆ V_{P} and N ⊆ V_{P}, and verify that: (1) N is a stable model of LP ∪ S, and, (2) N ⊧ M. By virtue of Proposition 15, (1) is done by a single call to a co-NP oracle; (2) can be simply checked in polynomial time. Hence, the problem lies in Σ_{2}^{P}. Hardness for this class follows from Propositions 4 and 15.

For necessity and relevance, we get as in the case of normal logic programs by Propositions 6 and 5 the same result as for (in)consistency checking.

Theorem 21 Deciding if a given hypothesis is relevant for a given disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{b}⟩ is Σ_{2}^{P} -complete.

Theorem 22 Deciding if a given hypothesis is necessary for a given disjunctive LPAPP= ⟨H, M, LP, ⊧_{st}^{b}⟩ is Π_{2}^{P} -complete.

Finally, we consider the effect of restricting the set of solutions to those minimal with respect to inclusion. Again, we find a complexity increase by one level in the polynomial hierarchy compared to normal logic programs.

Theorem 23 Deciding if a given hypothesis is ⊆-relevant for a given disjunctive LPAP P = ⟨H, M, LP, ⊧_{st}^{b}⟩ is Σ_{3}^{P} -complete.

Proof. Σ_{3}^{P} -Membership. By Theorem 20 consistency is in Σ_{2}^{P}. Hence, by Proposition 7, ⊆-relevance is in NP^{Σ_{2}^{P}} = Σ_{3}^{P}. Σ_{3}^{P} -Hardness. We demonstrate that the complementary problem, i.e., ⊆-dispensability, is hard for Π_{3}^{P}. We provide a transformation from checking if a QBF Φ = ∀Z∃X∀Y E is in QBF_{3,∃}, where Z = {z_{1}, …, z_{o}}, X = {x_{1}, …, x_{n}}, and Y = {y_{1}, …, y_{m}}. As above, we assume that E is in 3DNF, E = D_{1} ∨ ⋯ ∨ D_{r} and each D_{i} = L_{i,1} ∧ L_{i,2} ∧ L_{i,3} is a conjunction of literals L_{i,j} over atoms from Z ∪ X ∪ Y. Consider the disjunctive LPAP P = ⟨Z ∪ {w}, { w}, LP_{1}, ⊧_{st}^{b}⟩, where LP_{1} is the disjunctive logic program LP (∃X∀Y E), which has been already used in the proof of Theorem 16.

We claim that Φ is valid if and only if w is ⊆-dispensable for P.

Given Z1 ⊆ Z, we can identify Z1 with the truth assignment to Z which maps into true all and only the elements from Z1. From Lemma 2, it follows that Φ′ = ∃X∀Y E is true on Z1 if and only if LP_{1} ∪ Z1 ⊧_{st}^{b} w. Since Φ = ∀ZΦ′, we have that Φ is valid iff ∀Z1 ⊆ Z, LP_{1} ∪ Z1 ⊧_{st}^{b} w. Therefore, Φ is valid iff w is ⊆-dispensable for P. The claim is proven. Thus, ⊆-dispensability under inference ⊧_{st}^{c} is Π_{3}^{P} -hard, and, consequently, ⊆-relevance under ⊧_{st}^{c} is hard for the dual class Σ_{3}^{P}.

5.2.3 Minimal model semantics

Our proofs of the results on disjunctive abduction problems using stable models allow to establish similar complexity results for abduction based on minimal models. We denote by ⊧_{mm}^{b} and ⊧_{mm}^{c} brave and cautious inference from the minimal models of a disjunctive logic program, respectively. Notice that any disjunctive logic program has some minimal model, and hence cautious inference as used here and classical cautious inference coincide.

One can easily check that the upper complexity bounds for disjunctive stable models carry over to minimal models as well. Moreover, since ⊧_{mm}^{c} resorts to classical cautious minimal model inference, for deciding whether a set S is a solution for a disjunctive LPAP ⟨H, M, LP, ⊧_{mm}^{c}⟩, we get even a smaller bound of Π_{2}^{P} compared to D_{2}^{P} for the same problem using stable models.

To derive the matching hardness results in all cases but the mentioned exception, it is sufficient to modify the abduction problems in the proofs of the results on abduction using disjunctive stable models such that the programs are positive. (Recall that the stable models of a positive program coincide with its minimal models.)

In the proofs of Proposition 17 and Theorem 20, respectively, we can assume that the disjunctive programs are positive; thus, these constructions work also when minimal models are used. In all the other proofs, we modify the constructed programs by eliminating negative literals as follows.

(1) Elimination of literals ¬z_{i}: Replace each occurrence of ¬z_{i} in a rule by z′_{i}; add rules r_{i} ← z_{i} and r_{i} ← z′_{i} to the program (r_{i} is a new atom); add z′_{i} to the set H, and add r_{i} to the set M.

(2) Elimination of ¬w: Replace the rule q ← ¬w by q ∨q′ ← w (q′ is a new atom); remove q from the set M and add ¬q′ instead.

The programs in the abduction problems resulting from these steps are positive. Informally, step (1) introduces an atom z′_{i} for the complement of z_{i}, and at least one of both must appear in each solution. If both z_{i} and z′_{i} appear in a solution, then some of them can be discarded and the resulting set is another solution of the abduction problem. Step (2) hinges on the fact that if q, which must be provable from the stable models of the program augmented by the solution, has to be derived in a stable model from the rule q ← ¬w , then w must be false in it, and thus, given the replacement clause, q′ will be false in a stable model; if q is derived from another clause, then clearly q′ will be false.

Formally, one can show that in each case the employed reasoning task has the same answer on the original problem and the modified problem. Thus, the hardness results for abduction using disjunctive stable models carry over to the minimal model semantics. Proving Π_{2}^{P} - hardness of solution verification for LPAPs with inference ⊧_{st}^{c} is easy. Thus, we have the following result.

Theorem 24 The complexity of each of the reasoning tasks from above (consistency, relevance, necessity etc) on disjunctive LPAPs using inference ⊧_{mm}^{x}, where x ∈ {b, c}, coincides with the complexity of the same reasoning task on disjunctive LPAPs using inference ⊧_{st}^{x}, with the exception of solution verification for ⊧_{mm}^{c}, which is Π_{2}^{P} -complete. Moreover, hardness holds in each case for the class of positive programs.

Note that minimal model inference is, contrary to well-founded and stable model inference, independent of the syntactical form of program clauses. For example, the clauses a ← ¬b, b ← ¬a, and a ∨ b all have the same consequences under minimal model inference; this is obviously not true for well-founded and stable model inference. A consequence of syntax independence is the following result.

Theorem 25 For the abductive reasoning tasks above (solution verification, consistency, relevance etc) on disjunctive LPAPs using ⊧_{mm}^{x} inference, x ∈ {b, c}, hardness holds already on instances with normal (i.e., nondisjunctive) programs.

Proof. Observe that atoms in the head of a disjunctive rule can be negated and moved to the body without a change in the classical models of the rule. Thus, under inference ⊧_{mm}^{x}, x ∈ {b, c}, each disjunctive program can be efficiently rewritten to an equivalent normal program. By the results above, this proves the theorem.

6 Abduction from Function-free First Order Programs

In this section, we generalize the abduction model to the (function-free) first order case, i.e., logic programs with variables (also called datalog programs), and we discuss the complexity of this case.

We start by briefly recalling syntax and semantics of programs with variables.

A function-free first order rule is a formula

A ← B_{1} ∧ ⋯ ∧ B_{m} ∧ ¬C_{1} ∧ ⋯ ∧ ¬C_{l}, 1 ≤ n, 0 ≤ m, l, (2)

such that each A, B_{i}, and C_{j} is an atom p(t_{1}, …, t_{a}) of an a-ary predicate p, a ≥ 0, where each term t_{1}, … t_{a}, is either a variable or a constant; a function-free logic program is a finite set of such rules. Note that a function-free logic program resorts to a propositional program if all predicates in its rules are 0-ary.

The semantics of a function-free logic program LP is defined by first instantiating LP over the sets of constants that occur in LP and by then applying to the grounded program, which is regarded as a propositional program, the definitions given in the propositional case. Thus, the definitions of well-founded and stable model semantics given in Sections 2.1 and 5.1 are generalized to function-free logic programs.

Now, we generalize the concepts of logic programming abduction problem and solution.

Definition 4 A function-free logic programming abduction problem (FLPAP) P consists of a tuple ⟨H, M, LP, ⊧⟩, where H is a finite set of predicates called hypotheses, M is a finite set of ground literals called manifestations, LP is a function-free logic program, and ⊧ is an inference operator.

Let P = ⟨H, M, LP, ⊧⟩ be a FLPAP, and let S be a subset of the ground instantiation of the predicates in H with the constants from LP ∪ M. Then, S is a solution (or explanation) to P iff LP ∪ S ⊧ M.

The set of all solutions to P is denoted by Sol(P).

The properties of relevance and necessity of a ground atom g(a), g ∈ H, for P are defined analogous to the propositional case, and the computational problems relevance and necessity adapted accordingly.

Example 10 Consider the following logic program LP, describing a game where each player is identified by its position a a player wins if he can move and its opponent has no moves – this program has been used by Kolaitis to prove that some interesting queries can not be expressed by stratified programs [40].

win(X) ← move(X, Y) ∧ ¬win(Y) .

The legal moves are represented by facts defining the predicate move. Let P be the LPAP ⟨H, M, LP, ⊧_{wf}⟩, where LP is the program above, the set of abducible predicates is H = {move, player}, and the set of manifestation is M = {player(a), player(b), player(c), win(a)}. The abduction problem P asks for configurations of the game (i.e., set of moves), where a, b, and c are the players and a is the winner; each abductive solution of P identifies such a configuration. For instance, S_{1} = {move(c, a), move(a, b), player(a), player(b), player(c) } is a solution, while S_{2} = S_{1} ∪ {move(b, c)} is not.

Notice that under classical inference, S_{1} is not a solution, and does classical inference leads to different conclusions. However, S_{1} is a solution if we consider the completion of LP. To highlight the difference between ⊧_{wf} and classical inference from the completion, consider S_{3} = {move(a, b), move(a, c), move(b, c), move(c, b)}. Then, S_{3} is not a solution under ⊧_{wf}, but under classical inference from the completion of LP.

Notice that in the above definition, the hypotheses are predicates rather than ground facts. One might argue that, in certain cases, it would be more appropriate to have explicitly a set of abducible ground facts from which a solution must be formed, e.g., if a certain ground fact should not appear in a solution. Technically, this more restricted form of abduction can be easily emulated in our framework. For each abducible ground fact p(a), introduce a new 0-ary predicate (propositional letter) h_{p(a)}; put h_{p(a)} into the abducible predicates H, and add to the program LP the rule p(a) ← h_{p(a)} . Then, for all considered logic programming semantics (as well as for any other reasonable semantics), the solutions of the obtained abduction problem (which consist of subsets of H), correspond in the obvious way to the solutions from the set of abducible ground facts.

When we do abduction from a function-free program, two interesting issues emerge concerning the computational complexity. The first one is answering the questions for abduction problems restricted to instances where the rules with nonempty body are fixed (i.e., the hypotheses, the manifestations, and the elementary facts in the program may change and may be regarded as “data”). This restriction corresponds to abductive reasoning with a static background knowledge on the relationship between elementary facts. We refer to the complexity of this problem as the data complexity of abduction from function-free programs;

The second issue is answering the questions we described in Section 3 (relevance, necessity, etc.) for an arbitrary given abduction problem (i.e., also the background knowledge may change); we refer to this as combined complexity. The notions of data and combined complexity have been introduced by Vardi [78] in the context of query languages.

Concerning the data complexity, we observe the following.

Proposition 18 For each type of considered reasoning problem on a FLPAP P = ⟨H, M, LP, ⊧⟩, the complexity of the same type of reasoning problem on a propositional LPAP is an upper bound for data complexity.

Proof. Let B denote those predicates which occur in some rule of LP with nonempty body. A reasoning problem on P can be efficiently transformed into an equivalent reasoning problem P′ of the same type as follows.

Let LP 1 be the instantiation of LP ∪ M, and let for each ground atom p(a) be x_{p(a)} a new propositional atom. Now, proceed as follows: Remove from H all predicates that are not in B, remove from LP all rules with empty body, and remove from M all literals that involve predicates not in B; let H1, M1, and LP 1 denote the results of these operations, respectively. Then, add for each literal p(a) (resp. ¬p(a)) from M that has been removed to M1 the literal x_{p(a)} (resp. ¬x_{p(a)}); if the rule p(a) ← is in LP_{g}, then add x_{p(a)} ← to LP 1, and if p ∈ H, then add x_{p(a)} to H1. Finally, if the considered reasoning task involves a ground hypothesis g(a) (as in relevance etc.) such that g occurs not in B, then replace g(a) with x_{g(a)} and add x_{g(a)} to H_{1}, and add for each constant a in LP_{g} to LP 1 the fact u(a) ← , where u is a fresh unary predicate. Let H2, M2, and LP 2 be the result of these steps. Basically, we have replaced ground atoms that do not interfere with proper rules of LP by propositional atoms, and removed hypotheses and nonground facts that are not needed to answer the reasoning task. Notice that in LP 2 ∪ M2 the same constants occur as in LP ∪ M.

It holds that the reasoning problem (with possibly modified ground hypothesis) on P′ = ⟨H2, M2, LP 2, ⊧⟩ yields the same answer as the reasoning problem on P.

For fixed rules with nonempty head in LP, the size of the instantiation of LP 2 ∪ M2 over its constants is polynomial, as is the size of the instantiation of H2 over these constants. Hence, it follows that the complexity of each type of reasoning problem on the first order LPAP P is bounded by the complexity of the same type of reasoning problem in the propositional case.

On the other hand, we have that complexity in the propositional case also provides a matching lower bound for the data complexity. To establish this, we describe how hard instances of the problems in the propositional case can be reduced to data complexity in the first order case.

The key observation is that in the propositional case, all the problems from above remain as hard as in the general case if the program of the LPAP contains a rule true ← and each other rule in the program is of the form

a ← b_{1} ∧ ⋯ ∧ b_{i} ∧ ¬b_{i+1} ∧ ⋯ ∧ ¬b_{3}, for some i ∈ {0, …, 3}; (3) we call such a LPAP 3-bounded. This can be established as each positive rule a ← b_{1} ∧ b_{2} ∧ b_{3} ∧ ⋯ ∧ b_{n} can be equivalently replaced by two rules a ← c ∧ b_{3} ∧ ⋯ ∧ b_{n} and c ← b_{1} ∧ b_{2} , and true can be used to augment rule bodies with less than three literals; notice that in all hardness proofs above, negative literals occur only in rules with at most three literals in the body.

For each 3-bounded LPAP P = ⟨H, M, LP, ⊧⟩ we define a FLPAP P_{fo} = ⟨{s}, M′, LP′, ⊧⟩ as follows. The predicate s(X) intuitively means that X belongs to the solution of P. In the program LP′, the constants are the propositional atoms V_{P} of P. Each rule of the form (3) is encoded by the atom r_{i}(a, b_{1}, b_{2}, b_{3}), where i ∈ {0, …, 3} is the number of positive literals b_{1}, …, b_{i} in the body. The rules of LP′ are the following:

(1) t(true) ← ; (t(X) intuitively means that X is true)

(2) t(X) ← s(X) ;

(3) t(X_{0}) ← t(X_{1}) ∧ ⋯ ∧ t(X_{i}) ∧ ¬t(X_{i+1}) ∧ ⋯ ∧ ¬t(X_{3}) ∧ r_{i}(X_{0}, X_{1}, X_{2}, X_{3}), for each i = 0, …, 3; and

(4) r_{i}(a, b_{1}, …, b_{3}) ← , such that a ← b_{1} ∧ ⋯ ∧ b_{i} ∧ ¬b_{i+1} ∧ ⋯ ∧ ¬b_{3} occurs in LP.

The set of manifestations is M′ = {t(a)|a ∈ M} ∪ {¬t(a), ¬s(b)|¬a ∈ M, b ∈ V_{P} − H}.

Example 11 Consider the LPAP = ⟨{b, d}, {a, ¬c}, {a ← b ∧ ¬d , ⊧_{wf}⟩. The 3-bounded LPAP P = ⟨{b, d}, {a, ¬c}, {true ← , a ← true ∧ b ∧ ¬d , ⊧_{wf}}⟩ has the same solutions; in fact it has the unique solution {b}. The components LP′ and M′ in the FLPAP P_{fo} are as follows. Besides the rules (1)–(3), LP′ contains only the fact r_{2}(a, true, b, d) ← . The set V_{P} of atoms in P is {a, b, c, d, true}; hence, M′ = {t(a), ¬t(c), ¬s(a), ¬s(c), ¬s(true)}. The reader may verify that {s(b)} is the unique solution to P_{fo}.

The following property of P_{fo} is not difficult to establish.

Lemma 3 Let P be a 3-bounded LPAP with inference ⊧_{wf}, ⊧_{st}^{b}, or ⊧_{st}^{c}, and let P_{fo} be the FLPAP as defined above. Then, Sol(P) = {{a_{1}, …, a_{n}}|{s(a_{1}), …, s(a_{n})} ∈ Sol(P_{fo})}.

Notice that P_{fo} can be constructed from P in logarithmic space, and that the rules in LP′ with nonempty body are the same for every P. Thus, from Proposition 18 and Lemma 3 we obtain the following result.

Theorem 26 For any reasoning task on any type of abduction problem considered above, the data complexity of the first-order case coincides with the complexity in the propositional case.

We remark that the same complexity results can be shown for the restriction to instances where everything except the manifestations is kept fixed.

As with many logical query languages, the combined complexity is much higher than the data complexity. The exponential analogue of each complexity class –EXP for P, NEXP for NP, NEXP^{NP} for Σ_{2}^{P} etc– is an immediate upper bound, and is also in each case a matching lower bound. For the case with polynomial data complexity, this follows from folklore results about datalog. Note that the exponential analogue of Δ_{k+1}^{P}[O(log n)] is EXP^{Σ_{k}^{P}} [P ol(n)], i.e., exponential time with a polynomial number of calls to an Σ_{k}^{P} oracle; this class coincides with PSPACE^{Σ_{k}^{P}}, i.e., polynomial space with an oracle for Σ_{k}^{P}, if the oracle queries may be arbitrarily large [27]. A detailed analysis of the combined complexity of logic programming abduction is carried out in [27].

Disjunctive propositional logic programs can be generalized to function-free logic programs in the same way as normal logic programs; from above, it should be clear how syntax and semantics of such programs are defined. Moreover, it is straightforward to extend the definition of function-free logic program abduction problem to allow for disjunctive function-free programs; we omit the details.

As in the latter case, one can show that the results of the reasoning tasks for the disjunctive propositional case carry over to the data complexity of the disjunctive function-free case. The arguments for showing these to be upper bounds are similar, and the proof of the matching lower bounds is based on a proper modification of the above described translation of abduction from propositional programs into abduction from function-free first order programs. Similarly, the combined complexity of disjunctive abduction problems is exponentially higher than the data complexity.

7 Related Work

In this section we briefly overview some works on abductive logic programming.

The best known definition of abductive logic programming is due to Kakas and Mancarella. In [37], they define abduction from (normal) logic programs under the brave modality of the stable model semantics; integrity constraints can also be imposed on the solutions. In our framework, their proposal can be represented by LPAPs of the form ⟨H, M, LP, ⊧_{st}^{b}⟩, where LP is a logic program (integrity constraints can be simulated as shown in Section 3). Thus, the various abductive problems for [37] have exactly the computational complexity determined in Section 4.3.

Console, Theseider Dupré and Torasso in [14] analyze abductive problems ⟨H, M, LP, ⊧⟩ where LP is a hierarchical (i.e., non recursive) program and ⊧ is the entailment operator based on Clark’s program completion.

The relation of abduction to negation as failure has been investigated by Eshghi and Kowalski [22], Inoue [29], and Iwayama and Satoh [32], respectively. Under some syntactic conditions, a 1-1 correspondence between the solutions of an abductive problem and the answer sets of an extended logic program obtained from it has been proven.

In a recent work [4], Baral and Gelfond define a notion of entailment for abductive logic programs. In some sense their approach is similar to LPAPs of the form ⟨H, M, LP, ⊧_{st}^{c}⟩, but they impose stronger conditions.

An important bunch of work on abductive logic programming concerns the definition of abductive procedures, which compute an abductive explanation of a given manifestation [22, 35, 32, 70, 15, 17, 7].

The seminal work in this area is due to Eshghi and Kowalski [22], who consider abduction based on stable model semantics and provide a proof procedure to compute an abductive solution. This procedure has been then extended by Kakas and Mancarella to manipulate arbitrary abducibles. Both [22] and [35] procedures guarantee correctness only for callconsistent logic programs. In [70], the Sato and Iwayama give an abductive procedure which is correct for general logic programs provided that consistency (i.e., the existence of an abductive solution) is guaranteed. Other abductive procedures [15, 17, 7] consider semantics different from stable models (like, e.g., the completion semantics [13]) on the logic program.

Our work presents some relationships to the papers on abductive procedures. For instance, the use of metalevel constraints, adopted in [22] (on the demo predicate) to eliminate negation from the logic program, could be avoided by utilizing a technique similar to that shown in Section 5.2.3.

Moreover, in our framework most abductive procedures can be seen as a method to check the existence of solutions (i.e., Sol(P) ≠ ∅) of a LPAP P = ⟨H, M, LP, ⊧_{st}^{b}⟩, where LP is a normal (non-disjunctive) logic program. From Theorem 15, this problem is NP-complete. As a consequence, from one hand we derive that no abductive procedure may (in the worst case) terminate in polynomial time (unless P = NP). On the other hand, this result indicates that an “optimal” abductive procedure can be implemented by a “flat” backtracking algorithm. (For an extended discussion on backtracking algorithms, see Section 8.) Unfortunately, even if most abductive procedures are based on backtracking, they usually consist of two mutually recursive functions; it is thus difficult to state whether they comply the above mentioned upper complexity bound.

Critical overviews of several approaches to abductive logic programming have been given by Kakas, Kowalski and Toni [34] and by Inoue [30].

To our knowledge, complexity aspects of abductive logic programming have been less addressed than semantical aspects. In [19] Eiter and Gottlob present a detailed analysis of the complexity of abduction from classical propositional theories, which has also been discussed for restricted cases by Selman and Levesque [74], Bylander [8], and Friedrich et al. [24], who focussed on Horn and definite Horn theories and the ⊆-minimality preference criterion. In this context, Eshghi has identified in [23] a subclass of Horn theories for which finding a ⊆-minimal solution is tractable.

The results of [19] and this paper show that abduction from logic programs has complexity quite different than abduction from classical theories. Notice that in the abductive framework of [19], the inference operator used is ⊧_{P}, i.e., classical logical consequence; moreover, the manifestations are there restricted to propositional atoms. For a comparison with the results of this paper, we consider ⊧_{st}^{c} inference, since it corresponds in nature to ⊧_{P}, and omit the other inference operators ⊧_{wf}, ⊧_{st}^{b} considered here.

The results shows that in the general case (clausal theories resp. disjunctive logic programs), logic programming abduction is for each reasoning task harder (at least Σ_{3}^{P} /Π_{3}^{P} -hard) than classical abduction (which is Σ_{2}^{P} /Π_{2}^{P} -complete) and can get twice as hard (Σ_{4}^{P} -complete for ⊆-relevance). In classical abduction, relevance and necessity have complementary complexity (Σ_{2}^{P} -complete resp. Π_{2}^{P} -complete), and ⊆-minimality has no effect on the complexity. In logic programming abduction, however, ⊆-minimality does affect relevance, and leads to an increase in the complexity by one level of the polynomial hierarchy.

In [19], also classical abduction from definite Horn theories has been studied, which correspond 1-1 to Horn programs. However, due to different possible sets of manifestations in the frameworks, the results from [19] do not carry over automatically to the framework considered here; in fact, several corresponding reasoning tasks have different complexity. In particular, consistency, relevance, necessity and ⊆-necessity in the framework of [19] are polynomial, while they are NP-complete in the framework of this paper. Hence, the results of the present paper show as a byproduct that the slight generalization of the framework in [19] by allowing also negative literals as manifestations causes intractability for a number of tractable abductive reasoning tasks.

Abduction from normal logic programs and first-order programs has no corresponding counterpart in [19], and thus we can not compare respective results.

Sakama and Inoue have investigated the semantics and complexity of abductive logic programming in [31, 68]. They determined in [31] the complexity of the existence of abductive solutions on disjunctive programs for the particular case where the inference operator is ⊧_{st}^{b} (stable brave), and showed that the problem is Σ_{2}^{P} -complete. The NP-completeness result for the same problem for normal logic programs is contributed in [68] to [29, 32].

In [68], the authors also consider abduction from logic programs under the possible model semantics [67, 69]. In particular, they show that existence of an abductive solution from a disjunctive logic program is NP-complete under this semantics. Thus, from the computational side, as with deduction [68, 20], the possible model semantics is more attractive than the disjunctive stable model semantics.

Even the effective computation of abductive explanation has been addressed in several works [17, 15, 22, 32, 38], where suitable extensions of the SLDNF procedure have been designed for abduction (these procedures return an abductive explanation of the given query).

Finally, the use of abductive logic programming for dealing with incomplete information has been discussed by Denecker and De Schreye [16] and by Baral and Gelfond [4].

For related complexity results in the area of logic programming and nonmonotonicreasoning, cf. [11, 71, 10, 73]. The complexity of abduction in a set-covering based rather than logic-based framework has been analyzed in [9], where polynomial and NP-complete abductive problems are discussed.

Most recently, our work in this paper has been complemented by complexity results for abduction from logic programs in the presence of functions [47].

8 Conclusion

Abduction from logic programs has become a topic of growing interest recently. We have described in this paper a basic framework of abduction from logic programs, and we have performed a detailed study of the computational complexity of the main decisional problems that emerge in abductive reasoning (consistency, relevance of a hypothesis, and necessity of a hypothesis). The analysis considers the most acknowledged proposals for the semantics of logic programs, namely the well-founded semantics and the stable model semantics (in the usual variants of brave and cautious inference), and the stable as well as the minimal model semantics for disjunctive programs. Moreover, it took into account commonly applied criteria for reducing the space of all solutions by means of a preference (⪯) to those which are minimal with respect to inclusion (⊆) and cardinality (≤), respectively.

The complexity results for the case of propositional logic programs are summarized in Tables 1–6. They cover the lower end of the polynomial hierarchy, refined by classes Δ_{k}^{P} [O(log n)], up to Σ_{4}^{P}. Each entry represents completeness for the respective class; in particular, P means logspace-completeness for P. (Notice that all polynomial time transformations in this paper are computable in logarithmic space; in fact, all results can be proven under logspace-reductions as well).

The results reflect the conceptual complexity of combining the different common semantics and solution preference criteria. They show that abduction from logic programming, a topic of increasing interest, provides a rich variety of complete problems for a number of slots within the polynomial hierarchy. This gives support to the original belief that the polynomial hierarchy would be useful for classifying computational problems, cf. [75].

Briefly, the following conclusions can be drawn. Abduction from logic programs has the same complexity for well-founded inference (⊧_{wf}) and the brave variant of stable inference (⊧_{st}^{b}), excepting the verification of a given solution, which is polynomial under the former and NP-complete under the latter. Notice that the hardness results for well-founded inference hold for stratified programs and for negation-free programs (i.e., Horn programs) as well, with the exception of deciding ⊆-relevance, which is “only” NP-complete for Horn programs. Since the semantics of Horn programs is clear, this shows that, loosely speaking, the wellfounded semantics does mostly not increase the inherent complexity of abduction from logic programs, which makes it attractive.

For the appropriate cautious variant of stable inference (cautious inference ⊧_{st}^{c}), the complexity is in each case precisely one level higher in the polynomial hierarchy than for ⊧_{st}^{b}, again excepting solution verification, which has marginally higher complexity; this is noticeable since usually, the brave and the cautious variant of a reasoning task in a nonmonotonic formalism are of dual complexity (typically Σ_{2}^{P} and Π_{2}^{P}). Furthermore, allowing for disjunctive rules leads to another increase by one level in the polynomial hierarchy. This is explained by the fact that testing the stable model property migrates from polynomial time to co-NP-completeness. The effect of the solution preference criteria on the complexity meets the intuitive expectations. Imposing subset-minimality (⊆) leads in general to an increase by a full level in the polynomial hierarchy, while minimum cardinality (≤) leads merely to a minor increase, which can be interpreted as the need of computing the size of a smallest solution for solving the problem. It is worth mentioning that for abduction using classical semantics, imposing ⊆ does not lead to a complexity increase, cf. [19].

All results for disjunctive logic programming abduction in Tables 4–6 remain valid for the restriction to positive disjunctive logic programs, where the stable semantics coincides with the minimal model semantics. The results for the case of propositional programs carry over to the data complexity in the case of function-free first order logic programs. The combined complexity, which was not dealt with here in detail, parallels the data complexity with the corresponding exponential analogues (EXP for P, NEXP for NP etc); a treatment thereof appears in [27].

LPAP P = ⟨H, M, LP, ⊧⟩  Deciding S ∈ Sol(P) Deciding Sol(P) ≠ ∅
well-founded inference (⊧_{wf})  P  NP^{[74]}
stable brave inference (⊧_{st}^{b})  NP  NP^{[29, 32]}
stable cautious inference (⊧_{st}^{c})  D_{1}^{P}  Σ_{2}^{P}

Table 1: Complexity of solution verification and consistency checking

Logic Programming Abduction  Deciding whether h ∈ H is ⪯-relevant for P
LPAP P = ⟨H, M, LP, ⊧⟩  = (no preference)  ⊆  ≤
well-founded inference (⊧_{wf})  NP  Σ_{2}^{P}  Δ_{2}^{P}[O(log n)]
stable brave inference (⊧_{st}^{b})  NP  Σ_{2}^{P}  Δ_{2}^{P}[O(log n)]
stable cautious inference (⊧_{st}^{c})  Σ_{2}^{P}  Σ_{3}^{P}  Δ_{3}^{P}[O(log n)]

Table 2: Complexity of deciding relevance

Logic Programming Abduction  Deciding whether h ∈ H is ⪯-necessary for P
LPAP P = ⟨H, M, LP, ⊧⟩  = (no preference)  ⊆  ≤
well-founded inference (⊧_{wf})  co-NP  co-NP  Δ_{2}^{P}[O(log n)]
stable brave inference (⊧_{st}^{b})  co-NP  co-NP  Δ_{2}^{P}[O(log n)]
stable cautious inference (⊧_{st}^{c})  Π_{2}^{P}  Π_{2}^{P}  Δ_{3}^{P}[O(log n)]

Table 3: Complexity of deciding necessity

Disj. LPAP P = ⟨H, M, LP, ⊧⟩ Deciding S ∈ Sol(P) Deciding Sol(P) ≠ ∅
stable brave inference (⊧_{st}^{b})  Σ_{2}^{P}  Σ_{2}^{P} ^{[31]}
stable cautious inference (⊧_{st}^{c})  D_{2}^{P}  Σ_{3}^{P}

Table 4: Complexity of solution verification and consistency for disjunctive LPAPs

Disj. Logic Programming Abduction Deciding whether h ∈ H is ⪯-relevant for P
Disj. LPAP P = ⟨H, M, LP, ⊧⟩  = (no preference)  ⊆
stable brave inference (⊧_{st}^{b})  Σ_{2}^{P}  Σ_{3}^{P}
stable cautious inference (⊧_{st}^{c})  Σ_{3}^{P}  Σ_{4}^{P}

Table 5: Complexity of deciding relevance for disjunctive LPAPs

Disj. Logic Programming Abduction Deciding whether h ∈ H is ⪯-necessary for P
Disj. LPAP P = ⟨H, M, LP, ⊧⟩  = (no preference)  ⊆
stable brave inference (⊧_{st}^{b})  Π_{2}^{P}  Π_{2}^{P}
stable cautious inference (⊧_{st}^{c})  Π_{3}^{P}  Π_{3}^{P}

Table 6: Complexity of deciding necessity for disjunctive LPAPs

Our complexity results have the following impact on the design of algorithms. First of all, they provide a complete picture of efficient (polynomial time) intertranslatability between different reasoning tasks, and tell us which algorithms for specific abductive reasoning tasks can also be used to solve other abductive reasoning tasks, by applying an appropriate transformation of the input. Several efficient transformations are given in Secion 3.2.

Suppose now we want to implement an inference engine that is capable of performing a certain abductive reasoning task.

Consider a reasoning task at the first level of the polynomial hierarchy. If the problem is NP-complete, then we can implement a “flat” backtracking algorithm. For example, in case of stable model inference, Saccà’s backtracking fixpoint procedure [65, 43] can be suitably adapted. Optimization techniques may be applied to cut down branches in the computation tree, but if the algorithm should work on all instances, it is unrealistic that we obtain a polynomial algorithm. Furthermore, from the general nature of NP-complete problems, we must expect to put some analytical and programming effort in order to obtain a feasible algorithm for a reasonably large class of instances. For the co-NP-complete reasoning tasks, we obtain may use backtracking algorithms that solve the complementary problem. Note that for the NP-complete reasoning tasks (but not for the co-NP-complete), randomized local search techniques [39, 42] could be applied that lead to success with high probability.

For Δ_{2}^{P} [O(log n)]-complete problems, a combination of binary search and flat backtracking may be used, following the scheme in the proof of Theorem 5. First, the size of a smallest solution is computed, and then only solution candidates of this size are considered. The backtracking part solves the oracle queries.

Next suppose we want to design an algorithm for a reasoning task at the second level, e.g. for a Σ_{2}^{P} -complete one. Then, double backtracking is possible, i.e., backtracking where at terminal nodes a co-NP-complete problem has to be solved (e.g., classical propositional inference); in case a library procedure is not available, the latter can be done by using flat backtracking for solving the complementary problem. Note, however, that unlike in case of an NP-complete reasoning task, an overall flat backtracking algorithm is not possible (unless Σ_{2}^{P} = NP).

For problems at even higher levels, multiply nested backtracking is feasible; if the problem is complete for Σ_{k}^{P}, k-nested backtracking is possible, but not (k −1)-nested (unless the polynomial hierarchy collapses). Library procedures for subtasks (e.g., for ⊧_{st}^{b}, ⊧_{st}^{c} inference) may be used and decrease the backtracking level accordingly. For the Δ_{k+1}^{P}[O(log n)]-complete problems a combination of binary search and k-nested backtracking is possible.

The level of the polynomial hierarchy at which an abductive reasoning problem resides should be kept in mind; it serves as a basic constraint of whether a proposed backtracking algorithm for that problem is correct or not.

In order to obtain polynomial time algorithms for abduction, the instances have to be restricted so that all sources of complexity are eliminated. The higher the level at which an abduction problem resides, the stronger is the restriction of the instances. It remains to identify polynomial classes of abduction problems. In particular, it would be interesting to see whether there are polynomial classes of abduction problems from the fourth level that are relevant in practice.

Acknowledgements The authors would like to thank the referees for their valuable and instructive comments that helped to improve the presentation of this paper. In particular, Section 3.2 was proposed by a referee; it greatly improves understanding of the relationships between the different abduction problems investigated, and simplified proofs.

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] K. Apt and H. Blair. Arithmetic Classification of Perfect Models of Stratified Programs. In R. Kowalski and K. Bouwen, editors, Proc. Fifth Joint International Conference and Symposium on Logic Programming (JICSLP ’88), pp. 766–779. MIT Press, 1988.

[3] C. Baral, J. Lobo, and J. Minker. Generalized Disjunctive Well-Founded Semantics for Logic Programs. Annals of Mathematics and Artificial Intelligence, 5:89–132, 1992.

[4] C. Baral and M. Gelfond. Logic Programming and Knowledge Representation Journal of Logic Programming, 19/20:73–148, 1994.

[5] C. Baral and V. S. Subrahmanian. Stable and Extension Class Theory for Logic Programs and Default Logics. Journal of Automated Reasoning, 8:345–366, 1992.

[6] N. Bidoit and C. Froidevaux. General Logic Databases and Programs: Default Semantics and Stratification. Information and Computation, 19:15–54, 1991.

[7] A. Brogi, E. Lamma, P. Mancarella, and P. Mello. An Abductive Framework for Extended Logic Programming. In Proc. ICLP ’95, pp. 330–343, 1995.

[8] T. Bylander. The Monotonic Abduction Problem: A Functional Characterization on the Edge of Tractability. In Proc. Second International Conference on Principles of Knowledge Representation and Reasoning (KR-91), pp. 70–77, 1991.

[9] T. Bylander, D. Allemang, M. Tanner, and J. Josephson. The Computational Complexity of Abduction. Artificial Intelligence, 49:25–60, 1991.

[10] M. Cadoli and M. Lenzerini. The Complexity of Closed World Reasoning and Circumscription. Journal of Computer and System Sciences, 43:165–211, April 1994.

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

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

[13] K.L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and Databases, Plenum Press, pp. 293–322, 1978.

[14] 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.

[15] M. Denecker and D. De Schreye. SLDNFA: An Abductive Procedure for Normal Abductive Logic Programs. In Proc. JICSLP ’92, pp. 686–700. MIT Press, 1992.

[16] M. Denecker and D. De Schreye. Representing Incomplete Knowledge in Abductive Logic Programming. In Proc. International Symposium on Logic Programming (ILPS ’93), pp. 147–163. MIT Press, 1993.

[17] P. Dung. Negation as Hypotheses: An Abductive Foundation for Logic Programming. In Proc. International Conference on Logic Programming (ICLP ’91), pp. 3–17. MIT Press, 1991.

[18] P.M. Dung. On the Relation between Stable-and Well-founded Semantics of Logic Programs. Theoretical Computer Science, 105:7–25, 1992.

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

[20] T. Eiter and G. Gottlob. On the Computational Cost of Disjunctive Logic Programming: Propositional Case. Annals of Mathematics and Artificial Intelligence, 15(3/4): 289–323, 1995.

[21] T. Eiter and G. Gottlob and H. Mannila. Adding Disjunction to Datalog. Proc. ACM Symposium on Principles of Database Systems (PODS ’94), May 1994, pp. 267–278.

[22] K. Eshghi and R. Kowalski. Abduction Compared with Negation as Failure. In Proc. ICLP ’89, pp. 234–254. MIT Press, 1989.

[23] K. Eshghi. A Tractable Class of Abduction Problems. In Proc. International Joint Conference on Artificial Intelligence (IJCAI ’93), pp. 3–8, 1993.

[24] G. Friedrich, G. Gottlob, and W. Nejdl. Hypothesis Classification, Abductive Diagnosis, and Therapy. In Proc. International Workshop on Expert Systems in Engineering, pp. 69–78. LNCS/LNAI 462, 1990.

[25] M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Proc. Fifth Logic Programming Symposium, pp. 1070–1080. MIT Press, 1988.

[26] M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9:365–385, 1991.

[27] G. Gottlob, N. Leone and H. Veith. Second-Order Logic and the Weak Exponential Hierarchies. Technical Report CD-TR 95/80, Christian Doppler Lab for Expert Systems, TU Wien, 1995. Extended abstract in: Proc. Conference on Mathematical Foundations of Computer Science (MFCS ’95), pp. 66–81, LNCS 969, 1995.

[28] J. R. Hobbs and M. E. Stickel. Interpretation as Abduction. In Proc. 26th Annual Meeting of the Assoc. for Computational Linguistics, pp. 95–103, 1988.

[29] K. Inoue. Extended Logic Programs with Default Assumptions. In Proc. ICLP ’91, pp. 490–504. MIT Press, 1991.

[30] K. Inoue. Studies on Abductive and Nonmonotonic Reasoning. PhD thesis, Kyoto University, 1992.

[31] K. Inoue and C. Sakama. Transforming Abductive Logic Programs to Disjunctive Programs. In Proc. ICLP ’93, pp. 335–353, 1993.

[32] N. Iwayama and K. Satoh. Computing Abduction using the TMS. In Proc. ICLP ’91, pp. 505–518, 1991.

[33] 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.

[34] A. Kakas and R. Kowalski and F. Toni. Abductive Logic Programming. Journal of Logic and Computation, 2(6):719–771, 1992.

[35] A. Kakas and P. Mancarella. On the Relation Between Truth Maintenance and Abduction. In Proc. of PRICAI’90, pp. 438–443, 1990.

[36] A. Kakas and P. Mancarella. Database Updates Through Abduction. In Proc. Conference on Very Large Databases (VLDB ’90), pp. 650–661, 1990.

[37] A. Kakas and P. Mancarella. Generalized Stable Models: a Semantics for Abduction. In Proc. of ECAI-90, pp. 385–391, 1990.

[38] A. Kakas and P. Mancarella. Stable Theories for Logic Programs. In Proc. ILPS ’91, pp. 88–100, 1991.

[39] H. Kautz and B. Selman. An Empirical Study of Greedy Local Search for Satisfiability Testing. In Proc. National Conference on Artificial Intelligence (AAAI ’93), pp. 46–52. MIT Press, 1993.

[40] P.G. Kolaitis. The Expressive Power of Stratified Logics Programs. Information and Computation 90, 1991, pp. 50-66.

[41] K. Konolige. Abduction versus Closure in Causal Theories. Artificial Intelligence, 53:255–272, 1992.

[42] E. Koutsopias and Ch. Papadimitriou. On the Greedy Algorithm for Satisfiability. Information Processing Letters, 43:53–55, 1992.

[43] N. Leone, M. Romeo, P. Rullo, and D. Saccà, Effective Implementation of Negation in Database Logic Query Languages. In LOGIDATA+: Deductive Database with Complex Objects, LNCS 701, pp. 159–175, 1993.

[44] J. W., Lloyd. Foundations of Logic Programming, Springer-Verlag, 1987.

[45] J. Lobo, J. Minker, and A. Rajasekar. Foundations of Disjunctive Logic Programming. MIT Press, 1992.

[46] W. Lukasiewicz. Non-Monotonic Reasoning. Ellis Horwood Limited, Chichester, England, 1990.

[47] W. Marek, A. Nerode, and J. Remmel. On the Complexity of Abduction. In Proc. IEEE Symposium on Logic in Computer Science (LICS ’96), 1996. Forthcoming.

[48] W. Marek and M. Truszczyński. Autoepistemic Logic. Journal of the ACM, 38(3):588–619, 1991.

[49] W. Marek and M. Truszczyński. Computing Intersection of Autoepistemic Expansions. In A. Nerode, W. Marek, and V. Subrahmanian, editors, Proc. First Int’l Workshop on Logic Programming and Nonmonotonic Reasoning (LPNMR ’91), pp. 37–50, 1991. MIT Press.

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

[51] J. McCarthy. Programs with Common Sense. In Proc. of the Teddington Conference on the Mechanization of Thought Processes, pp. 75–91, London, 1959. Her Majesty’s Stationery Office.

[52] J. McCarthy. Circumscription – A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13:27–39, 1980.

[53] D. McDermott and J. Doyle. Non-Monotonic Logic I. Artificial Intelligence, 13:41–72, 1980.

[54] J. Minker. On Indefinite Data Bases and the Closed World Assumption. In Proc. 6^{th} Conference on Automated Deduction (CADE ’82), pp. 292–308, LNCS 138, 1982.

[55] R. Moore. Semantical Considerations on Nonmonotonic Logics. Artificial Intelligence, 25:75–94, 1985.

[56] C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

[57] C. S. Peirce. Abduction and Induction. In J. Buchler, editor, Philosophical Writings of Peirce, chapter 11. Dover, New York, 1955.

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

[59] F. Pirri, C. Pizzuti. Explaining Incompatibilities in Data Dictionary Design through Abduction. Data and Knowledge Engineering, North-Holland, 13:101–139,1994.

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

[61] T. Przymusinski. On the Declarative and Procedural Semantics of Stratified Deductive Databases. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pp. 193–216. Morgan Kaufman, Washington DC, 1988.

[62] T. Przymusinski. Stable Semantics for Disjunctive Programs. New Generation Computing, 9:401– 424, 1991.

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

[64] K. Ross. The Well-Founded Semantics for Disjunctive Logic Programs. Proc. First Int’l Conf. on Deductive and Object-Oriented Databases (DOOD-89), pp. 352–369. North-Holland, 1989.

[65] D. Saccá and C. Zaniolo. Stable Models and Nondeterminism in Logic Programs with Negation. In Proc. ACM PODS ’90, pp. 305–218, 1990.

[66] D. Saccá. Deterministic and Nondeterministic Stable Model Semantics for Unbound DATALOG Queries, Proc. 5th Int’l Conference on Database Theory (ICDT ’95), LNCS 893, pp. 353–367, 1995.

[67] C. Sakama. Possible Model Semantics for Disjunctive Databases. In Proc. First Int’l Conference on Deductive and Object-Oriented Systems (DOOD ’89), pp. 337–351. North-Holland, 1989.

[68] C. Sakama and K. Inoue. On the Equivalence between Disjunctive and Abductive Logic Programs. In Proc. ICLP ’94, pp. 88–100, 1994.

[69] C. Sakama and K. Inoue. An Alternative Approach to the Semantics of Disjunctive Logic Programs and Deductive Databases. In Journal of Automated Reasoning, 13:145–172, 1994.

[70] K. Satoh, N. Iwayama. A Query Evaluation Method for Abductive Logic Programming. In Proc. JICSLP ’92, pp. 671–685. MIT Press, 1992.

[71] M. Schaerf. Logic Programming and Autoepistemic Logics: New Relations and Complexity Results. In Proc. Italian AI Conference (IA*AI) ’93, LNCS 728, 1993.

[72] J. Schlipf. The Expressive Powers of Logic Programming Semantics. Journal of Computer and System Sciences, 51(1):64–86, 1995. Preliminary version in: Proc. ACM PODS ’90, pp. 196–204.

[73] J. Schlipf. Complexity and Undecidability Results in Logic Programming. Annals of Mathematics and Artificial Intelligence, 15(3/4), 1995.

[74] B. Selman and H. J. Levesque. Abductive and Default Reasoning: A Computational Core. In Proc. AAAI ’90, pp. 343–348. MIT Press, 1990.

[75] L. Stockmeyer. Classifying the Computational Complexity of Problems. Journal of Symbolic Logic, 52(1):1–43, 1987.

[76] L. Stockmeyer and A. Meyer. Word Problems Requiring Exponential Time. In Proc. 5th ACM Symposium on Theory of Computing (STOC ’73), pp. 1–9, 1973.

[77] A. Van Gelder, K. Ross, and J. Schlipf. The Well-Founded Semantics for General Logic Programs. Journal of the ACM, 38(3):620–650, 1991.

[78] M. Vardi. Complexity of Relational Query Languages. In Proc. 14th ACM STOC, pp. 137–146, 1982.