Compute Paracoherent Answer Sets via Saturation

Abstract

Answer Set Programming (ASP) is a well-established formalism for nonmonotonic reasoning. Paracoherent semantics for ASP have been suggested as a remedy, to handle cases in which no answer set exists due to the usage of cyclic default negation. In this paper we present a reduction of the task of computing a paracoherent answer set in the one of computing a stable model of a plain ASP program. The strategy is based on a direct encoding of a paracoherent semantics in plain ASP, which works on normal (i.e., non-disjunctive) ASP programs. This encoding is based on the traditional epistemic transformation and on the so-called saturation technique that is basically used to simulate a coNP check with the standard stable model check.

Keywords

• Logic Programming Answer Set Programming Paracoherent Reasoning Semi-Equilibrium Models

1 Introduction

Answer Set Programming (ASP) [ 17, 20, 16 ] is a well-established formalism for nonmonotonic reasoning, with a robust solving technology [ 18, 21–24, 29, 9, 13–15, 32, 31 ]. ASP can model in a natural declarative way, usually NP-hard, combinatorial problems by encoding them as a logic program and computing its answer sets, which encode the problem solutions. The availability of efficient solvers made possible the development of a large variety of applications to Artificial Intelligence [ 27, 26, 8, 5, 4 ], Databases [ 30 ], Game Theory [ 12 ], Information Extraction [ 1 ], including industrial ones [ 28 ]. It is known that there are some circumstances, arising in presence of cyclic definitions that involve negation as failure, some logic programs have no answer sets. While this is sometimes desired for encoding problems that admit no solutions, it is sometimes perceived as detrimental, especially when dealing with query answering. Addressing this issue, paracoherent semantics based on answer sets have been proposed to draw meaningful conclusions also from incoherent programs [ 3, 11, 10 ]. The term paracoherent has been chosen to highlight both similarities and differences to paraconsistent semantics: their goal is similar, but the latter addresses classical logical contradictions, while the former addresses contradictions due to unstratified (“cyclic”) negation.

Practical applications of these paracoherent semantics hinge on the availability of efficient algorithms and implementations [ 6, 7 ]. There is a vast potential of applications, the most immediate ones being debugging of ASP and incoherence-tolerant query answering. But also applications in diagnosis, planning, and reasoning about actions are conceivable [ 10 ].

In this paper we present a reduction of the task of computing a paracoherent answer set in the one of computing a stable model of a plain ASP program. The strategy is based on a direct encoding of a paracoherent semantics in plain ASP, which works on normal (i.e., non-disjunctive) ASP programs. This encoding is based on the traditional epistemic transformation and on the so-called saturation technique that is basically used to simulate a coNP check with the standard stable model check. The proposed encoding provides both an alternative proof of the complexity bounds of the task of computing paracoherent answer sets, and might be used to implement a paracoherent ASP solver just running an ASP solver. 2

Preliminaries

We start with recalling answer set semantics, and then present the paracoherent semantics of semi-stable and semi-equilibrium models. Finally, we conclude this section recalling computational complexity 2.1

Answer Set Programming

We concentrate on logic programs over a propositional signature S . A disjunctive rule r is of the form a1 _ _ al b1; :::; bm; not c1; :::; not cn; (1) where all ai, b j, and ck are atoms (from S ); l; m; n 0, and l + m + n > 0; not represents negation-as-failure. The set H(r) = fa1; :::; al g is the head of r, while B+(r) = fb1; :::; bmg and B (r) = fc1; : : : ; cng 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. A rule r is a fact, if B(r) = 0/ (we then omit ); a constraint, if H(r) = 0/ ; normal, if jH(r)j 1 and positive, if B (r) = 0/ . 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), that is the set of all atoms occurring in the program P.

Any set I S is an interpretation; it is a model of a program P (denoted I j= P) if and only if for each rule r 2 P, I \ H(r) 6= 0/ if B+(r) I and B (r) \ I = 0/ (denoted I j= r). A model M of P is minimal, if and only if no model M0 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(PI ), where PI is the well-known Gelfond-Lifschitz reduct [ 25 ] of P with respect to I, i.e., the set of rules a1 _ ::: _ al b1; :::; bm, obtained from rules r 2 P of form (1), such that B (r) \ I = 0/ . Finally, we say that a program P is consistent, if it admits some model, otherwise it is inconsistent; whereas it is coherent, if it admits some answer set (i.e., AS(P) 6= 0/ ), otherwise, it is incoherent.

Example 1. Consider the following logic program

P = fa not b; b c; not d; c

ag: For instance, a model of P is fb; dg. Then, P is consistent. Moreover, the set of all minimal models of P is given by MM(P) = ffbg; fa; c; dgg. However, P is incoherent. Indeed, Pfbg = fb c; c ag, but fbg is not a minimal model of Pfbg; and Pfa;c;dg = fa; c ag, but fa; c; dg is not a minimal model of Pfa;c;dg. 2.2

Paracoherent ASP

Here, we introduce two paracoherent semantics that allow for keeping a system responsive when a logic program has no answer set due to cyclic default negation. These semantics satisfy three desiderata properties identified by [ 10 ] and used also in other contexts [ 2 ].

Semi-Stable Models. Inoue and Sakama [ 33 ] introduced semi-stable model semantics. We consider an extended signature S k = S [ fKa j a 2 S g. Intuitively, Ka can be read as a is believed to hold. Semantically, we resort to subsets of S k as interpretations Ik and the truth values false ?, believed true bt, and true t. where ? bt t. The truth value assigned by Ik to a propositional variable a is defined by 8 t if a 2 Ik ; > Ik (a) = <

bt if Ka 2 Ik and a 62 Ik ; >: ? otherwise: The semi-stable models of a program P are obtained from its epistemic k-transformation Pk .

Definition 1 (Epistemic k-transformation Pk ). Let P be a program. Then its epistemic k-transformation is defined as the program Pk obtained from P by replacing each rule r of the form (1) in P, such that B (r) 6= 0/ , with: lr;1 _ : : : _ lr;l _ Kc1 _ : : : _ Kcn ai lr;i b1; : : : ; bm; lr;i; lr;i; c j; ai; lr;k; (2) (3) (4) (5) for 1 i; k l and 1 j

n, where the lr;i, lr;k are fresh atoms.

Note that for any program P, its epistemic k-transformation Pk is positive. For every interpretation Ik over S 0 S k , let G (Ik ) = fKa 2 Ik j a 62 Ik g denote the atoms believed true but not assigned true, also referred to as the gap of Ik . Given a set F of interpretations over S 0, an interpretation Ik 2 F is maximal canonical in F , if no Jk 2 F exists such that G (Ik ) G (Jk ). By mc(F ) we denote the set of maximal canonical interpretations in F . Semi-stable models are then defined as maximal canonical interpretations among the answer sets of Pk . Then we can equivalently paraphrase the definition of semi-stable models in [ 33 ] as follows. Definition 2 (Semi-stable models). Let P be a program over S . An interpretation Ik over S k is a semi-stable model of P, if Ik = S \ S k for some maximal canonical answer set S of Pk . The set of all semi-stable models of P is denoted by SST (P), i.e., SST (P) = fS \ S k j S 2 mc(AS(Pk ))g.

Example 2. Consider the program

Its epistemic k -transformation is

P = fb not a; c not b; a

c; d Pk = 8 l1 _ Ka; b > >< l2 _ Kb; c

a c; > >: l3 _ Kd; d l1; l2; l3; a; l1; l1 b; l2; l2 d; l3; l3 not dg. b; l1; 9

> c; l2; => > > d; l3 ; , which has the answer sets M1 = fKa; Kb; Kdg, M2 = fl1; b; Kb; Kdg, and M3 = fKa; l2; a; c; Kdg. Since G (M1) = fKa; Kb; Kdg, G (M2) = fKdg, and G (M3) = fKdg, among them M2 and M3 are maximal canonicals. Hence, M2 \ S k = fb; Kb; Kdg and M3 \ S k = fa; c; Ka; Kdg are semi-stable models of P.

Semi-Equilibrium Models. Semi-equilibrium models were introduced by [ 10 ] to avoid some anomalies in semi-stable model semantics concerning properties of modal logic. Like semi-stable models, semi-equilibrium models may be computed as maximal canonical answer sets, of an extension of the epistemic k -transformation.

Definition 3 (Epistemic HT -transformation PHT ). Let P be a program over S . Then its epistemic HT -transformation PHT is defined as the union of Pk with the set of rules: Ka

a; Ka1 _ : : : _ Kal _ Kc1 _ : : : _ Kcn

Kb1; : : : ; Kbm; (6) (7) for a 2 S , respectively for every rule r 2 P of the form (1).

Definition 4 (Semi-equilibrium models). Let P be a program over S , and let Ik be an interpretation over S k . Then, Ik 2 SEQ(P) if, and only if, Ik 2 fM \ S k j M 2 mc(AS(PHT ))g, where SEQ(P) is the set of semi-equilibrium models of P. Example 3. Consider the program P of Example 2. Its epistemic HT -transformation is PHT = Pk [

Ka a; Kb b; Kc Kb _ Ka; Kc _ Kb; Ka c; Kd Kc; Kd d; Kd which has the answer sets fKa; Kb; Kdg, fl1; b; Kb; Kdg, and fKa; l2; a; c; Kc; Kdg. Therefore, the semi-equilibrium models of P are fb; Kb; Kdg and fa; c; Ka; Kc; Kdg.

In the following, we refer to semi-stable models or semi-equilibrium models as paracoherent answer sets. We conclude this preliminary section with some useful observations concerning the computational complexity of the computation of a paracoherent answer set. Reasoning tasks Checking Brave inference Cautious inference Existence

Normal ASP programs ASP SST /SEQ

P coNP-c NP-c S2p-c coNP-c P2p-c NP-c NP-c

Disjunctive ASP programs

ASP SST /SEQ coNP-c P2p-c S2p-c S3p-c P2p-c P3p-c S2p-c NP-c The complexity of various reasoning tasks with paracoherent answer sets has been analyzed in [ 10 ]. Determining the existence of paracoherent answer sets is NP-complete (it is sufficient to test for existence of classical models). Paracoherent answer set checking is P2P-complete, leading to S3P-completeness for brave, and P3P-completeness for cautious reasoning in case of disjunctive ASP programs; while paracoherent answer set checking is coNP-complete, leading to S2P-completeness for brave, and P2P-completeness for cautious reasoning in case of normal ASP programs. These results are summarized in Table 2.3, where results for answer set semantics are also reported.

In this paper, we consider the computation of one paracoherent answer set, which is a functional problem. From previous work it is clear that this task is in FS3P for disjunctive ASP programs, and actually in FQ3P (functional polynomial time with a logarithmic number of calls to a S2P-complete oracle), because for computing one paracoherent answer set it is sufficient to solve a cardinality-optimization problem. Hence, this task is in FS2P for normal ASP programs, and actually in FQ2P (functional polynomial time with a logarithmic number of calls to an NP-complete oracle). 3

Saturation technique

In this section, we introduce an encoding for the computation of paracoherent answer sets based on saturation. Clearly, by computational complexity results, this encoding into a standard answer set program works only for normal ASP programs.

Let P be a normal ASP program. We consider the epistemic transformation program extended with the gap atoms P = Pc [ Pg. Then, we build an answer set program P 0 as follows. First, starting from P , we build a positive program, replacing each occurrence of an atom a with a fresh atom xa, and each occurrence of a negated atom not a with a fresh atom na. More formally, given a fresh atom w, for each rule r 2 P of the form (1), we build a rule, named W (r), of the form w na1; : : : ; nal ; xb1; : : : ; xbm; nc1; : : : ; ncn: (8) Let W (P ) = SfW (r)jr 2 P g be the set of all rules of the form (8). Then, given a rule r 2 P such that jH(r)j > 1, for each atom ai appearing in the head of r, we consider ncair ncair ncair xa j; nb j; xc j; xb j nc j cair; cair; 8 j = 1; : : : ; i 1; i + 1; : : : ; m; 8 j = 1; : : : ; m; 8 j = 1; : : : ; n: 8 j = 1; : : : ; m; 8 j = 1; : : : ; n: two fresh atoms, namely cair and ncair, and we build the following set of rules: cair na1; : : : ; nai 1; nai+1; : : : ; nal ; xb1; : : : ; xbm; nc1; : : : ; ncn; (9) (10) (11) (12) (13) (14) (15) Moreover, whenever B(r) 6= 0/ , we also consider the following set of rules: We denote by C(r; ai) the set of rules of the form (9), (10), (11), (12), (13), and (14). Note that in case of B(r) = 0/ , then C(r; ai) contains only rules of the form (9), (10), (11), and (12). We denote by crules(a) the set of all rules r of P such that a occurs in the head of r and jH(r)j > 1. Then, for each atom a 2 P , we construct the following rule (denoted by C(a)): w

xa; fncar : r 2 crules(a)g: Note that, whenever crules(a) = 0/ , the rule of the form (15) will be w xa. Now, let C(P ) be the set of all rules of the form C(r; ai) and C(a) that can be constructed from P . That is, C(P ) = SfC(r; ai) : ai 2 At(P ) and r 2 crules(ai)g [ SfC(a) : a 2 At(P )g. Then, for each atom a 2 At(P ), we construct a disjunctive rule of the form xa _ na: (denoted by D(xa)), and for each atom of the form cair 2 C(P ), we construct a disjunctive rule of the form cair _ ncair: (denoted by D(cair)). Hence, we set D(P ) = SfD(xa)ja 2 At(P )g [ SfD(cair)jcair 2 C(P )g. Finally, we consider the following program:

P 0 = W (P ) [ C(P ) [ D(P ).

Note that the program P 0 so constructed is a sort of completion of the original program P [ 19 ]. Therefore, the set of all answer sets of the positive program P 0 extended by the constraint w:, corresponds to the set of all answer sets of the original program P . More formally, by setting Mx = fa 2 At(P ) : xa 2 Mg and ASx(P 0) = fMx : M 2 AS(P 0)g, it holds that Theorem 1. Let P be a normal ASP program. Then, ASx(P 0 [ f w:g) = AS(P ).

Now, to minimize the gap atoms, we consider the following set of rules: Pcheck = 8 un(gap(Ka)) > >>> eq(gap(Ka)) < eq(gap(Ka)) >> w >>: w xgap(Ka); not gap(Ka); xgap(Ka); gap(Ka); ngap(Ka); not gap(Ka); un(gap(Ka)); feq(gap(Ka)) : a 2 At(P)g 8a 2 At(P); 9

> 8a 2 At(P); >>>

= 8a 2 At(P); 8a 2 At(P); >> > > ; Intuitively, the program Pcheck minimizes the gap atoms, by comparing any two answer sets of P . Indeed, the atom w is derived whenever the comparison shows that the set of the gap atoms of an answer set is not smaller (that is uncomparable or equal) than the set of the gap atoms of another answer set. Indeed, the first rule means that whenever a gap atom belongs to an answer set M0 of the completion P 0 (that mimics an answer set of the original program P , see Theorem 1), but that atom does not belong to another answer set M of the original program P , then the gap of M0 is uncomparable to the gap of M. In this case, we derive w from the fourth rule. Whereas, the fifth rule means that we derive w, if we have derived each atom of the form eq(gap(Ka)). These atoms can be derived by the third and the fourth rules, whenever the set of gap atoms of an answer set of P 0 is equal to the set of gap atoms of an answer set of P .

Finally, we consider the following set of rules (so-called saturation rules) which derive each new atom created in the construction of P 0 and Pcheck, whenever w is derived.

Psaturation = 8 a > >< un(gap(Ka))

eq(gap(Ka)) > > : w; w; w; not w 8a 2 At(P 0); 9

> 8a 2 At(P); => 8a 2 At(P); > > ; Note that, the last rule force to derive w to obtain an answer set, otherwise the program should be incoherent. Now, by considering Prew as the union of P , P 0, Pcheck, and Psaturation, there is a one-to-one correspondance between answer sets of Prew and paracoherent answer sets of P. More formally, Theorem 2. Let P be a normal program. Then, M 2 AS(Prew) implies M \ At(P) 2 PAS(P), and M0 2 PAS(P) implies M0 [ (At(Prew) n At(P)) 2 AS(Prew).

Intuitively, P 0 is a “copy” of P , and the program Pcheck compares any two answer sets of P (by comparing answer sets of P and P 0). Now, if M is an answer set of Prew, then w 2 M, and so each new atom occurring in P 0 and Pcheck belongs to M. Moreover, there is an answer set J of P contained into M. As M is an answer set, it is a minimal model of the reduct of Prew, that is P J [ P 0 [ PcJheck [ Psaturation n f not w:g. This means that the set of gap atoms of each other answer set of P and the set of gap atoms of J are uncomparable or equal. Otherwise, M should not be a minimal model of the reduct. Hence, the gap minimality property is satisfied by M, thus M \ At(P) is a paracoherent answer set of P. The same intuition also explains why M0 [ (At(Prew) n At(P)) is an answer set of Prew, whenever M0 is a paracoherent answer set of P. 4

Conclusion

Paracoherent semantics have been suggested as a remedy, which extend the classical notion of answer sets to draw meaningful conclusions also from incoherent programs. In this paper we presented an encoding of paracoherent answer set in plain ASP. The proposed encoding confirms (being usable in an alternative proof) the complexity bounds of the task of computing paracoherent answer sets, and might be used to implement a paracoherent ASP solver just running an ASP solver. As far as future work is concerned, we plan to test in an experimental analysis whether the encoding can be fruitfully employed for implementing an efficient paracoherent ASP solver.

References

1. Adrian , W.T., Manna , M. , Leone , N. , Amendola , G. , Adrian , M. : Entity set expansion from the web via ASP . In: ICLP (Technical Communications) . OASICS , vol. 58 , pp. 1 : 1 - 1 : 5 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik ( 2017 )

2. Alviano , M. , Amendola , G. , Pen˜aloza, R.: Minimal undefinedness for fuzzy answer sets . In: AAAI 2017 . pp. 3694 - 3700 ( 2017 )

3. Amendola , G.: Dealing with incoherence in ASP: split semi-equilibrium semantics . In: DWAI@AI*IA. CEUR Workshop Proceedings , vol. 1334 , pp. 23 - 32 . CEUR-WS.org ( 2014 )

4. Amendola , G.: Preliminary results on modeling interdependent scheduling games via answer set programming . In: RCRA@AI*IA . p. to appear. CEUR Workshop Proceedings, CEURWS.org ( 2018 )

5. Amendola , G.: Solving the stable roommates problem using incoherent answer set programs . In: RCRA@AI*IA . p. to appear. CEUR Workshop Proceedings, CEUR-WS.org ( 2018 )

6. Amendola , G. , Dodaro , C. , Faber , W. , Leone , N. , Ricca , F. : On the computation of paracoherent answer sets . In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9 , 2017 , San Francisco, California, USA. pp. 1034 - 1040 ( 2017 )

7. Amendola , G. , Dodaro , C. , Faber , W. , Ricca , F. : Externally supported models for efficient computation of paracoherent answer sets . In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, February 2-7 , 2018 , New Orleans, Louisiana, USA. pp. 1034 - 1040 ( 2018 )

8. Amendola , G. , Dodaro , C. , Leone , N. , Ricca , F. : On the application of answer set programming to the conference paper assignment problem . In: AI*IA. Lecture Notes in Computer Science , vol. 10037 , pp. 164 - 178 . Springer ( 2016 )

9. Amendola , G. , Dodaro , C. , Ricca , F. : ASPQ: an asp-based 2qbf solver . In: QBF@SAT. CEUR Workshop Proceedings , vol. 1719 , pp. 49 - 54 . CEUR-WS.org ( 2016 )

10. Amendola , G. , Eiter , T. , Fink , M. , Leone , N. , Moura , J.: Semi-equilibrium models for paracoherent answer set programs . Artif. Intell . 234 , 219 - 271 ( 2016 )

11. Amendola , G. , Eiter , T. , Leone , N.: Modular paracoherent answer sets . In: Logics in Artificial Intelligence - 14th European Conference, JELIA2014 , Funchal, Madeira, Portugal, September 24-26 , 2014 . Proceedings. pp. 457 - 471 ( 2014 )

12. Amendola , G. , Greco , G. , Leone , N. , Veltri , P. : Modeling and reasoning about NTU games via answer set programming . In: IJCAI 2016 . pp. 38 - 45 ( 2016 )

13. Amendola , G. , Ricca , F. , Truszczynski , M. : Generating hard random boolean formulas and disjunctive logic programs . In: IJCAI . pp. 532 - 538 . ijcai. org ( 2017 )

14. Amendola , G. , Ricca , F. , Truszczynski , M.: A generator of hard 2qbf formulas and asp programs . In: KR . AAAI Press ( 2018 )

15. Amendola , G. , Ricca , F. , Truszczynski , M. : Random models of very hard 2qbf and disjunctive programs: An overview . In: ICTCS. CEUR Workshop Proceedings , CEUR-WS.org ( 2018 )

16. Bonatti , P.A. , Calimeri , F. , Leone , N. , Ricca , F. : Answer set programming . In: 25 Years GULP. Lecture Notes in Computer Science , vol. 6125 , pp. 159 - 182 . Springer ( 2010 )

17. Brewka , G. , Eiter , T. , Truszczynski , M. : Answer set programming at a glance . Com. ACM 54 ( 12 ), 92 - 103 ( 2011 )

18. Calimeri , F. , Gebser , M. , Maratea , M. , Ricca , F. : Design and results of the Fifth Answer Set Programming Competition . Artif. Intell . 231 , 151 - 181 ( 2016 )

19. Clark , K.L. : Negation as failure . In: Logic and Data Bases . pp. 293 - 322 ( 1977 )

20. Gebser , M. , Kaminski , R. , Kaufmann, B. , Schaub , T. : Answer Set Solving in Practice . Morgan & Claypool Publishers ( 2012 )

21. Gebser , M. , Leone , N. , Maratea , M. , Perri , S. , Ricca , F. , Schaub , T. : Evaluation techniques and systems for answer set programming: a survey . In: IJCAI 2018 . pp. 5450 - 5456 ( 2018 )

22. Gebser , M. , Maratea , M. , Ricca , F. : The Design of the Sixth Answer Set Programming Competition . In: LPNMR. LNCS , vol. 9345 , pp. 531 - 544 . Springer ( 2015 )

23. Gebser , M. , Maratea , M. , Ricca , F. : What's hot in the answer set programming competition . In: AAAI . pp. 4327 - 4329 . AAAI Press ( 2016 )

24. Gebser , M. , Maratea , M. , Ricca , F. : The sixth answer set programming competition . Journal of Artificial Intelligence Research 60 , 41 - 95 ( 2017 )

25. Gelfond , M. , Lifschitz , V. : Classical negation in logic programs and disjunctive databases. New Generation Comput . 9 ( 3 /4), 365 - 386 ( 1991 ). https://doi.org/10.1007/BF03037169, http://dx.doi.org/10.1007/BF03037169

26. Grasso , G. , Iiritano , S. , Leone , N. , Lio , V. , Ricca , F. , Scalise , F. : An asp-based system for team-building in the gioia-tauro seaport . In: PADL. Lecture Notes in Computer Science , vol. 5937 , pp. 40 - 42 . Springer ( 2010 )

27. Grasso , G. , Iiritano , S. , Leone , N. , Ricca , F. : Some DLV applications for knowledge management . In: LPNMR. Lecture Notes in Computer Science , vol. 5753 , pp. 591 - 597 . Springer ( 2009 )

28. Grasso , G. , Leone , N. , Manna , M. , Ricca , F. : ASP at work: Spin-off and applications of the DLV system . In: Logic Programming , Knowledge Representation, and Nonmonotonic Reasoning . pp. 432 - 451 . LNCS 6565 ( 2011 )

29. Lierler , Y. , Maratea , M. , Ricca , F. : Systems, engineering environments, and competitions . AI Magazine 37 ( 3 ), 45 - 52 ( 2016 )

30. Manna , M. , Ricca , F. , Terracina , G.: Taming primary key violations to query large inconsistent data via ASP . TPLP 15 ( 4-5 ), 696 - 710 ( 2015 )

31. Maratea , M. , Pulina , L. , Ricca , F. : A multi-engine approach to answer-set programming . TPLP 14 ( 6 ), 841 - 868 ( 2014 )

32. Maratea , M. , Ricca , F. , Faber , W. , Leone , N.: Look-back techniques and heuristics in DLV: implementation, evaluation, and comparison to QBF solvers . J. Algorithms 63 ( 1-3 ), 70 - 89 ( 2008 )

33. Sakama , C. , Inoue , K. : Paraconsistent stable semantics for extended disjunctive programs . J. Log. Comput . 5 ( 3 ), 265 - 285 ( 1995 )