On the Indiscernibility of Individuals in Logic Programming

Thomas Eiter, Georg Gottlob, Nicola Leone

Christian Doppler Labor für Expertensyteme Technische Universität Wien Paniglgasse 16, 1040 Wien

July 30, 1996

CD-TR 96/101

On the Indiscernibility of Individuals in Logic Programming

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

According to Leibniz’s principle, two individuals a and b are indiscernible, if they share the same properties. Indiscernibility of objects provides a potential for optimization in deductive systems, and has e.g. been exploited in the area of active database systems. In this paper, we address the issue of indiscernibility in logic programs and outline possible benefits for computation. After a formal definition of the notion of indiscernibility, we investigate some basic properties. The main contribution is then an analysis of the computational cost of checking indiscernibility of individuals (i.e. constants) in logic programs without function symbols, which we pursue in detail for ground logic programs. For the concern of query optimization, they show that online computation of indiscernibility is expensive, and thus suggest to adopt an offline strategy, which may pay off for certain computational tasks.

1 Introduction

Logic programming, extended with negation and disjunction, is nowadays widely recognized as a powerful tool for knowledge representation and commonsense reasoning [5].

After a great effort for identifying the most intuitive semantics [40, 15, 31, 41, 33, 34], as well as useful linguistic and epistemic extensions of logic programs [22, 21, 14, 16, 20, 9], the logic programming community is recently paying more attention to discovering both semantical and computational properties of logic programs, cf. [26, 27, 37, 11, 8, 23, 6, 38], which may strengthen the theoretical foundations of the field, provide a better understanding of the various semantics, and help in the design of efficient algorithm for the computation.

This paper addresses the property of indiscernibility of individuals (constants) in logic programs.

Intuitively, for semantics based on the “canonical model” approach, which give a unique and always existing model M as the meaning of the logic program (like, e.g., the perfect [31] or the well-founded [41] semantics), two constants a and b are globally indiscernible (denoted a ≡ b) if replacing both a by b and b by a in M does leave the canonical model M unchanged. In this case a ≡ b implies that an atom, say p(a, t), is true in the canonical model M if and only if p(b, t) is true in M as well.

Indiscernibility can be also limited to a set Q of predicates (local indiscernibility). In this case, we limit the [a, b] replacement to the atoms with predicate Q. Given an interpretation I, we denote by I_{Q} the subset of I with predicates in Q, and we denote by I[a, b] the result of replacing b by a and vice versa in I. Thus, we say that a and b are Q-indiscernible (denoted a ≡_{Q} b) if M_{Q}[a, b] = M, that is, replacing both a by b and b by a in the atoms with predicate Q of M does leave the canonical model M unchanged.

For instance, consider a positive logic program with predicates v, e and path, where v and e specify the nodes and the edges of a directed graph G = (V, E), respectively, and path defines the reflexive and transitive closure of e in the usual manner. Then, two vertices a and b are {path}-indiscernible precisely if they belong to the same strongly connected component of G. Moreover, an equivalence class [a]_{≡_{{path}}} of all constants {path}-indiscernible from a is a strongly connected components of G. In particular, the graph G is strongly connected if and only if there is a single such class, i.e., all nodes are {path}-indiscernible (see Example 3.4 in Section 3).

For semantics based on “multiple models” (like, e.g., the stable model semantics [15, 33, 16]), the notion of indiscernibility is slightly more involved, as the non-determinism coming from the multiplicity of the (preferred) models must be taken into account. For instance, consider indiscernibility under stable model semantics. Then, a ≡_{Q} b if, for each stable model M of P, there exists a stable model M′ of P such that M_{Q}[a, b] = M′_{Q}[a, b]; in other words, replacing both a by b and b by a in the atoms with predicate Q of M generates an interpretation which coincides with some stable model of P on the atoms from Q. Global indiscernibility is then defined in the obvious way. (We refer the reader to section 3 for a detailed account of these definitions.)

Q-Indiscernibility of constants in a logic program can be used for the following purposes. For example, it can be useful to know about indiscernibility if one is concerned with finding a

model of a program that contains a particular fact. Such a model finding task arises e.g. in the in course of diagnosis, where one wants to find a model that amounts to a diagnosis.

Suppose we want to find a model of a program P in which an observed fact p(a) is true, and we know that a and b are {p}-indiscernible.

Then, if we succeed to find a model M of P in which p(b) is true, then we know that there is a model M′ of P in which p(a) is true satisfying M′_{{p}} = M_{{p}}[a, b].

If a and b are globally indiscernible, then we can obtain the desired model by M[a, b], and we are done.

Indiscernibility may also be useful in reasoning. If we know that a and b are {p}-indiscernible, and we succeed to prove p(a) (under cautious or brave semantics), then we can infer that also p(b) must be provable. For example, consider

P = {p(a) ← ¬p(b); p(b) ← ¬p(a)}

This program has the stable models M_{1} = {p(a), ¬p(b)}, M_{2} = {¬p(a), p(b)}; thus, a and b are {p}-indiscernible. If we succeed to prove p(a) credulously (e.g., by generating the stable model M_{1}), then we can infer that also p(b) is credulously provable. On the other hand, if we want to infer p(a) under cautious semantics, and we generate M_{2}, then we can immediately infer from indiscernibility that p(a) is not provable from P, since p(b) is false in M_{2}, and hence there exists a model of P in which p(a) is false.

Since a and b are globally indiscernible in this program, the stable model M_{2} can be immediately generated from M_{1}, as M_{2} = M_{1}[a, b].

Unfortunately, as will be clear from the next sections, local indiscernibility comes at a high computational cost, and so it is not useful to determine indiscernibility on-line; it may be useful, however, to determine it off-line and use it when reasoning is done.

The contribution of this paper is mainly twofold.

First, we define precisely the notion of indiscernibility in the framework of logic programming, demonstrate some basic properties of indiscernibility and provide a number of examples which explain the intuitive meaning of indiscernibility.

Second, we provide an in depth analysis of the complexity of both local and global indiscernibility in ground logic programming. We pay also attention on the impact of syntactical restrictions on the complexity of indiscernibility. In fact, we determine the complexity of indiscernibility for normal positive, normal stratified, normal general, disjunctive positive, and disjunctive general logic programs.

The complexity analysis of ground logic programs highlights some important points:

• Deciding whether two given constants a, b are indiscernible in a given ground normal or disjunctive logic program P, is intractable and complete for a class Π_{i}^{P} of the polynomial hierarchy, where i ≤ 3. This applies to both global and local indiscernibility (where the local predicates Q are part of the input),^{1} with the exception of normal logic programs that use stratified negation.

• The complexity of global indiscernibility coincides with the complexity of cautious reasoning under the stable model semantics, and is P-complete for stratified normal logic programs, co-NP-complete for normal logic programs, and Π_{2}^{P} -complete for disjunctive logic programs.

• In case of intractability, local indiscernibility is always one level higher up in the polynomial hierarchy than global indiscernibility.

• In case of disjunctive programs, hard cases of indiscernibility checking are already present with positive (i.e., negation-free) programs.

In case of nonground logic programs, the complexities increase by an exponential (from P to EXPTIME, co-NP to co-NEXP, Π_{2}^{P} to co-NEXP^{NP} and so on), and thus indiscernibility checking has provably an exponential lower bound.

To our knowledge, no other notion of indiscernibility has been defined in the framework of logic programming. Different notions of indiscernibility have been defined in other contexts [1, 2, 7]. In particular, in [2] indiscernibility is used to optimize active databases computations. In [1] indiscernibility is employed to determine some expressibility results. Finally, in [7] indiscernibility allows to identify the extensions of a default theory which holds some nice properties and should therefore be preferred over the others.

1As follows immediately from the results we derive, the same complexity results hold if the local predicates Q are fixed.

The sequel of the paper is organized as follows. Section 2 contains preliminaries on both Logic Programming and Complexity Theory. Section 3 defines formally the notion of indiscernibility. Section 4 is devoted to the analysis of the complexity of indiscernibility on ground programs. Finally, we briefly consider nonground programs and draw our conclusions in Section 5. The appendix overviews some problems on abductive logic programming which are utilized to derive hardness results in the complexity section.

2 Preliminaries

2.1 Logic Programming

The section recalls the basic concepts of logic programming. The syntax of logic programs is given first; then, stable semantics [15, 41] is provided. Stratified programs [3] and their properties are finally presented.

A term is either a constant or a variable^{2}. An atom is a(t_{1}, ..., t_{n}), where a is a predicate of arity n and t_{1}, ..., t_{n} are terms. A literal is either a positive literal p or a negative literal ¬p, where p is an atom.

A (disjunctive) rule r is a clause of the form

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

where a_{1}, ⋯, a_{n}, b_{1}, ⋯, b_{m} are atoms. The disjunction a_{1} ∨ ⋯ ∨ a_{n} is the head of r, while the conjunction b_{1}, ..., b_{k}, ¬b_{k+1}, ..., ¬b_{m} is the body of r. If n = 1 (the head is ∨-free), then r is normal; if m = 0 (the body is ¬-free), then r is positive. A (disjunctive) program P is a finite set of rules. Program P is normal (resp., positive) if all rules in P are normal (resp. positive).

A term, an atom, a literal, a rule or program is ground if no variable appears in it. A ground program is also called propositional program.

Let P be a program. The Herbrand universe U_{P} of P is the set of all constants appearing in P. The Herbrand base B_{P} of P is the set of all possible ground atoms constructible from the predicates appearing in the rules of P and the constants occurring in U_{P} (clearly, both U_{P} and B_{P} are finite). Given a rule r occurring in a program P, a ground instance of r is a rule obtained from r by replacing every variable X in r by σ(X), where σ is a mapping from the variables occurring in r to the constants in U_{P}. We denote by ground(P) the (finite) set of the ground instances of the rules occurring in P.

An (total) interpretation for P is a subset I of B_{P}. A ground positive literal A is true (resp., false) w.r.t. I if A ∈ I (resp., A ∉ I). A ground negative literal ¬A is true (resp., false) w.r.t. I if A ∉ I (resp., A ∈ I).

Let r be a ground rule in ground(P). Rule r is satisfied (or true) w.r.t. I if its head is true w.r.t. I (i.e., some head atom is true) or its body is false (i.e., some body literal is false) w.r.t. I.

2Note that function symbols are not considered in this paper.

A model for P is an interpretation M for P such that every rule r ∈ ground(P) is true w.r.t. M. A model M for P is minimal if no proper subset of M is a model for P. The set of all minimal models for P is denoted by MM(LP).

The first proposal for assigning a semantics to a disjunctive logic program is due to Minker, who presented in [28] a model-theoretic semantics for positive programs. According to [28], the semantics of a program LP is given by the set MM(P) of the minimal models for P. Observe that every program admits at least one minimal model, that is, for every program P, MM(P) ≠ ∅ holds.

Example 2.1 For the positive program P_{1} = {a ∨ b ←} the (total) interpretations {a} and {b} are its minimal models (i.e., MM(P) = { {a}, {b} }). As another example, for the program P_{2} = {a ∨ b ←; b ← a; a ← b}, {a, b} is the only minimal model. □

As far as general programs (i.e., programs where negation may appear) are concerned, a number of semantics has been recently proposed [8, 16, 28, 32, 33, 34, 35, 36] (see [4, 10, 24] for comprehensive surveys).

A generally acknowledged proposal is the extension of the stable model semantics [15] to take into account disjunction [16, 33]. Given a program LP and a total interpretation I, the Gelfond-Lifschitz transformation (“GL transformation”, for short) of P with respect to I, denoted by P^{I}, is the positive program defined as follows:

\begin{aligned}P^{I} = \{a_{1} ∨ ⋯ ∨ a_{n} ← b_{1}, ⋯, b_{k} | & a_{1} ∨ ⋯ ∨ a_{n} ← b_{1}, ⋯, b_{k}, ¬b_{k+1}, ⋯, ¬b_{m} ∈ ground(P) \\ & and b_{i} ∉ I, for all k < i ≤ m\} \end{aligned}

Definition 2.2 [33] Let I be an interpretation for a program P. I is a stable model for P if I ∈ MM(P^{I}) (that is I is a minimal model of the positive program P^{I}). The set of all stable models for P is denoted by ST M(P). □

Example 2.3 Let P = {a ∨ b ← c, b ← ¬a, ¬c, a ∨ c ← ¬b}. Consider I = {b}. Then, P^{I} = {a ∨ b ← c, b ←}. It is easy to verify that I is a minimal model for P^{I}; thus, I is a stable model for P. □

Clearly, if P is positive then P^{I} coincides with ground(P). It turns out that, for a positive program, minimal and stable models coincide.

A normal positive programs P has exactly one stable model which coincide with the least model of P (i.e., it is the unique minimal model of P). When negation is allowed, however, even a normal program can admit several stable models. In this respect, an interesting class of normal programs is the following. A normal program P is (locally) stratified if each atom p ∈ B_{P} can be associated a positive integer l(p) such that, for each rule r ∈ ground(P) with head p and each ground atom q, the following holds: (i) if ¬q occurs in the body of r, then l(p) > l(q); (ii) if q occurs in the body of r, then l(p) ≥ l(q). In particular, if all ground atoms with the same predicate have the same number associated, then P is globally stratified.

Every stratified normal program P has the nice property of admitting precisely one stable model.

Proposition 2.4 Let P be a normal logic program. If P is stratified, then P has precisely one stable model.

Concluding we recall the complexity of recognizing stable models, for both normal and disjunctive programs.

Proposition 2.5 (cf. [26]) Given a normal propositional logic program P and an interpretation M, deciding whether M is a stable model of P is possible in polynomial time.

Proposition 2.6 (cf. [11]) Given a disjunctive propositional logic program P and an interpretation M, deciding whether M is a stable model of P is co-NP-complete. Hardness holds even if P is positive.

2.2 Complexity Theory

For NP-completeness and complexity theory, cf. [30]. The classes Σ_{k}^{P} , Π_{k}^{P} and Δ_{k}^{P} of the Polynomial Hierarchy (PH) (cf. [39]) 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.

Observe that for all k ≥ 1,

Σ_{k}^{P} ⊆ Δ_{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.

There is an exponential analog of PH, called the Weak EXP Hierarchy (WEXPH) [18], whose classes ExpΔk, ExpΣ_{k}^{P}, and ExpΠ_{k}^{P} are defined like the classes Δ_{k}^{P}, Σ_{k}^{P}, and Π_{k}^{P}, with the only difference that Turing machines have an exponential bound on the execution time rather than a polynomial. In particular, ExpΔ_{0}^{P} = ExpP = EXPTIME, ExpΣ_{1}^{P} = ExpNP = NEXP (nondeterministic exponential time), ExpΠ_{1}^{P} = Expco-NP = co-NEXP, ExpΠ_{2}^{P} = co-NEXP^{NP}, and so on. Intuitively, the classes of WEXPH comprise problems whose time complexity is within an exponential factor to the analog classes in PH. Every problem which is complete for a class of WEXPH has provably exponential worst case complexity, and is thus provably intractable; for complete problems within PH, this is currently not known.

3 Indiscernibility

The semantics of a program P is a set Sem_{P} of models (e.g., the set MM(P) of minimal models or the set ST M(P) of stable models).

In this section we assume that a program P and its semantics Sem_{P} is given.

Let Q be a set of predicates and I a set of ground literals. We denote by I_{Q} the restriction of I to the predicates from Q, that is, the set of the literals of I whose predicate is in Q. Moreover, given two constants a, b ∈ U_{P}, we denote by I[a, b] the set of literals obtained by replacing all occurrences of a and b in I by b and a, respectively.

Definition 3.1 Given a set Q of predicates of P. Two constants a, b ∈ U_{P} are Q-indiscernible, denoted a ≡_{Q} b, if, for each model M ∈ Sem_{P}, there exists a model M′ ∈ Sem_{P} such that M_{Q}[a, b] = M′_{Q}. Constants a, b ∈ U_{P} are (globally) indiscernible, denoted a ≡ b, if a ≡_{Q} b, where Q is the set of all predicates of P. □

Proposition 3.2 For any program P, the relations ≡ and ≡_{Q} are equivalence relations on its Herbrand universe U_{P}.

Proof. We have to check that ≡ and ≡_{Q} satisfy reflexivity, symmetry, and transitivity.

We consider here the case where Q contains all predicates, i.e., global indiscernibility (≡); the arguments for local indiscernibility are similar. Reflexivity holds, since obviously for every interpretation I and constant a, I[a, a] = I. Also symmetry holds, since I[a, b] = I[b, a] for every interpretation I and constants a, b. Finally, transitivity holds, since I[a, c] = I[a, b][b, c][a, b] for every interpretation I and constants a, b, and c, and if a ≡ b, b ≡ c and M is a model of program P, then each of M[a, b], M[a, b][b, c], and M[a, b][b, c][a, b] is a model of P as well. □

Given a constant a, we denote by [a]_{≡} and [a]_{≡_{Q}} the equivalence class of a under ≡ and ≡_{Q}, respectively (e.g., [a]_{≡_{Q}} is the set of all constants Q-indiscernible from a).

For convenience, we also write “p” for “{p}” in case Q is a singleton {p}.

For semantics based on the canonical model approach, which give a unique and always existing model as the intended meaning of the program (e.g., well-founded semantics [41] for normal programs, or the least model semantics for normal positive programs), two constants a and b are indiscernible if and only if their substitution is the identity on the canonical model. For instance, a is indiscernible from b on a normal positive program P, if M_{Q}[a, b] = M_{Q}, where M is the least model of P.

Proposition 3.3 Let a and b be two constants in U_{P} and Q be a set of predicates of P. If |Sem_{P} | = 1, then

(a ≡_{Q} b) ⟺ (M_{Q}[a, b] = M_{Q})

where {M} = Sem_{P}.

Proof. Immediate from Definition 3.1. □

(b) (a)  c a  b b a  c

Figure 1: Graphs G and G′

Example 3.4 Consider a positive logic program with predicates v, e and path, where v and e specify the nodes and the edges of a directed graph G = (V, E), respectively, and path defines the reflexive and transitive closure of e. Then, two vertices a and b are path-indiscernible precisely if they belong to the same strongly connected component of G. The classes [a]_{≡_{path}} are the strongly connected components of G. In particular, G is strongly connected if and only if there is a single such class, i.e., all nodes are path-indiscernible.

For instance, given the program

\begin{aligned}P = \{ & path(X, X) ← v(X), path(X, Y) ← e(X, Z) ∧ path(Z, Y), v(X) ← e(X, Y), \\ & v(Y) ← e(X, Y), e(a, b), e(b, c), e(c, a)\}, \end{aligned}

representing the graph G of Figure 1.a, we have that all nodes are path-indiscernible, that is, [a]_{≡_{path}} = {a, b, c} (= [b]_{≡_{path}} = [c]_{≡_{path}}); notice that G is strongly connected.

For instance, a and b are path-indiscernible, since the least model (which is also the unique stable model) of the program is

\begin{aligned}M = \{ & v(a), v(b), v(c), e(a, b), e(b, c), e(c, a), path(a, a), path(b, b), path(c, c), \\ & path(a, b), path(b, c), path(a, c) path(c, a), path(c, b), path(b, a)\} \end{aligned}

and

M_{path} = {path(a, a), path(b, b), path(c, c), path(a, b), path(b, c), path(a, c)
path(c, a), path(c, b), path(b, a) }
= M_{path}[a, b].

Observe that a and b are also {v}-indiscernible; but they are not {e}-indiscernible. Thus, they are not globally indiscernible.

For program P′ = P − {e(c, a)}, no pair of nodes is path-indiscernible. Indeed, the least model of the program is

\begin{aligned}M = \{ & v(a), v(b), v(c), e(a, b), e(b, c), path(a, a), path(b, b), path(c, c), path(a, b), \\ & path(b, c), path(a, c) \}. \end{aligned}

Thus,

M_{path} = { path(a, a), path(b, b), path(c, c), path(a, b), path(b, c), path(a, c) }

and it is different from

M_{path}[a, b] = { path(a, a), path(b, b), path(c, c), path(b, a), path(a, c), path(b, c) }

P′ describes the graph G′ of Figure 1.b, whose strongly connected components are {a}, {b}, and {c}, respectively. □

It is worth noting that, for multiple model semantics (like, e.g., the minimal model semantics), condition (M_{Q}[a, b] = M_{Q}) is sufficient to guarantee that (a ≡_{Q} b), but, it is not necessary.

Example 3.5 Let P be the program {q(a) ∨ q(b)}. If we consider the minimal model semantics, then we have Sem_{P} = {M, N}, where M = {q(a)} and M = {q(b)}. Therefore, (a ≡_{q} b), even if (M_{q}[a, b] ≠ M_{q}) (and also (N_{q}[a, b] ≠ N_{q}) holds). □

We next provide an example of indiscernibility in case of multiple stable models.

Example 3.6 Consider the following program P

\begin{matrix}r_{1} : & color(X, red) ∨ color(X, blue) ∨ color(X, green) ← v(X) \\ r_{2} : & bad-coloring ← e(X, Y), color(X, C), color(Y, C) \\ r_{3} : & abs ← bad-coloring, ¬abs \end{matrix}

Program P represents the 3-colorability of a graph. Given a set F of facts for predicates v and e (encoding the vertex and the edges of a graph G, respectively), there is a one-to-one correspondence between the stable model of P ∪ F and the good coloring of the graph G.

Now, suppose that the color of vertex a is fixed to red (by adding the fact color(a, red) to the program). Then, [a]_{color} is the set of vertex which are colored red in every admissible coloring of the graph where a is red. That is, a vertex b is color-indiscernible from a, if and only if its color is red in every admissible coloring where a is red. As a consequence, [a]_{color} contains all vertices that have always the the same color as a, in every admissible coloring of the graph. □

4 The Complexity of Indiscernibility

The main decisional problems arising in the context of indiscernibility are as follows. Let a program P, two constants a and b in U_{P}, and a set of predicates Q of P be given.

• Is a Q-indiscernible from b ? (Local Indiscernibility)

• Is a globally indiscernible from b ? (Global Indiscernibility)

In this section we analyze the complexity of the above decisional problems on indiscernibility for the case of ground (i.e., propositional) programs. In particular, we shall study the complexity of both local and global indiscernibility under stable model semantics for general disjunctive programs and syntactical subclasses of them.

4.1 Normal Logic Programming

Throughout this section we assume that the logic programs are normal (i.e., disjunction-free).

We start by analyzing the complexity of indiscernibility for the syntactically simplest classes of logic programs.

Theorem 4.1 If P is either a positive or a stratified program, then both global and local indiscernibility are P-complete.

Proof. From Proposition 2.4, P has precisely one stable model M. As a consequence, by virtue of Proposition 3.3, a ≡_{Q} b iff M_{Q}[a, b] = M_{Q}. As a consequence, Q-indiscernibility check for for a, b can be done by first computing the unique stable model M of P, and then checking if M[a, b] = M. Both these tasks are polynomial (for positive or stratified normal programs) and, as a consequence, Q-indiscernibility can be recognized in polynomial time. This strategy is correct regardless whether Q is the set of all predicates of P or Q is a subset of it. Therefore, both local and global indiscernibility are polynomial. P-completeness is an easy consequence of the fact that inference of a ground atom A from a ground datalog program is P-time complete [42] (add a fact p(b, a) and a rule p(a, b) ← A, where p is a new predicate and a, b are fresh constants, and ask whether a and b are indiscernible). □

We next prove that global indiscernibility for normal logic programs with negation is a co-NP-complete decisional problem. The proof of co-NP membership is based on an alternative characterization of global indiscernibility, which is shown below.

Theorem 4.2 Let a and b be two constants in U_{P}.

(a ≡ b) ⟺ (∀M ∈ Sem_{P} M[a, b] ∈ Sem_{P})

Proof. Sufficiency is immediate from Definition 3.1. Concerning necessity, recall that global indiscernibility is indiscernibility under the set of all predicates of P. Now, if Q is the set of all predicates of the program, then, given a model M ∈ Sem_{P}, either M[a, b] ∈ Sem_{P} or no model M′ ∈ Sem_{P} can exist such that M_{Q}[a, b] = M′_{Q}. □

Thus, two constants are globally indiscernible if and only if (·)[a, b] is an automorphism on the set Sem_{P}.

Theorem 4.3 Global indiscernibility is co-NP-complete.

Proof. Membership in co-NP is an immediate consequence of Theorem 4.2. To show hardness, we reduce the problem of deciding whether a ground logic program P has no stable model, which is co-NP-complete [26, 27], to this problem. Let a and b fresh constants not occurring in P, and let p a new predicate. Then, consider the program

P′ = P ∪ { p(a) ← , p(b) ← p(b) }.

Clearly, a, and b are globally indiscernible in P′ if and only if P has no stable model. This proves the result. □

We now turn our attention to the complexity of local indiscernibility.

Theorem 4.4 Let P be a ground logic program and Q be a set of predicates of P. Deciding if two given constants a and b are Q-indiscernible is Π_{2}^{P} -complete. Hardness holds even if P has only two monadic predicates.

Proof. Π_{2}^{P} -Membership. To decide that a and b are not Q-indiscernible, we proceed as follows. Guess M ⊆ B_{LP}, verify that: (i) M is a stable model of P, (ii) there exists no stable model M′ of P such that M_{Q}[a, b] = M′_{Q}. By Proposition 2.5, (i) is done in polynomial time; while (ii) is done by a single call to a NP oracle (to check the complement of (ii) we may guess M′ and polynomially verify the condition M_{Q}[a, b] = M′_{Q}). The problem is therefore in Π_{2}^{P}.

Π_{2}^{P} -Hardness. We give a transformation from abductive logic programming. In particular, we consider the necessity problem [12], which is as follows. An abduction problem P = ⟨Hyp, Man, LP ⟩ is a set of propositional atoms Hyp, a set of propositional literals Man, and a propositional logic program LP. An explanation of P is a subset S ⊆ Hyp such that LP ∪S has a stable model and LP ∪ S infers each literal L ∈ Man under cautious stable inference. Now, the problem is the following one. Given P and h ∈ Hyp, decide whether h is necessary for P, i.e., h belongs to every explanation of P. As shown in [12], this problem is Π_{2}^{P} -complete (see appendix for more details).

We reduce this problem to local indiscernibility as follows. Define a program P which includes the following clauses.

1. For each clause b_{0} ← (¬)b_{1}, … (¬)b_{m} in LP, include the clause

p(b_{0}) ← (¬)p(b_{1}), …, (¬)p(b_{m}).

The propositional atoms in LP are viewed as constants, and p(c) tells that c is a proposition.

2. for each h_{i} ∈ Hyp, include the rules

s(h_{i}) ← ¬p(h_{i}^{∗})
p(h_{i}^{∗}) ← ¬s(h_{i})
p(h_{i}) ← s(h_{i})

where h_{i}^{∗} is a new constant. Here s(h_{i}) intuitively states that h_{i} is included in an explanation for P. The first two rules choose then a subset S of Hyp; the third rule expresses that the chosen S is added to LP, by stating that the atoms in S are true.

3. for each positive literal b_{i} ∈ Man (resp. negative literal ¬b_{i} ∈ Man) include the rule

p(not exp) ← ¬p(b_{i}); (resp. p(not exp) ← p(b_{i}))

where not exp is a new constant. Intuitively, p(not exp) will be true in a stable model of P if it witnesses that the choice of S made in this model is not an explanation.

4. Finally, include the rules

p(c) ← ¬p(d)
p(d) ← ¬p(c)
s(a) ← p(c)
s(b) ← p(d), p(not exp)
s(b) ← p(d), s(h)

where a, b, c and d are new constants. The first two rules choose between p(c) and p(d); the third rule generates a stable model containing s(a); upon every choice for S in 2., there is always a possibility to apply this rule, and thus a stable model containing s(a) exists. The last two rules alternatively generate on the choice for S a stable model containing s(b), but only if either p(not exp) or s(h) (i.e., the choice for S includes h) is true.

It holds that a and b are s-indiscernible in P if and only if h is necessary for P.

To prove this claim, assume first that h is not necessary for P but a ≡_{s} b. We will derive a contradiction, which proves the only if-direction.

Since h is not necessary for P, there exists an explanation S of P such that h ∉ S. Take any stable model N of LP ∪ S and define an interpretation M of P as follows:

M = {p(b) | b ∈ N} ∪ {s(h_{i}) | h_{i} ∈ S} ∪ {p(h_{i}^{∗}) | h_{i} ∈ H \ S} ∪ {p(c), s(a)}

It is easy to see that M is a stable model of P (note that N ⊧ Man). Since a and b are s-indiscernible, there must exist a stable model M′ of P such that M′_{s} = M_{s}[a, b]. Notice that M′_{s} = (M_{s} \ {s(a)}) ∪ {s(b)}. Since s(h) is false in M′, it follows p(d), p(not exp) ∈ M′. Consequently, for some positive literal b_{i} ∈ Man (resp. negative literal ¬b_{i} ∈ Man), we have p(b_{i}) ∉ M′ (resp. p(b_{i}) ∈ M′). It is easy to see (and immediate from well-known modularity properties of stable models, cf. [13, 23]) that the restriction of M′ to the atoms of the grounded program from 1. and 2. is a stable model of that program; let N′ be this stable model. Since the only rules with head p(b_{i}) are in 1. and 2., we infer that p(b_{i}) ∉ N′ (resp. p(b_{i}) ∈ N′). The stable model N′ of the ground program from 1. and 2. obviously corresponds to a stable model N′′ = {b | p(b) ∈ N′, b occurs in LP ∪ S} of LP ∪ S. Thus, LP ∪ S has a stable model N′′ such that N′′ |̸= Man. Therefore, S is not an explanation of P. This is a contradiction, which proves the only if-direction.

For the if direction, suppose that a ≢_{s} b. Hence, there exists a stable model M of P such that for no other stable model M′ of P, M′_{s} = M_{s}[a, b]. Let S = {h_{i} ∈ H | s(h_{i}) ∈ M}. We show that S is an explanation of P such that h ∉ S, which proves the if-direction.

By modularity, the restriction of M to the ground program from 1. and 2. is a stable model of that program. Hence, we infer that N = {b | p(b) ∈ M, b occurs in LP ∪ S} is a stable model of the program LP ∪ S.

Regardless of which rules in 1.–3. are applied, the rules in 4. always provide the possibility to include s(a) in a stable model of P; it follows s(a) ∈ M. Moreover, since no M′_{s} as stated exists, clearly s(h) ∉ M, which means h ∉ S, and p(not exp) ∉ M (otherwise, the rule s(b) ← p(d), p(not exp) can be applied to generate a stable model containing s(b)); the latter implies, by the rules in 3., that p(b_{i}) ∈ M (resp. p(b_{i}) ∉ M) for every positive literal b_{i} ∈ M (resp. negative literal ¬b_{i} ∈ M). Consequently, N is a stable model of LP ∪ S such that LP ∪ S ⊧ Man. To show that S is an explanation of P, it thus remains to show that N′ ⊧ Man for every stable model N′ of LP ∪ S. Towards a contradiction, suppose this is false for some N′. From N′ it is straightforward to build a stable model of the program from 1.–3. in which p(not exp) is true; clearly, by including p(d) and s(b) this model extends to a stable model M′ of P. As easily checked, M′_{s} = (M_{s} \ {s(a)}) ∪ {s(b)} = M_{s}[a, b]. This is a contradiction. It follows that S is an explanation of P such that h ∉ S. This proves the if-direction.

Since the program P is easily constructed from P, the result follows. □ Observe that Theorem 4.4 grasps the simplest case where local indiscernibility is Π_{2}^{P} -hard,

namely, that there are two monadic predicates. Indeed, whenever the program P contains only one predicate, local indiscernibility coincides to global indiscernibility, which is in NP by virtue of Theorem 4.3.

4.2 Disjunctive Logic Programming

Theorem 4.5 Deciding global indiscernibility of two constants a and b for a disjunctive logic program P under stable models is Π_{2}^{P} -complete, and hard already for positive programs.

Proof. Membership is a consequence of Theorem 4.2. To prove that a and b are not indiscernible, we can guess a stable model M of P such that M[a, b] is not a stable model of P. Verifying whether an interpretation N is a stable model of a ground disjunctive program P is in co-NP; thus, the guess for M can be verified in polynomial time with an oracle for NP.

To prove hardness, we reduce the problem of cautious inference from a positive ground disjunctive logic program P to our problem. As shown in [11], cautious inference of a literal ¬w from a given propositional program P is Π_{2}^{P} -hard. Let p be a new predicate and a and b be fresh constants, and define the program P′ by

P′ = P ∪ { p(a) ∨ p(b) ←; p(a) ← w }

Then, a and b are globally indiscernible in P′ if and only if ¬w is cautiously inferred from P. Indeed, observe that the minimal models of P′ are the minimal models of P ∪ M, for all minimal model M of P, and each minimal model of P′, restricted to the language of P, is a minimal model of P. (This follows from modularity properties of disjunctive logic programs, see [13, 23].)

Suppose ¬w is not inferred from the minimal models of P. Then, P has a minimal model M in which w is contained. As a consequence, M ∪ {p(a)} is a minimal model of P′, while M ∪ {p(b)} is not. As a consequence, a and b are not indiscernible in P′. On the other hand, if a and b are not indiscernible in P′, there is a minimal model M of P′ such that M[a, b] is not a minimal model of P′. Since clearly exactly one of p(a) and p(b) is in M, it follows that p(a) ∈ M and w ∈ M. Since M is, restricted to the language of P, a minimal model of P, a minimal model of P exists which contains w. Thus, ¬w is not inferred from the minimal models of P. This proves the result. □

Theorem 4.6 Deciding local indiscernibility of constants a and b for a set of predicates Q in a ground disjunctive logic program P is Π_{3}^{P} -complete. Hardness holds even for positive logic programs with two monadic predicates.

Proof. Π_{3}^{P} -Membership. The proof of membership is similar as in the case of normal logic programs, with the only difference that an co-NP-oracle is used to check whether an interpretation M is a stable model (for normal logic programs, that problem is polynomial), which is by the Proposition 2.6 co-NP-complete.

Π_{3}^{P} -Hardness. For the general case, Π_{3}^{P} -hardness is shown using the same reduction as in the proof of Theorem 4.4, but applied to a disjunctive logic programming abduction problem ⟨Hyp, Man, LP ⟩, i.e., the program LP is a disjunctive logic program. Indeed, the necessity problem (deciding whether a given hypothesis h ∈ H belongs to all explanations) is Π_{3}^{P} -complete [13] (see also appendix). The proof that the reduction is correct is analogous.

In the rest of the proof, we show that Π_{3}^{P} -hardness holds under the restriction to positive programs P. For that, we use the fact that the necessity problem remains Π_{3}^{P} -hard even if the disjunctive logic program LP in P is positive. Thus, all rules in the group 1. of the reduction are positive. We show how the nonpositive rules in the other groups 2.–4. can be be replaced by positive rules.

• The choice rules

\begin{matrix}s(h_{i}) ← ¬p(h_{i}^{∗}) \\ p(h_{i}^{∗}) ← ¬s(h_{i}) \end{matrix}

for each h_{i} ∈ H from 2. are replaced by the equivalent single disjunctive rule

s(h_{i}) ∨ p(h_{i}^{∗}) ←;

Similarly, the choice

\begin{matrix}p(c) ← ¬p(d) \\ p(d) ← ¬p(c) \end{matrix}

from 4. is implemented by the single disjunctive rule

p(c) ∨ p(d) ←

• for each rule from 3. that has a negative literal in the body, i.e., rule

p(not exp) ← ¬p(b_{i})

introduce the following positive rules:

\begin{aligned}p(c_{i}) ∨ p(d_{i}) & ← \\ p(c_{i}) & ← p(b_{i}) \\ p(not exp) & ← p(d_{i}), \end{aligned}

where c_{i} and d_{i} are fresh constants. The effect of these rules is as follows. By the first rule, each stable model M of the program must contain either p(c_{i}) or p(d_{i}). If M includes p(b_{i}), it includes p(c_{i}) (as it is a model), and hence, by the minimality of a stable model, p(d_{i}) is not contained in M. Therefore, the last clause cannot be applied to include p(not exp) in M. If p(b_{i}) is not in the model, then either p(c_{i}) or p(d_{i}) is in M, but not both; in the latter case, p(not exp) is included, and hence some stable model M containing p(not exp) exists.

It holds that in the obtained positive program P, the constants a and b are s-indiscernible if and only if h is necessary for P. This shows that deciding local indiscernibility is Π_{3}^{P} -hard, even if the program P is positive and and there are only two monadic predicates. The result follows.

□

5 Discussion and Conclusion

The results on indiscernibility checking for normal and disjunctive ground logic programs are summarized in Table 1. They show that this problem is polynomial only in case where the underlying program has no disjunction and negation is stratified. If we allow either for disjunction or for arbitrary negation, then indiscernibility checking becomes intractable, where local indiscernibility is always one level higher in the polynomial hierarchy than global indiscernibility.

Deciding a ≡ b Deciding a ≡_{Q} b
normal positive  P-complete  P-complete
normal stratified  P-complete  P-complete
normal general  co-NP-complete Π_{2}^{P} -complete
disjunctive positive Π_{2}^{P} -complete  Π_{3}^{P} -complete
disjunctive general Π_{2}^{P} -complete  Π_{3}^{P} -complete

Table 1: Complexity of indiscernibility for ground logic programming

It appears that global indiscernibility checking has the same complexity as cautious inference of a literal from the stable models of a normal resp. disjunctive logic program, which is co-NP-complete and Π_{2}^{P} -complete, respectively; the same holds in case of a positive disjunctive logic program.

The results for the ground case suggest that in the nonground case, the complexity of indiscernibility checking increases by an exponential, similar as for reasoning problems [12]. Indeed, by first grounding a given program P and then applying the algorithm for the ground case, we obtain that the exponential analog of the respective complexity class in Table 1 (EXPTIME for P and ExpΠ_{k}^{P} for Π_{k}^{P}, in particular co-NEXP for co-NP) is an upper bound of the complexity of indiscernibility checking. Moreover, by utilizing results through complexity upgrading techniques [13, 17], it is possible to derive matching hardness results; we do not pursue this here. Notice that by our reductions in the previous section, the EXPTIME-hardness results follows immediately from the result that inference of a ground atom from a nonground datalog program is EXPTIME-complete (cf. [42]), and the ExpΠ_{2}^{P} -hardness results for disjunctive programs from the result that brave inference of a ground literal from a (positive) disjunctive datalog program is ExpΣ_{2}^{P} -complete [13].

As pointed out, indiscernibility may be useful in the process of model finding as well as reasoning. From the computational side, it is not attractive (and in case of local indiscernibility even disadvantageous) to determine indiscernibility online. However, the indiscernibility relation can be determined off-line for later online use. In particular, indiscernibility information can be quite useful for model finding; notice that it is not viable to precompute all stable model of a logic program, since there may be exponentially many and hence they occupy exponential space. On the other hand, the indiscernibility relation occupies only linear space.

The results of this paper give a clear picture of the complexity of indiscernibility of logic programs in case of no function symbols. In the case where function symbols are present, global and local indiscernibility are clearly undecidable, since it is undecidable whether a normal logic program has a stable model [25]. We leave the study of indiscernibility on logic programs with function symbols for other research.

References

[1] A. Abiteboul, K. Compton, and V. Vianu. Queries are Easier than You Thought (Probably). In Proceedings ACM PODS ’92, pages 218–229, 1992.

[2] S. Abiteboul and A. van Gelder. Optimizing Active Databases using the Split Technique. In J. Biskup and R. Hull, editors, Proceedings 4th Intl. Conference on Database Theory (ICDT ’92), LNCS 646, pages 171–187, 1992.

[3] K. Apt, H. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In Minker [29], pages 89–148.

[4] K. Apt and N. Bol. Logic Programming and Negation: A Survey. Journal of Logic Programming, 19/20:9–71, 1994.

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

[6] R. Ben-Eliyahu and R. Dechter. Propositional Semantics for Disjunctive Logic Programs. Annals of Mathematics and Artificial Intelligence, 12:53–87, 1994.

[7] R. Ben Eliyahu, N. Francez, M. Kaminski. Similarity Preservation in Default Logic. Technical Report 96-04, Department of mathematics and computer science, Ben-Gurion university of the Negev, Beer Sheva, Israel.

[8] S. Brass and J. Dix. Characterizations of the Stable Semantics by Partial Evaluation. Journal of Logic Programming, 1996, to appear.

[9] F. Buccafurri, N. Leone, and P. Rullo. Stable Models and their Computation for Logic Programming with Inheritance and True Negation. Journal of Logic Programming, 27(1):5–43, 1996.

[10] J. Dix. Semantics of Logic Programs: Their Intuitions and Formal Properties. An Overview. In Logic, Action and Information. Proc. of the Konstanz Colloquium in Logic and Information (LogIn’92), pages 241–329. DeGruyter, 1995.

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

[12] T. Eiter, G. Gottlob, and N. Leone. Abduction From Logic Programs: Semantics and Complexity. Theoretical Computer Science, to appear. Extended abstract in Proc. LPNMR’95, LNCS 982, 1–14, 1995.

[13] T. Eiter, G. Gottlob, and H. Mannila. Adding Disjunction to Datalog. In Proc. ACM PODS ’94, pages 267–278, 1994.

[14] M. Gelfond. Logic Programming and Reasoning with Incomplete Information. Annals of Mathematics and Artificial Intelligence, 12:89–116, 1994.

[15] M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Logic Programming: Proceedings Fifth Intl Conference and Symposium, pages 1070–1080, Cambridge, Mass., 1988. MIT Press.

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

[17] G. Gottlob, N. Leone, and H. Veith. Second-Order Logic and the Weak Exponential Hierarchies. In J. Wiedermann and P. Hajek, editors, Proc. 20th Conf. on Mathematical Foundations of Computer Science (MFCS ’95), LNCS 969, pages 66–81, Prague, 1995. Full paper available as CD/TR 95/80, Christian Doppler Lab for Expert Systems, TU Vienna.

[18] L. Hemachandra. The Strong Exponential Hierarchy Collapses. Journal of Computer and System Sciences, 39:299–322, 1989.

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

[20] R. Kowalski and F.Sadri. Logic Programs with Exceptions. In Proceedings ICLP-90, pages 598–616. MIT Press, 1990.

[21] E. Laenens, D. Saccá, and D. Vermeir. Extending Logic Programming. In Proceedings ACM SIGMOD Int’l Conference on Management of Data, 1990.

[22] E. Laenens and D. Vermeir. A Fixpoint Semantics for Ordered Logic. Journal of Logic Programming, 1:159–185, 1990.

[23] V. Lifschitz and H. Turner. Splitting a Logic Program. In Proceedings ICLP-94, pages 23–38, Santa Margherita Ligure, Italy, June 1994. MIT-Press.

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

[25] W. Marek, A. Nerode, and J. Remmel. The Stable Models of a Predicate Logic Program. Journal of Logic Programming, 21(3), 1994.

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

[27] W. Marek and M. Truszczyński. Computing Intersection of Autoepistemic Expansions. In A. Nerode, W. Marek, and V. Subrahmanian, editors, Proc. LPNMR-91, pages 37–50, Washington DC, July 1991. MIT Press.

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

[29] J. Minker, editor. Foundations of Deductive Databases and Logic Programming. Morgan Kaufman, Washington DC, 1988.

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

[31] T. Przymusinski. On the Declarative and Procedural Semantics of Stratified Deductive Databases. In Minker [29], pages 193–216.

[32] T. Przymusinski. Well-founded Semantics Coincides with 3-Valued Semantics. Fundamenta Informaticae, 13:445–463, 1990.

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

[34] T. Przymusinski. Static Semantics for Normal and Disjunctive Logic Programs. Annals of Mathematics and Artificial Intelligence, 14(2-4), 1995.

[35] K. Ross. The Well-Founded Semantics for Disjunctive Logic Programs. In Proceedings First Intl. Conf. on Deductive and Object-Oriented Databases (DOOD-89), pages 352–369, 1989.

[36] C. Sakama. Possible Model Semantics for Disjunctive Databases. In Proceedings First Intl. Conf. on Deductive and Object-Oriented Databases (DOOD-89), pages 337–351, Kyoto Japan, 1989.

[37] D. Saccá, C. Zaniolo. Deterministic and Non-Deterministic Stable Models. submitted for publication to Journal of Logic and Computation, T.R. ISI-CNR, 1996.

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

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

[40] M. H. van Emden and R. Kowalski. The Semantics of Logic as a Programming Language. Journal of the ACM, 3:733–742, 1976.

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

[42] M. Vardi. Complexity of relational query languages. In Proceedings 14th ACM STOC, pages 137–146, San Francisco, 1982.

Appendix

Abductive logic programming deals with the problem of finding an explanation for observations, based on a theory represented by a logic program [19]. Roughly, abduction is an inverse of modus ponens: Given the clause a ← b and the observation b, abduction concludes a as a possible explanation.

A number of variants of abductive logic programmings have been introduced so far; the paper [12] presents a basic framework of abduction, discusses different modes of abduction, and presents a detailed analysis of the complexity of the main abductive reasoning tasks.

An propositional abductive logic programming problem (LPAP) is formally described as a tuple P = ⟨Hyp, Man, LP ⟩, where Hyp is a set of propositional atoms (called hypotheses), Man is a set of propositional literals (called manifestations or observations), and LP is a propositional logic program (with negation allowed). In case LP is a disjunctive logic program, we have a disjunctive LPAP. An explanation for P is a subset S ⊆ H which satisfies the following properties:

1. The program LP ∪ S has some stable model; and

2. LP ∪ S ⊧ Man, i.e., each literal in Man is a cautious consequence of the stable models of the program LP ∪ S.

(In fact in [12] abduction based on different semantics and reasoning modalities are considered.)

In general, an LPAP may have no, a single, or several explanations. In account of the latter, necessity of a hypothesis has been identified as an important property. A hypothesis is necessary for an LPAP P, if it occurs in every explanation of P. The problem of deciding whether a hypothesis is necessary is one of the main decisional abductive reasoning tasks, since it is important for computing the core of abductive explanations. Thus, the necessity problem of logic programming abduction is as follows: Given a LPAP P = ⟨Hyp, Man, LP ⟩ and a hypothesis h ∈ H, decide whether h is necessary for P.

Concerning the computational complexity of the necessity problem, the following results have been established in [12]:

[12, Theorem 11] Deciding if a given hypothesis is necessary for a given LPAP P = ⟨Hyp, Man, LP ⟩ is Π_{2}^{P} -complete.

[12, Theorem 18,24] Deciding if a given hypothesis is necessary for a given disjunctive LPAP P = ⟨Hyp, Man, LP ⟩ is Π_{3}^{P} -complete; moreover, the problem is Π_{3}^{P} -hard already on instances where LP is positive, i.e., ¬-free.

For a formal proof of these results, we refer the reader to the [12]; we here only describe the intuition why the problems have this complexity.

In order to decide whether hypothesis h is necessary, all explanations of P must be inspected (in the worst case) too see that this is not the case; in order to show that h is not necessary, we have to exhibit an explanation S for P in which h is not contained. There is an exponential space of candidates S ⊆ H, and in fact there are cases where exponentially many explanations exist. An explanation S such that h ∉ S might be nondeterministically guessed; we are left with proving then that the guess is proper, i.e., is in fact an explanation. Deciding whether a given S is an explanation turns out difficult; first, we must decide whether LP ∪ S has some stable model and second, whether LP ∪ S ⊧ Man. Both tests are inference problems that are well-known NP- and co-NP-complete problems [27]. Thus, we can verify the guess with an oracle for NP in polynomial time. Overall, we have a Σ_{2}^{P} algorithm for deciding whether h is not necessary; as a consequence, the necessity problem is in Π_{2}^{P}.

Hardness is shown in [12] encoding the test of validity of quantified Boolean formulas of form ∀X∃Y E, where X, Y are sets of propositional variables and E is a Boolean formula whose atoms are from X ∪ Y.

For the case of disjunctive LPAPs, the situation is similar as for normal LPAPs. The only difference is that the complexity of deciding whether LP ∪S has a (disjunctive) stable model and LP ∪ S ⊧ Man is Σ_{2}^{P} -complete and Π_{2}^{P} -complete, respectively [11]. Consequently, we need an oracle for Σ_{2}^{P} problems in order to decide whether a given S is an explanation. Hardness for Π_{3}^{P} is shown in [12] again by an encoding of validity testing of quantified Boolean formulas, which in this case have form ∀X∃Y ∀ZE.

That deciding necessity is already Π_{3}^{P} -hard on positive disjunctive programs LP is somewhat unexpected, but not really surprising. In fact, cautious inference of literals from the minimal models of a positive disjunctive program is Π_{2}^{P} -hard [11]. This causes that the full power of the Σ_{2}^{P} -oracle is needed for checking whether a set S is an explanation.