Dealing with Incoherence in ASP: Split Semi-Equilibrium Semantics? Giovanni Amendola Department of Mathematics and Computer Science, University of Calabria Via P. Bucci, Cubo 30b, 87036 Rende (CS), Italy amendola@mat.unical.it Abstract. The answer set semantics may assign a logic program no model due to classic contradiction or cyclic negation. The latter can be remedied by a paraco- herent semantics given by semi-equilibrium (SEQ) models, which are 3-valued interpretations that generalize the logical reconstruction of answer sets given by equilibrium models. However SEQ-models miss modularity in the rules, such that a natural modular (bottom up) evaluation of programs is hindered. We thus refine SEQ-models using splitting sets, the major tool for modularity in answer set programs. We consider canonical models that are independent of any particular splitting sequence from a class of splitting sequences, and present two such classes whose members are efficiently recognizable. Split SEQ-models does not make reasoning harder, except for deciding model existence in presence of constraints. 1 Introduction Answer set programming is a popular formalism in logic programming (LP). The answer set semantics [5] does not assign to every logic program a model. This can be either due to a logical contradiction, as emerging e.g. in the program {open ← not closed ; ¬open ←}1 , or due to cyclic negation, as e.g. in the program {shaves(joe, joe) ← not shaves(joe, joe)} (a paraphrase of Russell’s paradox, where joe is the barber). In order to avoid trivialization of reasoning from such programs, Inoue and Sakama [15] introduced paraconsistent semantics for answer set programs. While dealing with explicit contradictions can be achieved with similar methods as for (non-)classical logic (cf. [2, 1, 8]), dealing with cyclic negation turned out to be tricky. With the idea that atoms may also be possibly true, Inoue and Sakama defined a semi-stable semantics which for Russell’s paradox above yields the model that shaves(joe, joe) is possibly true. In fact, semi-stable models approximate answer sets and coincide with them whenever a program has some answer set; otherwise, they yield under Occam’s razor models with a least set of atoms believed to be true. That is, the intrinsic closed world assumption (CWA) of logic programs is slightly relaxed for achieving stability of models. In a similar vein, we can regard many semantics for non-monotonic logic programs that relax answer sets as paracoherent semantics, e.g. [4, 9, 13, 14, 17, 18]. Ideally, such a relaxation meets for a program P the following desiderata [3]: ? This work has been carried out under the supervision of professors Thomas Eiter and Nicola Leone, and was partially supported by Regione Calabria under the EU Social Fund and project PIA KnowRex POR FESR 2007- 2013, and by the Italian Ministry of University and Research under PON project “Ba2Know (Business Analytics to Know) S.I.-LAB n. PON03PE 0001. 1 Note that ’¬’ denotes the strong negation, instead ’not ’ denotes the negation as failure. (D1) Every (consistent) answer set of P corresponds to a model (answer set coverage). (D2) If P has some (consistent) answer set, then its models correspond to answer sets (congruence). (D3) If P has a classical model, then P has a model (classical coherence). However, only few paracoherent semantics satisfy all three desiderata (cf. [3]). A recent one are semi-equilibrium (SEQ) models [3], which improve semi-stable models by avoiding some anomalies. SEQ-models are a relaxation of Pearce’s well-known equilibrium models [10], which provide a logical reconstruction of answer sets alias stable models in terms of a non-monotonic version of Heyting’s [6] logic of here and there (HT-logics). Roughly speaking, SEQ-models are 3-valued interpretations in which atoms can be true, false or believed to be true; the gap between believed and derivably true atoms is globally minimized by SEQ-models. While the SEQ-semantics has nice properties, it may select models that do not respect modular structure in the rules. To illustrate this, consider the following example. Example 1 Suppose we have a program that captures knowledge about friends of a person regarding visits to a party, where go(X) informally means that X will go:    go(John) ← not go(Mark );  P = go(Peter ) ← go(John), not go(Bill ); go(Bill ) ← go(Peter )   Then P has no answer set; its semi-equilibrium models (a subset of HT-models) are M1 = (∅, {go(Mark )}), and M2 = ({go(John)}, {go(John), go(Bill )}). Informally, a key difference between M1 and M2 concerns the beliefs on Mark and John. In M2 Mark does not go, and, consequently, John will go (moreover, Bill is believed to go, and Peter will not go). In M1 , instead, we believe Mark will go, thus John will not go (likewise Peter and Bill). None of the two models provides a fully coherent view (on the other hand, the program is incoherent, having no answer set). Nevertheless, M2 appears preferable over M1 , since, according with a layering (stratification) principle, which is widely agreed in LP, one should prefer go(John) rather than go(Mark ), as there is no way to derive go(Mark ) (which does not appear in the head of any rule of the program). Modularity via rule dependency as in the example above is widely used in problem modeling and logic programs evaluation; in fact, program decomposition is crucial for efficient answer set computation. For the program P above, advanced answer set solvers like DLV and clasp immediately set go(Mark ) to false, as go(Mark ) does not occur in any rule head. In a customary bottom up computation along program components, answer sets are gradually extended until the whole program is covered, or incoherence is detected at some component (in our example for the last two rules). But rather than to abort the computation, we would like to switch to a paracoherent mode and continue with building semi-equilibrium models, as an approximation of answer sets. In this general setting, we refine SEQ-models with the following contributions. – Resorting to splitting sets [7], the major tool for modularity in modeling and evaluat- ing answer set programs, we define split SEQ-models (Section 3), for which the program is evaluated in progressive layers according to a splitting sequence of the atoms. In the example above, the natural sequence S = ({go(Mark )}, {go(Mark ), go(John)}, {go(Mark ), go(John), go(Bill ), go(Peter )}) will yield the expected result. – In general, the resulting split SEQ-models depend on the particular splitting sequence S. We thus introduce canonical splitting sequences, with the property that the models are independent of any particular from a class of splitting sequences, and thus yield canonical models (Section 4). For constraint-free programs P , the class derived from the strongly connected components (SCCs) of P warrants this property, as well as modularity property. For arbitrary programs, independence is held by a class derived from the maximal joined components (MJCs), merging SCCs involved in constraints. – We characterize the computational complexity of split SEQ-model semantics, for canonical models and various classes of logic programs (Section 5). The refined semantics (SCC -models) lends for a modular use and bottom up evalua- tion of programs. Cautious merging of components (MJC -models) aims at preserving independence and possible parallel evaluation. So this semantics is attractive for incor- poration into answer set evaluation frameworks, in order to add paracoherent features. 2 Preliminaries We start with recalling answer set semantics and fixing notation, and then present the paracoherent semantics of semi-equilibrium models. Answer Set Programs. Following the traditional grounding view [5], we concentrate on programs over a propositional signature Λ. A disjunctive rule r is of the form a1 ∨ · · · ∨ al ← b1 , ..., bm , not bm+1 , ..., not bn , (1) where all ai and bj are atoms (from Λ) and l ≥ 0, n ≥ m ≥ 0 and l + n > 0; not represents negation-as-failure. The set H(r) = {a1 , ..., al } is the head of r, while B + (r) = {b1 , ..., bm } and B − (r) = {bm+1 , . . . , bn } are the positive body and the negative body of r, respectively; the body of r is B(r) = B + (r) ∪ B − (r). We denote by At(r) = H(r) ∪ B(r) the set of all atoms occurring in r. For any set of atoms S, we let not S = {not a | a ∈ S}; rules of form (1) will also be written (in abuse of notation) H(r) ← B + (r), not B − (r). A rule r is a fact, if B(r) = ∅ (we then omit ←); a constraint, if H(r) = ∅; normal, if |H(r)| ≤ 1 and positive, if B − (r) = ∅. A (disjunctive logic) program P is a finite set of disjunctive rules. P is S called normal [resp. positive] if each r ∈ P is normal [resp. positive]. We let At(P ) = r∈P At(r). Any set I ⊆ Λ is an interpretation; it is a model of a program P (denoted I |= P ) iff for each rule r ∈ P , I ∩ H(r) 6= ∅ if B + (r) ⊆ I and B − (r) ∩ I = ∅ (denoted I |= r). A model M of P is minimal, iff no model M 0 ⊂ M of P exists. We denote by MM (P ) the set of all minimal models of P and by AS(P ) the set of all answer sets (or stable models) of P , i.e., the set of all interpretations I such that I ∈ MM (P I ), where P I is the well-known Gelfond-Lifschitz reduct [5] of P w.r.t. I. Semi-equilibrium paracoherent semantics. We call logic programs that lack answer sets due to cyclic dependency of atoms among each other by rules through negation in- coherent (cf. Russel’s paradox). The semi-equilibrium semantics [3] avoids incoherence by resorting to the view of answer sets in the logic of here and there (HT-logic) [10, 11]. We focus here on formulas φ of the form b1 ∧ ... ∧ bm ∧ ¬bm+1 ∧ ... ∧ ¬bn → a1 ∨ ... ∨ al , (2) which correspond in an obvious way to rules of form (1). In HT-logic, interpretations are pairs (X, Y ), X ⊆ Y ⊆ Λ, where X is the here world and Y the there world. Intuitively, the atoms in X are true (value t), atoms not in Y are false (f ), and the atoms in gap(X, Y ) = Y \ X are believed to be true (bt). For any set A of HT-interpretations, we denote by mc(A) the set of maximal canonical interpretations (X, Y ) ∈ A, i.e., no (X 0 , Y 0 ) ∈ A exists such that gap(X 0 , Y 0 ) ⊂ gap(X, Y ). We define (X, Y ) to be an HT-model of the formula φ, denoted (X, Y ) |= φ, in a recursive way: 1. (X, Y ) |= a iff a ∈ X; 2. (X, Y ) 6|= ⊥; (⊥ is falsity) 3. (X, Y ) |= φ ∧ ψ iff (X, Y ) |= φ and (X, Y ) |= ψ; 4. (X, Y ) |= φ ∨ ψ iff (X, Y ) |= φ or (X, Y ) |= ψ; 5. (X, Y ) |= φ → ψ iff (i) (X, Y ) 6|= φ or (X, Y ) |= ψ, and (ii) Y |= φ → ψ;2 6. (X, Y ) |= ¬φ iff (X, Y ) |= φ → ⊥. In particular, (X, Y ) |= ¬a iff a ∈ / Y , and (X, Y ) |= r for a rule r of form (2) iff either {a1 . . . , ak } ∩ X 6= ∅, {b1 , . . . , bm } 6⊆ Y , or {bm+1 , . . . , bn } ∩ Y 6= ∅. A HT-interpretation (X, Y ) is an HT-model of a theory (i.e., a set of formulas) Θ, denoted (X, Y ) |= Θ iff (X, Y ) |= φ for each φ ∈ Θ. It is an equilibrium (EQ) model of Θ iff X = Y and for every X 0 ⊂ Y it holds that (X 0 , Y ) 6|= Θ. As shown by Pearce [10], M ⊆ At(P ) fulfills M ∈ AS(P ) iff (M, M ) is an EQ- model of ΘP . Paracoherent answer sets emerge with minimal sets of believed atoms. Definition 1 ([3]) A semi-equilibrium (SEQ) model (or paracoherent answer set) of a program P is any HT-model (X, Y ) of P s.t. (i) (X 0 , Y ) 6|= P , for all X 0 ⊂ X (h- minimality) and (ii) no HT-model (X 0 , Y 0 ) of P satisfies h-minimality and gap(X 0 , Y 0 )⊂ gap(X, Y ) (gap-minimality). The set of all semi-equilibrium models of P is denoted by SEQ(P ). Example 2 Consider the program P = {a ← b; b ← not a}. Its HT-models are (∅, a), (∅, ab), (a, a), (a, ab), (b, ab) and (ab, ab). Hence, there is no equilibrium model for P , while SEQ(P ) = {(∅, a)}. 3 Split Semi-Equilibrium Semantics In this section, we introduce a refinement to the semi-equilibrium semantics. In fact we observe that sometimes gap minimization is too weak. Consider the following example. Example 3 Let P = {c ← b, not c; b ← not a}; then SEQ(P ) = { (b, bc), (∅, a)}. Here (b, bc) is more appealing than (∅, a) because a is not derivable, as no rule has a in the head. Moreover, intuitively, P1 = {b ← not a} is a lower (coherent) part feeding into the upper part P2 = {c ← b, not c}. To overcome this limitation, we introduce a refined paracoherent semantics, called split semi-equilibrium semantics. It coincides with the answer sets semantics in case of coherent programs, and selects a subset of the SEQ-models otherwise. The main results 2 Note that in condition 5.(ii) ’|=’ is the standard operator of classical propositional logic. of this section are two model-theoretic characterizations which identify necessary and sufficient conditions for deciding whether a SEQ-model is selected. Splitting sets and sequences. Splitting sets [7] allow us to divide a program P into two parts which can be evaluated bottom up. Formally, a set S ⊆ At(P ) is a splitting set of P , if for each rule r in P s. t. H(r) ∩ S 6= ∅, then At(r) ⊆ S. We denote by bS (P ) = {r ∈ P | At(r) ⊆ S} the bottom of P , tS (P ) = P \ bS (P ) the top of P relative to S. Splitting sets naturally lead to splitting sequences. A splitting sequence S = (S1 , . . . , Sn ) of P is a sequence of splitting sets of P s. t. Si ⊆ Sj for each i < j. Split semi-equilibrium models. We introduce the notion of SEQ-models related to a splitting set. Given a splitting set S for a program P and an HT-interpretation (I, J) for bS (P ), we let P S (I, J) = P \ bS (P ) ∪ {a | a ∈ I} ∪ {← not a | a ∈ J} ∪ {← a | a ∈ S \ J}. Informally, the bottom part of P w.r.t. S is replaced with rules and constraints which fix in any EQ-model of the remainder (= tS (P )) the values of the atoms in S to (I, J). Definition 2 (Semi-equilibrium models related to a splitting set) Let S be a splitting set of a program P . Then the semi-equilibrium models of P related to S are defined as  [  SEQ S (P ) = mc SEQ(P S (I, J)) . (3) (I,J)∈SEQ(bS (P )) Example 4 (cont’d) For the splitting set S = {a, b} of P in Example 3, bS (P ) = {b ← not a} and SEQ(bS (P )) = {(b, b)}. Hence, P S (b, b) = {c ← b, not c; b; ← not b; ← a} and SEQ S (P ) = SEQ(P S (b, b)) = {(b, bc)}. For any HT-model (X, Y ) and splitting set S of a program P , we define the restric- tion of (X, Y ) to S as (X, Y )|S = (X ∩ S, Y ∩ S). We have proved the following semantic characterization for semi-equilibrium models related to a splitting set: Theorem 1 Let S be a splitting set of a program P . Then (X, Y ) ∈ SEQS (P ) iff (X, Y ) ∈ SEQ(P ) and (X, Y )|S ∈ SEQ(bS (P )). Now we generalize the use of splitting sets to compute the SEQ-models of a program via splitting sequences. Definition 3 (Semi-equilibrium models related to a splitting sequence) Given a split- ting sequence S = (S1 , . . . , Sn ) for a program P , we let S 0 = (S2 , ..., Sn ) and define the semi-equilibrium models of P related to the splitting sequence S = (S1 , ..., Sn ) as  [ 0  SEQS (P ) = mc SEQS (P S1 (I, J)) . (4) (I,J)∈SEQ(bS1 (P )) The SEQ-models related to a splitting sequence can be characterized similarly as those related to a splitting set. To ease presentation, for a program P and split- ting sequence S = (S1 , ..., Sn ), we let P0 = P and Pk = (Pk−1 )Sk (Ik , Jk ), where (Ik , Jk ) ∈ SEQ(bSk (Pk−1 )), k = 1, ..., n. We now state the main result of this section. Theorem 2 Let S = (S1 , ..., Sn ) be a splitting sequence of a program P . Then (X, Y ) ∈ SEQ S (P ) iff (X, Y ) ∈ SEQ(P ) and (X, Y )|Sk ∈ SEQ(bSk (Pk−1 )), for k = 1, ..., n. Note that a classically consistent program does not necessarily have split SEQ- models. In fact, if P = {← b; b ← not a} and S = {a}, then SEQ(bS (P )) = {(∅, ∅)} and so SEQS (P ) = ∅. However (a, a) and (∅, a) are HT-models of P . 4 Canonical Semi-Equilibrium Models The split SEQ-semantics depends on the choice of the particular splitting sequence, which is not much desirable. We thus consider a way to obtain a refined split SEQ- semantics independent of a particular splitting sequence, but imposes conditions on sequences that come naturally with the program and can be easily tested. Attractive are the strongly connected components (SCCs) of a given program, which are at the heart of bottom up evaluation algorithms in ASP systems. In absence of constraints, we get the desired independence of a particular splitting sequence, and so we can talk about the SCC -models of a program. Allowing for constraints will need a slight extension. 4.1 SCC -split sequences and models Recall that the dependency graph of a program P is the directed graph DG(P ) = hVDG , EDG i, where VDG = At(P ) and EDG = {(a, b) | a ∈ H(r), b ∈ B(r) ∪ (H(r) \ {a}), r ∈ P }. The SCCs of P , denoted SCC (P ), are the SCCs of DG(P ), and the supergraph of P is the graph SG(P ) = hVSG , ESG i, where VSG = SCC (P ) and ESG = {(C, C 0 ) | C 6= C 0 ∈ SCC (P ), ∃a ∈ C, ∃b ∈ C 0 , (a, b) ∈ EDG }. Note that SG(P ) is a directed acyclic graph (dag); recall that a topological ordering of a dag G = hV, Ei is an ordering v1 , v2 , ..., vn of its vertices, denoted ≤, such that for every (vi , vj ) ∈ E we have i > j. Such an ordering always exists, and the set O(G) of all topological orderings of G is nonempty. We thus define Definition 4 Let P be a program and let ≤ = (C1 , ..., Cn ) be a topological ordering of SG(P ). Then the splitting sequence induced by ≤ is S≤ = (S1 , ..., Sn ), where S1 = C1 and Sj = Sj−1 ∪ Cj , for j = 2, ..., n. We call any such S≤ a SCC -splitting sequence; note that S≤ is indeed a splitting sequence of P . We now have the following result. Theorem 3 Let P be a constraint-free program. For every ≤, ≤0 ∈ O(SG(P )), we have SEQ S≤ (P ) = SEQS≤0 (P ). This result allows to define the SCC -models of P as M SCC (P ) = SEQ S≤ (P ) for an arbitrary topological ordering of SG(P ). We then obtain: Proposition 1 The SCC -models semantics, given by M SCC (P ) for constraint-free P , satisfies (D1)-(D3). Example 5 Consider P = {a ← c, not a; a ← not b; c ← not d; b ← not e}; its SCCs are C1 = {a}, C2 = {b}, C3 = {c}, C4 = {d} and C5 = {e}. For ≤ = (C4 , C5 , C3 , C2 , C1 ), we obtain that SEQ S≤ (P ) = SEQ (S2 ,S3 ,S4 ,S5 ) (P S1 (∅, ∅)) = SEQ (S3 ,S4 ,S5 ) (P1S2 (∅, ∅)) = SEQ (S4 ,S5 ) (P2S3 (c, c)) = SEQ (S5 ) (P3S4 (bc, bc)) = {(bc, abc)}; hence M SCC (P ) = {(bc, abc)}. For ≤0 = (C5 , C2 , C4 , C3 , C1 ), we obtain SEQ S≤0 (P ) = {(bc, abc)}, in line with Theorem 3. Note that SEQ(P ) = {(bc, abc), (b, bd), (ac, ace)}. 0 Finally, if we replace in Equation (4) SEQ, SEQ S , and SEQ S all by M SCC , then the resulting equation holds; i.e., we can compute SCC -models modularly bottom up along an arbitrary splitting sequence (using always M SCC ). 4.2 MJC -split sequences and models Theorem 3 fails if we allow constraints in P . E.g., P = {b; ← b, not a} has the SCCs {a} and {b}; hence O(SG(P )) = {({a}, {b}), ({b}, {a})}. But the respective SEQ-models are different: SEQ ({a},{a,b}) (P ) = ∅ and SEQ ({b},{a,b}) (P ) = {(b, ba)}. We thus consider merging SCCs of P in such a way that independence of topological orderings is preserved and merging is done only if deemed necessary. This is embodied by the maximal joinable components of P , which lead to so called MJC -split sequences and models. Informally, relevant SCCs are merged if they intersect with a constraint. We call (K1 , K2 ) from SCC (P )2 a related pair, if either K1 = K2 or some constraint r ∈ P fulfills At(r) ∩ K1 6= ∅ and At(r) ∩ K2 6= ∅; by C(K1 ,K2 ) (P ) we denote the set of all such constraints. A related pair (K1 , K2 ) is a joinable pair iff K1 = K2 or some (C1 , . . . , Cn ) in O(SG(P )) exists such that (i) K1 = Cs and K2 = Cs+1 for some 1 ≤ s < n, (ii) (K2 , K1 ) ∈ / ESG and (iii) there exists r ∈ C(K1 ,K2 ) (P ) s.t. At(r) ⊆ C1 ∪ ... ∪ Cs+1 . We denote by JP (P ) the set of all joinable pairs. We extend joinability from pairs to any number of SCCs. Definition 5 Let P be a program. Then K1 , ..., Km ∈ SCC (P ) are joinable iff m = 2 and some K ∈ SCC (P ) exists such that (K1 , K), (K, K2 ) ∈ JP (P ),Sor other- m wise Ki , Kj are joinable for each i, j = 1, ..., m. We let JC(P ) = { i=1 Ki | K1 , ..., Km ∈ SCC (P ) are joinable} and call MJC (P ) = {J ∈ JC(P ) | ∀J 0 ∈ JC(P ) : J 6⊂ J 0 } the set of all maximal joined components (MJC s) of P . Example 6 For P = {← b, not a; ← b, not c; d ← not a; c ← not e; b ← c}, we have SCC (P ) = {{a}, {b}, {c}, {d}, {e}}. We note that ({c}, {b}) is a related, but not a joinable pair, since ({c}, {b}) satisfies (i) and (iii), but not (ii). Whereas ({a}, {b}) is the only nontrivial joinable pair; hence M JC(P ) = {{a, b}, {c}, {d}, {e}}. We define the MJC graph of P as JG(P ) = hVJG , EJG i, where VJG = MJC (P ) and EJG = {(J, J 0 ) | J 6= J 0 ∈ MJC (P ), ∃a ∈ J, ∃b ∈ J 0 , (a, b) ∈ EDG }. Note that JG(P ) is like SG(P ) a dag, and hence admits a topological ordering. We thus define Definition 6 Let P be a program and ≤ = (J1 , ..., Jm ) be a topological ordering of JG(P ). Then the splitting sequence induced by ≤ is S≤ = (S1 , ..., Sm ), where S1 = J1 and Sk = Sk−1 ∪ Jk , for k = 2, . . . , m. The sequence S≤ is again indeed a splitting sequence, which we call a MJC -splitting sequence. We obtain a result analogous to Theorem 3, but in presence of constraints. Theorem 4 For every program P and ≤, ≤0 ∈ O(JG(P )), we have SEQ S≤ (P ) = SEQS≤0 (P ). Similarly as SCC -models, we thus can define the MJC -models of P as M MJC (P ) = SEQ S≤ (P ) for an arbitrary topological ordering ≤ of JG(P ). The problem in Sec- tion 4.2 disappears when we use the MJCs. The program P = {← b, not a; b} there has the single MJC J = {a, b}, since the two SCCs {a} and {b} are related through the constraint ← b, not a and thus joinable. Therefore we get (b, ab) as the (single) MJC -model of P . As for the desiderata, we note: Proposition 2 The MJC -models semantics, given by M MJC (P ) for any program P , satisfies (D1)-(D2). Table 1. Complexity of split SEQ-models (completeness results). The same results hold for canonical models (SCC -, MJC -split seq. S); diverging results for SEQ-models are in brackets. Problem / Program P : normal, strat. normal, disj. stratified, headcycle-free disjunctive (MCH) Model checking: (X, Y ) ∈ SEQS (P )? coNP Π2p (INF) Brave reasoning: P |=b,v S a? Σ2p Σ3p Cautious reasoning: P |=c,v S a? Π2p Π3p (CON) Existence: SEQ S (P ) 6= ∅ ? Σ2p [ NP ] Σ3p [ NP ] Classical coherence (D3), however, is not ensured by MJC -models, due to lean component merging that fully preserves dependencies. Example 7 (cont’d) Reconsider P in Ex. 6. Then for the ordering ≤= ({a}, {d}, {e}, {c}, {b}) we obtain SEQ S≤ (P ) = ∅, while for ≤0 = ({e}, {c}, {b}, {a}, {d}) we obtain SEQ S≤0 (P ) = {(bc, abc)}. On the other hand, JG(P ) has the single topo- logical ordering ≤= ({e}, {c}, {a, b}, {d}), and SEQ S≤ (P ) = {(bc, abc)}; hence M MJC (P ) = {(bc, abc)}. Note that SEQ(P ) = {(bc, abc), (d, de)}. 5 Complexity and Computation In this section, we consider the computational complexity of the following major reason- ing tasks for programs under split SEQ-semantics. (MCH) Given a program P , a splitting sequence S and an HT-interpretation (X, Y ), decide whether (X, Y ) is a split semi-equilibrium model of P . (INF) Given a program P , a splitting sequence S, an atom a and v ∈ {t, f , bt}, decide if a is a brave [resp. cautious] SEQ S -consequence of P with value v, denoted P |=b,v c,v S S a [resp. P |=S a], i.e., a has in some (all) (X, Y ) ∈ SEQ (P ) value v. (CON) Given a program P and a splitting sequence S, decide whether SEQ S (P ) 6= ∅. We consider also SCC - and MJC -splitting sequences and several classes of pro- grams, viz. normal, disjunctive, stratified, and headcycle-free programs.Recall that a program P is stratified, if for each r ∈ P and C ∈ SCC (P ) either H(r) ∩ C = ∅ or B − (r) ∩ C = ∅; P is headcycle-free (hcf), if |H(r) ∩ C| ≤ 1 for each r ∈ P and C ∈ SCC (P 0 ), where P 0 = {a ← B + (r) | r ∈ P, a ∈ H(r)}. Positive programs are here of less interest, as SEQ S (P ) = {(M, M ) | M ∈ MM (P )} for each splitting sequence S. Our complexity results are summarized in Table 1. Constructing and recognizing canonical splitting sequences. It is well-known that SCC (P ) and SG(P ) are efficiently computable from P (using Tarjan’s [16] algorithm even in linear time); hence, it is not hard to see that one can recognize a SCC -splitting sequence S in polynomial time, and that every such S can be (nondeterministically) generated in polynomial time (in fact, in linear time). We obtain similar tractability results for MJC (P ) and M JC-splitting sequences. Theorem 5 Given a program P , M JC(P ) and JG(P ) are computable in polynomial time (in time O(cs·kP k), where cs = |{r ∈ P | H(r) = ∅}| and kP k is the size of P ). 6 Application: Inconsistency-Tolerant Query Answering The standard answer set semantics may be regarded as appropriate when a knowledge base, i.e., logic program, is properly specified adopting the CWA principle to deal with incomplete information. Query answering over a knowledge base then resorts usually to brave or cautious inference from the answer sets of a knowledge base; let us focus on the latter here. However, if (unexpected) incoherence arises, then we lose all information and query answers are trivial. This, however, may not be satisfactory, especially if it is not possible to modify the knowledge base, which may be due to various reasons. Paracoherent semantics can be exploited to overcome this problem and to render query answering operational, without trivialization. In particular, SEQ-semantics is attractive as it builds on simple grounds and (1) brings in “unsupported” assumptions, (2) stays in model building close to answer sets, but distinguishes atoms that require such assumptions from atoms derivable without them, (3) keeps the CWA/LP spirit of minimal assumptions, and (4) easily lifts to extensions (nested programs, arbitrary formulas, aggregates, etc). For instance, consider a variant of the Russell paraphrase from the Introduction [15]: P = {shaves(joe, X ) ← not shaves(X , X ); man(paul )}. While this program has no answer set, SEQ-semantics gives us the model ({shaves(joe, paul ), man(paul )}, {shaves(joe, paul ), man(paul ), shaves(joe, joe)}); here the incoherent rule shaves(joe, joe) ← not shaves(joe, joe) obtained by ground- ing is isolated from rest of the program, avoiding the absence of solutions (a similar intu- ition is underlying the definition of CWA inhibition rule in [12], used for contradiction removal in a logic program), and allows us to derive, for instance, that shaves(joe, paul ) and man(paul ) are true; furthermore, we can infer that shaves(joe, joe) can not be false. Such a capability seems very attractive in query answering. Now reconsider the program in Ex. 1, and let us ask for query go(John). Again answer set semantics yields only a trivial answer to the query. However the local inco- herence is due to the second and the third rule, and the CWA implies that go(Mark ) is false; hence there is no reason to avoid the answer. Moreover split-SEQ semantics yields the unique model ({go(John)}, {go(John), go(Bill )}) and removes the SEQ-model ambiguity, as it makes stronger gap minimization through the bottom-up evaluation. In this way, the relaxation of CWA is minimized. 7 Conclusion We have studied a refinement of SEQ-semantics that respects modular structure, and we gave a semantics via splitting sets that is amenable to bottom up evaluation of programs. The generic framework of Equilibrium Logic makes it easy to define SEQ-semantics via gap minimization for many extensions of the programs considered here, such as nested programs, programs with aggregates and external atoms, hybrid knowledge bases etc; programs with classical negation require to use more truth values [8]. It remains to consider modularity in these extensions and to define suitable refinements of SEQ- models. Particularly interesting are modular logic programs where explicit (by module encapsulation) and implicit modularity (by splitting sets) occur at the same time. Besides language extensions, another issue is generalizing the model selection. To this end, preference of gap minimization at higher over lower levels must be supported; however, this intuitively requires more guessing and hinders bottom up evaluation. Finally, efficient algorithms and an implementation are to be done, as well integration into an answer set building framework. References 1. Alcântara, J., Damásio, C.V., Pereira, L.M.: A declarative characterization of disjunctive paraconsistent answer sets. In: Proc. ECAI-04. pp. 951–952. IOS Press (2004) 2. Blair, H.A., Subrahmanian, V.S.: Paraconsistent logic programming. Theor. Comput. Sci. 68(2), 135–154 (1989) 3. Eiter, T., Fink, M., Moura, J.: Paracoherent answer set programming. In: F. Lin, U. Sattler and M. Truszcyński (eds.), Proc. KR-10, May 9-13, 2010, Toronto, Canada. pp. 486–496. AAAI Press (2010) 4. Eiter, T., Leone, N., Saccà, D.: On the partial semantics for disjunctive deductive databases. Ann. Math. & Artif. Intell. 19(1/2), 59–96 (1997) 5. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 365–385 (1991) 6. Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussis- chen Akademie der Wissenschaften 16(1), 42–56 (1930) 7. Lifschitz, V., Turner, H.: Splitting a logic program. In: Proc. ICLP-94. pp. 23–38. MIT-Press (1994) 8. Odintsov, S.P., Pearce, D.: Routley semantics for answer sets. In: Proc. LPNMR-05. LNCS 3662, pp. 343–355. Springer (2005) 9. Osorio, M., Ramı́rez, J.R.A., Carballido, J.L.: Logical weak completions of paraconsistent logics. J. Log. Comput. 18(6), 913–940 (2008) 10. Pearce, D.: Equilibrium logic. Ann. Math. & Artif. Intell. 47(1-2), 3–41 (2006) 11. Pearce, D., Valverde, A.: Quantified equilibrium logic and foundations for answer set pro- grams. In: Proc. ICLP-08. LNCS 5366, pp. 546–560. Springer (2008) 12. Pereira, L.M., Alferes, J.J., Aparı́cio, J.N.: Contradiction removal semantics with explicit negation. In: Logic at Work. LNCS 808, pp. 91–105. Springer (1992) 13. Pereira, L.M., Pinto, A.M.: Revised stable models - a semantics for logic programs. In: Proc. EPIA-05. LNCS 3808, pp. 29–42. Springer (2005) 14. Przymusinski, T.: Stable semantics for disjunctive programs. New Generation Computing 9, 401–424 (1991) 15. Sakama, C., Inoue, K.: Paraconsistent stable semantics for extended disjunctive programs. J. Log. Comput. 5(3), 265–285 (1995) 16. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972) 17. van Gelder, A., Ross, K., Schlipf, J.: The well-founded semantics for general logic programs. J. ACM 38(3), 620–650 (1991) 18. You, J.H., Yuan, L.: A three-valued semantics for deductive databases and logic programs. J. Comput. Syst. Sci. 49, 334–361 (1994)