=Paper= {{Paper |id=Vol-2272/short7 |storemode=property |title=Compute Paracoherent Answer Sets via Saturation |pdfUrl=https://ceur-ws.org/Vol-2272/short7.pdf |volume=Vol-2272 |authors=Francesco Ricca |dblpUrl=https://dblp.org/rec/conf/aiia/Ricca18 }} ==Compute Paracoherent Answer Sets via Saturation== https://ceur-ws.org/Vol-2272/short7.pdf
    Compute Paracoherent Answer Sets via Saturation

                                      Francesco Ricca

       Department of Mathematics and Computer Science, University of Calabria, Italy
                                ricca@mat.unical.it


       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 com-
       puting 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 pro-
       grams. 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 Rea-
       soning · Semi-Equilibrium Models.


1   Introduction
Answer Set Programming (ASP) [17, 20, 16] is a well-established formalism for non-
monotonic 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 prob-
lems by encoding them as a logic program and computing its answer sets, which en-
code the problem solutions. The availability of efficient solvers made possible the de-
velopment 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 pro-
posed 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 an-
swering. But also applications in diagnosis, planning, and reasoning about actions are
conceivable [10].
2        F. Ricca

    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 se-
mantics 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 Σ . 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 Σ ); l, m, n ≥ 0, and l + m + n > 0; not repre-
sents negation-as-failure. The set H(r) = {a1 , ..., al } is the head of r, while B+ (r) =
{b1 , ..., bm } and B− (r) = {c1 , . . . , cn } 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 |H(r)| ≤ 1 and positive, if B− (r) = 0.  / A (disjunctive
logic) program P is a finite set of disjunctive rules. P isScalled normal [resp. positive]
if each r ∈ P is normal [resp. positive]. We let At(P) = r∈P At(r), that is the set of all
atoms occurring in the program P.
    Any set I ⊆ Σ is an interpretation; it is a model of a program P (denoted I |= P) if
and only if for each rule r ∈ P, I ∩ H(r) 6= 0/ if B+ (r) ⊆ I and B− (r) ∩ I = 0/ (denoted
I |= r). A model M of P is minimal, if and only if 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(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 ∈ 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 = {a ← not b; b ← c, not d; c ← a}.
                                               Compute Paracoherent ASP via Saturation         3

For instance, a model of P is {b, d}. Then, P is consistent. Moreover, the set of all
minimal models of P is given by MM(P) = {{b}, {a, c, d}}. However, P is incoherent.
Indeed, P{b} = {b ← c; c ← a}, but {b} is not a minimal model of P{b} ; and P{a,c,d} =
{a; c ← a}, but {a, c, d} is not a minimal model of P{a,c,d} .


2.2   Paracoherent ASP

Here, we introduce two paracoherent semantics that allow for keeping a system re-
sponsive 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 Σ κ = Σ ∪ {Ka | a ∈ Σ }. Intuitively, Ka can be read
as a is believed to hold. Semantically, we resort to subsets of Σ κ as interpretations I κ
and the truth values false ⊥, believed true bt, and true t. where ⊥  bt  t. The truth
value assigned by I κ to a propositional variable a is defined by
                                   
                                    t if a ∈ I ,
                                               κ
                           κ
                          I (a) = bt if Ka ∈ I κ and a 6∈ I κ ,
                                   
                                    ⊥ otherwise.

The semi-stable models of a program P are obtained from its epistemic κ-transformation
Pκ .

Definition 1 (Epistemic κ-transformation Pκ ). Let P be a program. Then its epis-
temic κ-transformation is defined as the program Pκ obtained from P by replacing
each rule r of the form (1) in P, such that B− (r) 6= 0,
                                                      / with:

                      λr,1 ∨ . . . ∨ λr,l ∨ Kc1 ∨ . . . ∨ Kcn ← b1 , . . . , bm ,            (2)
                                                            ai ← λr,i ,                      (3)
                                                               ← λr,i , c j ,                (4)
                                                          λr,i ← ai , λr,k ,                 (5)

for 1 ≤ i, k ≤ l and 1 ≤ j ≤ n, where the λr,i , λr,k are fresh atoms.

Note that for any program P, its epistemic κ-transformation Pκ is positive. For every in-
terpretation I κ over Σ 0 ⊇ Σ κ , let G (I κ ) = {Ka ∈ I κ | a 6∈ I κ } denote the atoms believed
true but not assigned true, also referred to as the gap of I κ . Given a set F of interpreta-
tions over Σ 0 , an interpretation I κ ∈ F is maximal canonical in F , if no J κ ∈ F exists
such that G (I κ ) ⊃ G (J κ ). By mc(F ) we denote the set of maximal canonical interpre-
tations in F . Semi-stable models are then defined as maximal canonical interpretations
among the answer sets of Pκ . Then we can equivalently paraphrase the definition of
semi-stable models in [33] as follows.
4       F. Ricca

Definition 2 (Semi-stable models). Let P be a program over Σ . An interpretation I κ
over Σ κ is a semi-stable model of P, if I κ = S ∩ Σ κ for some maximal canonical answer
set S of Pκ . The set of all semi-stable models of P is denoted by SST (P), i.e., SST (P) =
{S ∩ Σ κ | S ∈ mc(AS(Pκ ))}.

Example 2. Consider the program
                    P = {b ← not a; c ← not b; a ← c; d ← not d}.
Its epistemic κ-transformation is
                                                                  
                        
                         λ1 ∨ Ka; b ← λ1 ; ← a, λ1 ; λ1 ← b, λ1 ; 
                                                                   
                          λ2 ∨ Kb; c ← λ2 ; ← b, λ2 ; λ2 ← c, λ2 ;
                                                                  
                    κ
                   P =                                              ,
                        
                            a ← c;                                
                                                                   
                          λ3 ∨ Kd; d ← λ3 ; ← d, λ3 ; λ3 ← d, λ3
                                                                  

which has the answer sets M1 = {Ka, Kb, Kd}, M2 = {λ1 , b, Kb, Kd}, and M3 = {Ka,
λ2 , a, c, Kd}. Since G (M1 ) = {Ka, Kb, Kd}, G (M2 ) = {Kd}, and G (M3 ) = {Kd},
among them M2 and M3 are maximal canonicals. Hence, M2 ∩ Σ κ = {b, Kb, Kd} and
M3 ∩ Σ κ = {a, c, Ka, Kd} 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 canon-
ical answer sets, of an extension of the epistemic κ-transformation.

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

                                                     Ka ← a,                           (6)
                   Ka1 ∨ . . . ∨ Kal ∨ Kc1 ∨ . . . ∨ Kcn ← Kb1 , . . . , Kbm ,         (7)

for a ∈ Σ , respectively for every rule r ∈ P of the form (1).

Definition 4 (Semi-equilibrium models). Let P be a program over Σ , and let I κ be
an interpretation over Σ κ . Then, I κ ∈ SEQ(P) if, and only if, I κ ∈ {M ∩ Σ κ | M ∈
mc(AS(PHT ))}, 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
                                                                  
             HT            Ka ← a; Kb ← b; Kc ← c; Kd ← d;
            P =P ∪   κ                                               ,
                           Kb ∨ Ka; Kc ∨ Kb; Ka ← Kc; Kd ← Kd
which has the answer sets {Ka, Kb, Kd}, {λ1 , b, Kb, Kd}, and {Ka, λ2 , a, c, Kc, Kd}.
Therefore, the semi-equilibrium models of P are {b, Kb, Kd} and {a, c, Ka, Kc, Kd}.

    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 ob-
servations concerning the computational complexity of the computation of a paracoher-
ent answer set.
                                                Compute Paracoherent ASP via Saturation       5

      Reasoning tasks           Normal ASP programs               Disjunctive ASP programs
                               ASP      SST /SEQ                 ASP          SST /SEQ
                                                                                  p
      Checking                  P        coNP-c                 coNP-c          Π2 -c
                                            p                     p               p
      Brave inference          NP-c       Σ2 -c                  Σ2 -c          Σ3 -c
                                             p                     p              p
      Cautious inference      coNP-c      Π2 -c                  Π2 -c          Π3 -c
                                                                  p
      Existence                NP-c       NP-c                   Σ2 -c          NP-c

Table 1. Computational complexity of some reasoning tasks for answer set semantics, semi-stable
model semantics and semi-equilibrium model semantics (completeness results).




2.3   Complexity Considerations

The complexity of various reasoning tasks with paracoherent answer sets has been an-
alyzed 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 check-
ing is Π2P -complete, leading to Σ3P -completeness for brave, and Π3P -completeness for
cautious reasoning in case of disjunctive ASP programs; while paracoherent answer set
checking is coNP-complete, leading to Σ2P -completeness for brave, and Π2P -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 FΣ3P for disjunc-
tive ASP programs, and actually in FΘ3P (functional polynomial time with a logarithmic
number of calls to a Σ2P -complete oracle), because for computing one paracoherent an-
swer set it is sufficient to solve a cardinality-optimization problem. Hence, this task is in
FΣ2P for normal ASP programs, and actually in FΘ2P (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χ ∪ Pg . Then, we build an answer set program Π 0 as
follows. First, starting from Π , 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 ∈ Π of the form
(1), we build a rule, named W (r), of the form

                     w ← na1 , . . . , nal , xb1 , . . . , xbm , nc1 , . . . , ncn .         (8)

Let W (Π ) = {W (r)|r ∈ Π } be the set of all rules of the form (8). Then, given a rule
              S

r ∈ Π such that |H(r)| > 1, for each atom ai appearing in the head of r, we consider
6       F. Ricca

two fresh atoms, namely cari and ncari , and we build the following set of rules:

         cari ← na1 , . . . , nai−1 , nai+1 , . . . , nal , xb1 , . . . , xbm , nc1 , . . . , ncn ;    (9)
                ncari ← xa j ;                      ∀ j = 1, . . . , i − 1, i + 1, . . . , m;         (10)
                ncari ← nb j ;                                           ∀ j = 1, . . . , m;          (11)
                ncari ← xc j ;                                           ∀ j = 1, . . . , n.          (12)

Moreover, whenever B(r) 6= 0,
                           / we also consider the following set of rules:

                        xb j ← cari ;                            ∀ j = 1, . . . , m;                  (13)
                        nc j ← cari ;                             ∀ j = 1, . . . , n.                 (14)

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 Π such that a occurs in
the head of r and |H(r)| > 1. Then, for each atom a ∈ Π , we construct the following
rule (denoted by C(a)):

                                w ← xa, {ncar : r ∈ crules(a)}.                                       (15)

Note that, whenever crules(a) = 0,    / the rule of the form (15) will be w ← xa. Now, let
C(Π ) be the set of all rules   of the form C(r, ai ) and C(a) that canSbe constructed from
Π . That is, C(Π ) = {C(r, ai ) : ai ∈ At(Π ) and r ∈ crules(ai )} ∪ {C(a) : a ∈ At(Π )}.
                      S

Then, for each atom a ∈ At(Π ), we construct a disjunctive rule of the form xa ∨ na. (de-
noted by D(xa)), and for each atom of the form cari ∈ C(Π ), we construct a disjunctive
rule of theSform cari ∨ ncari . (denoted by D(cari )). Hence, we set D(Π ) = {D(xa)|a ∈
                                                                              S

At(Π )} ∪ {D(cari )|cari ∈ C(Π )}. Finally, we consider the following program:
                                  Π 0 = W (Π ) ∪C(Π ) ∪ D(Π ).
Note that the program Π 0 so constructed is a sort of completion of the original program
Π [19]. Therefore, the set of all answer sets of the positive program Π 0 extended by
the constraint ← w., corresponds to the set of all answer sets of the original program
Π . More formally, by setting Mx = {a ∈ At(Π ) : xa ∈ M} and ASx (Π 0 ) = {Mx : M ∈
AS(Π 0 )}, it holds that
Theorem 1. Let Π be a normal ASP program. Then, ASx (Π 0 ∪ {← w.}) = AS(Π ).
    Now, to minimize the gap atoms, we consider the following set of rules:
                                                                           
                
                 un(gap(Ka)) ← xgap(Ka), not gap(Ka); ∀a ∈ At(P);         
                 eq(gap(Ka)) ← xgap(Ka), gap(Ka);             ∀a ∈ At(P); 
                
                                                                           
                                                                            
      Πcheck = eq(gap(Ka)) ← ngap(Ka), not gap(Ka); ∀a ∈ At(P);
                              w ← un(gap(Ka));                 ∀a ∈ At(P); 
                
                                                                           
                
                                                                           
                                                                            
                              w ← {eq(gap(Ka)) : a ∈ At(P)}
                                                                           

Intuitively, the program Πcheck minimizes the gap atoms, by comparing any two answer
sets of Π . Indeed, the atom w is derived whenever the comparison shows that the set of
                                         Compute Paracoherent ASP via Saturation        7

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 M 0 of the completion Π 0 (that mimics an answer set
of the original program Π , see Theorem 1), but that atom does not belong to another
answer set M of the original program Π , then the gap of M 0 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 Π 0 is equal to the set of gap atoms of an answer set of Π .
    Finally, we consider the following set of rules (so-called saturation rules) which de-
rive each new atom created in the construction of Π 0 and Πcheck , whenever w is derived.

                                               a ← w; ∀a ∈ At(Π 0 ); 
                                                                       
                                
                                                                       
                                   un(gap(Ka)) ← w; ∀a ∈ At(P);
                                                                       
                  Πsaturation =
                                
                                  eq(gap(Ka)) ← w; ∀a ∈ At(P);        
                                                 ← not w
                                                                       

Note that, the last rule force to derive w to obtain an answer set, otherwise the pro-
gram should be incoherent. Now, by considering Πrew as the union of Π , Π 0 , Πcheck ,
and Πsaturation , there is a one-to-one correspondance between answer sets of Πrew and
paracoherent answer sets of P. More formally,

Theorem 2. Let P be a normal program. Then, M ∈ AS(Πrew ) implies M ∩ At(P) ∈
PAS(P), and M 0 ∈ PAS(P) implies M 0 ∪ (At(Πrew ) \ At(P)) ∈ AS(Πrew ).

    Intuitively, Π 0 is a “copy” of Π , and the program Πcheck compares any two answer
sets of Π (by comparing answer sets of Π and Π 0 ). Now, if M is an answer set of Πrew ,
then w ∈ M, and so each new atom occurring in Π 0 and Πcheck belongs to M. Moreover,
there is an answer set J of Π contained into M. As M is an answer set, it is a minimal
model of the reduct of Πrew , that is Π J ∪ Π 0 ∪ Πcheck
                                                      J  ∪ Πsaturation \ {← not w.}. This
means that the set of gap atoms of each other answer set of Π 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 M 0 ∪ (At(Πrew ) \ At(P)) is an
answer set of Πrew , whenever M 0 is a paracoherent answer set of P.


4   Conclusion

Paracoherent semantics have been suggested as a remedy, which extend the classical no-
tion 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 pro-
posed 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 em-
ployed for implementing an efficient paracoherent ASP solver.
8        F. Ricca

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., Peñ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, CEUR-
    WS.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 para-
    coherent 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 Con-
    ference 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 program-
    ming 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 para-
    coherent answer set programs. Artif. Intell. 234, 219–271 (2016)
11. Amendola, G., Eiter, T., Leone, N.: Modular paracoherent answer sets. In: Logics in Ar-
    tificial 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 pro-
    grams. In: KR. AAAI Press (2018)
15. Amendola, G., Ricca, F., Truszczynski, M.: Random models of very hard 2qbf and dis-
    junctive 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. Mor-
    gan & Claypool Publishers (2012)
                                            Compute Paracoherent ASP via Saturation            9

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 Com-
    petition. 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 man-
    agement. 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 inconsis-
    tent 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)