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 paracoherent 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.
Answer set programming is a popular formalism in logic programming (LP). The answer
set semantics [
In order to avoid trivialization of reasoning from such programs, Inoue and Sakama
[
In a similar vein, we can regard many semantics for non-monotonic logic programs
that relax answer sets as paracoherent semantics, e.g. [
However, only few paracoherent semantics satisfy all three desiderata (cf. [
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: P = <8 ggoo((PJeothenr )) gnoo(tJgooh(nM);anrkot);go(Bill ); =9
: go(Bill ) go(Peter ) ;
Then P has no answer set; its semi-equilibrium models (a subset of HT-models) are M1 = (;; fgo(Mark )g), and M2 = (fgo(John)g; fgo(John); go(Bill )g). 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 [
The refined semantics (SCC -models) lends for a modular use and bottom up evaluation of programs. Cautious merging of components (MJC -models) aims at preserving independence and possible parallel evaluation. So this semantics is attractive for incorporation into answer set evaluation frameworks, in order to add paracoherent features. 2
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 [
A (disjunctive logic) program P is a finite set of disjunctive rules. P is called normal [resp. positive] if each r 2 P is normal [resp. positive]. We let At(P ) = Sr2P At(r).
Any set I is an interpretation; it is a model of a program P (denoted I j= P ) iff
for each rule r 2 P , I \ H(r) 6= ; if B+(r) I and B (r) \ I = ; (denoted I j= 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 2 MM (P I ), where P I is
the well-known Gelfond-Lifschitz reduct [
sets due to cyclic dependency of atoms among each other by rules through negation
incoherent (cf. Russel’s paradox). The semi-equilibrium semantics [
In particular, (X; Y ) j= :a iff a 2= Y , and (X; Y ) j= r for a rule r of form (2) iff either fa1 : : : ; akg \ X 6= ;, fb1; : : : ; bmg 6 Y , or fbm+1; : : : ; bng \ Y 6= ;. A HT-interpretation (X; Y ) is an HT-model of a theory (i.e., a set of formulas) , denoted (X; Y ) j= iff (X; Y ) j= for each 2 . It is an equilibrium (EQ ) model of iff X = Y and for every X 0 Y it holds that (X 0; Y ) 6j= .
As shown by Pearce [
Example 2 Consider the program P = fa b; b not ag. 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 ) = f(;; a)g. 3
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 = fc b; not c; b not ag; then SEQ (P ) = f (b; bc); (;; a)g. Here (b; bc) is more appealing than (;; a) because a is not derivable, as no rule has a in the head. Moreover, intuitively, P1 = fb not ag is a lower (coherent) part feeding into the upper part P2 = fc b; not cg.
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) ’j=’ 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 [
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 n bS (P ) [ fa j a 2 Ig [ f not a j a 2 J g [ f a j a 2 S n J g:
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 ).
set of a program P . Then the semi-equilibrium models of P related to S are defined as SEQ S (P ) = mc
[ (I;J)2SEQ(bS(P ))
SEQ(P S (I; J )) : (3) Example 4 (cont’d) For the splitting set S = fa; bg of P in Example 3, bS (P ) = fb not ag and SEQ (bS (P )) = f(b; b)g. Hence, P S (b; b) = fc b; not c; b; not b; ag and SEQ S (P ) = SEQ(P S (b; b)) = f(b; bc)g.
For any HT-model (X; Y ) and splitting set S of a program P , we define the restriction of (X; Y ) to S as (X; Y )jS = (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 ) 2 SEQS (P ) iff (X; Y ) 2 SEQ(P ) and (X; Y )jS 2 SEQ(bS (P )).
Now we generalize the use of splitting sets to compute the SEQ -models of a program via splitting sequences.
ting sequence S = (S1; : : : ; Sn) for a program P , we let S0 = (S2; :::; Sn) and define the semi-equilibrium models of P related to the splitting sequence S = (S1; :::; Sn) as SEQS (P ) = mc [
SEQS0 (P S1 (I; J )) : (4) (I;J)2SEQ(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 splitting sequence S = (S1; :::; Sn), we let P0 = P and Pk = (Pk 1)Sk (Ik; Jk), where (Ik; Jk) 2 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 ) 2 SEQ S (P ) iff (X; Y ) 2 SEQ (P ) and (X; Y )jSk 2 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 = f b; b not ag and S = fag, then SEQ(bS (P )) = f(;; ;)g and so SEQS (P ) = ;. However (a; a) and (;; a) are HT-models of P .
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.
Recall that the dependency graph of a program P is the directed graph DG(P ) = hVDG; EDGi, where VDG = At(P ) and EDG = f(a; b) j a 2 H(r); b 2 B(r) [ (H(r) n fag); r 2 P g. The SCCs of P , denoted SCC (P ), are the SCCs of DG(P ), and the supergraph of P is the graph SG(P ) = hVSG; ESGi, where VSG = SCC (P ) and ESG = f(C; C0) j C 6= C0 2 SCC (P ); 9a 2 C; 9b 2 C0; (a; b) 2 EDGg. 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 ) 2 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.
sequence of P . We now have the following result. is indeed a splitting Theorem 3 Let P be a constraint-free program. For every ; 02 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 = fa c; not a; a not b; c not d; b not eg; its SCCs are C1 = fag, C2 = fbg, C3 = fcg, C4 = fdg and C5 = feg. 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)) = f(bc; abc)g; hence M SCC (P ) = f(bc; abc)g. For 0= (C5; C2; C4; C3; C1), we obtain SEQ S 0 (P ) = f(bc; abc)g, in line with Theorem 3. Note that SEQ (P ) = f(bc; abc); (b; bd); (ac; ace)g.
Finally, if we replace in Equation (4) SEQ , SEQ S , and SEQ S0 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 ). Theorem 3 fails if we allow constraints in P . E.g., P = fb; b; not ag has the SCCs fag and fbg; hence O(SG(P )) = f(fag; fbg), (fbg; fa ) . But the respective g g SEQ -models are different: SEQ (fag;fa;bg)(P ) = ; and SEQ (fbg;fa;bg)(P ) = f(b; ba)g. 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 2 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) 2= ESG and (iii) there exists r 2 C(K1;K2)(P ) s.t. At(r) C1 [ ::: [ Cs+1. We denote by J P (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 2 SCC (P ) are joinable iff m = 2 and some K 2 SCC (P ) exists such that (K1; K); (K; K2) 2 J P (P ), or otherwise Ki; Kj are joinable for each i; j = 1; :::; m. We let J C(P ) = f Sim=1 Ki j K1; :::; Km 2 SCC (P ) are joinableg and call MJC (P ) = fJ 2 J C(P ) j 8J 0 2 J C(P ) : J 6 J 0g the set of all maximal joined components (MJC s) of P . Example 6 For P = f b; not a; b; not c; d not a; c not e; b cg, we have SCC (P ) = ffag; fbg; fcg; fdg; fegg. We note that (fcg; fbg) is a related, but not a joinable pair, since (fcg; fbg) satisfies (i) and (iii), but not (ii). Whereas (fag; fbg) is the only nontrivial joinable pair; hence M J C(P ) = ffa; bg; fcg; fdg; fegg.
We define the MJC graph of P as J G(P ) = hVJG; EJGi, where VJG = MJC (P ) and EJG = f(J; J 0) j J 6= J 0 2 MJC (P ); 9a 2 J; 9b 2 J 0; (a; b) 2 EDGg. Note that J G(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 J G(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 SEQS 0 (P ).
; 02 O(J G(P )), we have SEQ S (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 J G(P ). The problem in Section 4.2 disappears when we use the MJCs. The program P = f b; not a; bg there has the single MJC J = fa; bg, since the two SCCs fag and fbg 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).
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 = (fag; fdg; feg; fcg; fbg) we obtain SEQ S (P ) = ;, while for 0= (feg; fcg; fbg; fag; fdg) we obtain SEQ S 0 (P ) = f(bc; abc)g. On the other hand, J G(P ) has the single topological ordering = (feg; fcg; fa; bg; fdg), and SEQ S (P ) = f(bc; abc)g; hence M MJC (P ) = f(bc; abc)g. Note that SEQ(P ) = f(bc; abc); (d; de)g. 5
In this section, we consider the computational complexity of the following major reasoning 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 2 ft; f ; btg, decide if a is a brave [resp. cautious] SEQ S -consequence of P with value v, denoted P j=bS;v a [resp. P j=cS;v a], i.e., a has in some (all) (X; Y ) 2 SEQS (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 programs, viz. normal, disjunctive, stratified, and headcycle-free programs.Recall that a program P is stratified, if for each r 2 P and C 2 SCC (P ) either H(r) \ C = ; or B (r) \ C = ;; P is headcycle-free (hcf), if jH(r) \ Cj 1 for each r 2 P and a B+(r) j r 2 P; a 2 H(r)g. Positive programs aCre2heSrCeCof(lPes0s),inwtehreerset,Pa0s S=EfQ S (P ) = f(M; M ) j M 2 MM (P )g for each splitting sequence S. Our complexity results are summarized in Table 1.
SCC (P ) and SG(P ) are efficiently computable from P (using Tarjan’s [
Theorem 5 Given a program P , M J C(P ) and J G(P ) are computable in polynomial time (in time O(cs kP k), where cs = jfr 2 P j H(r) = ;gj and kP k is the size of P ). 6
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 [
not shaves(X ; X ); man(paul )g.
While this program has no answer set, SEQ -semantics gives us the model
(fshaves(joe; paul ); man(paul )g; fshaves(joe; paul ); man(paul ); shaves(joe; joe)g);
here the incoherent rule shaves(joe; joe) not shaves(joe; joe) obtained by
grounding is isolated from rest of the program, avoiding the absence of solutions (a similar
intuition is underlying the definition of CWA inhibition rule in [
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 incoherence 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 (fgo(John)g; fgo(John); go(Bill )g) 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
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 [
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.