Establish Coherence in Logic Programs Modelling
Expert Knowledge via Argumentation
Andre Thevapalan1 , Jesse Heyninck1,2 and Gabriele Kern-Isberner1
1
    Technische Universität Dortmund, Germany
2
    University of Cape Town and CAIR, South Africa


                                         Abstract
                                          When modelling expert knowledge, default negation is very useful, but might lead to there being no
                                         stable models. Detecting the exact causes of the incoherence in the logic program manually can be-
                                         come quite cumbersome, especially in larger programs. Moreover, establishing coherence does require
                                         expertise regarding the modelled knowledge as well as technical knowledge about the program and its
                                         rules. This paper introduces a method to detect the causes of incoherence in logic programs by using
                                         argumentation graphs and proposes strategies to modify the responsible parts of the program in order
                                         to obtain a coherent program.

                                         Keywords
                                         Logic Programming, Coherence, Argumentation Graphs




1. Introduction
With the availability of both strong and default negation, answer set programming offers
valuable features for the usage in real-life applications. But often knowledge bases are subject
to change. Adding rules to a logic program is not as straightforward as it might seem. Due
to its declarative nature, adding new information can easily lead to contradictory knowledge.
Such contradictions can result from rules whose conclusions are contradictory while both
their premises can potentially hold simultaneously. Several approaches deal with this notion
of contradictions when updating logic programs [1, 2, 3, 4, 5, 6]. However, by using default
negation, another form of inconsistency can appear which is called incoherence. Incoherent
answer set programs do not possess answer sets even though the cause of the incoherence
generally comprises only one or more smaller parts of the program. Several approaches show
how these causes can be found and which part of the programs are affected and thus have
to be revised in order to restore the coherence of a program [7, 8, 9]. But to the best of our
knowledge, there does not exist a method describing how to establish coherence, particularly in
collaboration with an expert on the modelled knowledge. To disburden users from dealing with
actual logic program rules and from coming up with a solution themselves, we therefore propose

CAUSAL’21: Workshop on Causal Reasoning and Explanation in Logic Programming, September 20–27, 2021
   andre.thevapalan@tu-dortmund.de (A. Thevapalan); jesse.heyninck@tu-dortmund.de (J. Heyninck);
gabriele.kern-isberner@cs.tu-dortmund.de (G. Kern-Isberner)
 0000-0001-5679-6931 (A. Thevapalan); 0000-0002-3825-4052 (J. Heyninck); 0000-0001-8689-5391
(G. Kern-Isberner)
                                       Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)
a method to compute possible solutions that reuses the coherent program parts while modifying
the incoherence-causing parts as minimally invasive as possible. For that, we adapt results on
coherence in argumentation graphs [9] for normal logic programs which in turn enables us to
locate those parts of the program (called SCUPs) that are responsible for the incoherence. We
will then present different methods how the logic program can be amended in order to obtain a
coherent logic program without performing unncessary modifications.
   The paper is organized as follows. After providing some necessary preliminaries in Section
2 and 3, in Section 4, we introduce amendments for argumentation graphs and for normal
logic programs and establish results in parallel between both types of amendments. The
paper concludes by outlining how the presented approach can serve as part of a framework to
interactively establish coherence in logic programs in Section 5, followed by a brief discussion
of possible areas of application in Section 7.


2. Preliminaries
2.1. Normal Logic Programs
In this paper, we look at non-disjunctive normal logic programs (NLPs)1 [10] under the (three-
valued) stable semantics [11]. A NLP is a finite set of rules over a set 𝒜 of propositional atoms.
A default-negated atom 𝐴, also called default literal, is written as ∼𝐴. A rule 𝑟 is of the form
𝐴0 ← 𝐴1 , . . . , 𝐴𝑚 , ∼𝐴𝑚+1 , . . . , ∼𝐴𝑛 ., with atoms 𝐴0 , . . . , 𝐴𝑛 and 0 ≤ 𝑚 ≤ 𝑛. The atom 𝐴0
is the head of 𝑟, denoted by 𝐻(𝑟), and {𝐴1 , . . . 𝐴𝑚 , ∼𝐴𝑚+1 , . . . ∼𝐴𝑛 } is the body of 𝑟, denoted
by 𝐵(𝑟). Furthermore, {𝐴1 , . . . , 𝐴𝑚 } is denoted by 𝐵 + (𝑟) and {𝐴𝑚+1 , . . . , 𝐴𝑛 } by 𝐵 − (𝑟). A
rule 𝑟 with 𝐵(𝑟) = ∅ is called a fact, and if 𝐻(𝑟) = ∅, rule 𝑟 is called a constraint. A rule 𝑟 with
𝐵 − (𝑟) ̸= ∅ will be called a default rule. A normal logic program 𝒫 can then be defined as a set
of rules. A set 𝐼 of atoms satisfies a rule 𝑟 if 𝐻(𝑟) ∈ 𝐼 whenever 𝐵 + (𝑟) ⊆ 𝐼 and 𝐵 − (𝑟) ∩ 𝐼 = ∅.
We say for a set of atoms 𝐼, rule 𝑟 holds if 𝐼 satisfies 𝑟.
   A three-valued interpretation is a pair of sets of atoms ⟨𝐼, 𝐼 ′ ⟩ with 𝐼 ∩ 𝐼 ′ = ∅, where 𝐼
represents the atoms which are true and 𝐼 ′ represents the atoms which are false. Thus, any
atom 𝐴 ̸∈ 𝐼 ∪ 𝐼 ′ is undecided. We will also say, for any atom 𝐴, ⟨𝐼, 𝐼 ′ ⟩(𝐴) = T iff 𝐴 ∈ 𝐼,
⟨𝐼, 𝐼 ′ ⟩(𝐴) = F iff 𝐴 ∈ 𝐼 ′ , and ⟨𝐼, 𝐼 ′ ⟩(𝐴) = U otherwise. The truth-order ⪯𝑡 over {T, F, U} is
defined as F ≺𝑡 U ≺𝑡 T whereas the knowledge order is defined by U ≺𝑘 T, F. A three-valued
interpretation 𝐽 satisfies a positive rule 𝑟 iff min⪯𝑡 {𝐽(𝐴) | 𝐴 ∈ 𝐵(𝑟)} ⪰𝑡 𝐽(𝐻(𝑟)). We
furthermore define a constant U s.t. for every interpretation 𝐽, 𝐽(U) = U. The three-valued
              ′
reduct 𝒫 ⟨𝐼,𝐼 ⟩ of a program is obtained as follows:
                                         ′
                                   𝒫 ⟨𝐼,𝐼 ⟩ = {𝐻(𝑟) ← 𝐵 + (𝑟). | 𝑟 ∈ 𝒫, 𝐵 − (𝑟) ⊆ 𝐼 ′ }∪                      (1)
                               +                        −                     −         ′
                {𝐻(𝑟) ← 𝐵 (𝑟), U. | 𝑟 ∈ 𝒫, 𝐵 (𝑟) ∩ 𝐼 = ∅ and 𝐵 (𝑟) ∖ 𝐼 ̸= ∅}.                                 (2)
                                                    ′
Intuitively, we add 𝐻(𝑟) ← 𝐵 + (𝑟) to 𝒫 ⟨𝐼,𝐼 ⟩ when all negative atoms in 𝑟 are false, whereas
we add 𝐻(𝑟) ← 𝐵 + (𝑟), U when all negative atoms in 𝑟 are not true, and there is some negative
atoms in 𝑟 that is not false. We say 𝐽 is a stable interpretation for 𝒫 iff 𝐽 is the ⪯𝑡 -minimal
    1
    Albeit the presented approach aims to be used with answer set programs, for the proof of concept in this paper
normal logic programs will suffice.
interpretation of 𝒫 𝐽 . 𝐽 is a regular interpretation [12] if it is stable and for every stable
interpretation 𝐽 ′ , 𝐽 ′ ⪯𝑘 𝐽. A set of atoms 𝐼 is an answer set of 𝒫 if ⟨𝐼, 𝒜 ∖ 𝐼⟩ is a stable
interpretation [10].
Definition 1 (Coherence). Let 𝒫 be an NLP. 𝒫 is coherent if 𝒫 has at least one answer set.
Otherwise, 𝒫 will be called incoherent.
Example 1. The following NLP 𝒫1 will be used as a running example throughout the paper:

   𝑟1 : fever ← highTemp, ∼sunstroke.
   𝑟2 : fatigue ← lowEnergy, ∼stress, ∼workedOut.
   𝑟3 : highTemp ← tempAbove37 . 𝑟4 : sunstroke ← highTemp, ∼fever .
   𝑟5 : allergy ← pollenSeason, fatigue, ∼flu, ∼cold .
   𝑟6 : cold ← fatigue, soreThroat, ∼migraine.
   𝑟7 : flu ← fatigue, ∼migraine. 𝑟8 : migraine ← headache, ∼allergy.
   𝑟9 : soreThroat. 𝑟10 : headache. 𝑟11 : pollenSeason. 𝑟12 : lowEnergy. 𝑟13 : tempAbove37 .

 𝒫1 has no answer sets and is, therefore, incoherent. It has, however, the three-valued stable inter-
pretations 𝐽1 , 𝐽2 and 𝐽3 , where:

           ℱ ={soreThroat, headache, pollenSeason, lowEnergy, tempAbove37 }
           𝐽1 =⟨ℱ ∪ {fatigue}, {stress, workedOut}⟩
           𝐽2 =⟨ℱ ∪ {sunstroke, fatigue}, {fever , stress, workedOut}⟩
           𝐽3 =⟨ℱ ∪ {fever , fatigue}, {sunstroke, stress, workedOut}⟩

   By way of illustration, we explain why 𝐽1 is a three-valued stable interpretation. This can be
seen by first calculating 𝒫1𝐽1 :

                𝑟1′ : fever ← highTemp, U. 𝑟2′ : fatigue ← lowEnergy.
                𝑟3′ : highTemp ← tempAbove37 . 𝑟4′ : sunstroke ← highTemp, U.
                𝑟5′ : allergy ← pollenSeason, fatigue, U.
                𝑟6′ : cold ← fatigue, soreThroat, U. 𝑟7′ : flu ← fatigue, U.
                𝑟8′ : migraine ← headache, U. 𝑟9 , 𝑟10 , 𝑟11 , 𝑟12 , 𝑟13

It can be easily checked that 𝐽1 is the ⪯𝑡 minimal interpretation of 𝒫1𝐽1 .


3. Argumentation Graphs
In this section, we introduce assumption-based argumentation [13] which will allow us to
straightforwardly reason about incoherence and its causes in logic programs. The basic idea is
the following: given a logic 𝒫, an argumentation graph, which is a directed graph consisting of
arguments and attacks between these arguments, is constructed by considering sets of default
literals as arguments. An attack between two arguments takes place if we can derive a (positive)
                             ∼cold , ∼flu,                ∼fever                ∼sunstroke
              ∼allergy        ∼stress,
                             ∼workedOut
                                             ∼cold

                                                                    ∼stress,
                                              ∼flu
                                                                   ∼workedOut
                              ∼migraine,
             ∼migraine       ∼workedOut,
                               ∼stress                              ∼fatigue


Figure 1: Argumentation Graph AF(𝒫1 ) from Example 1


atom that occurs negated in the attacked set from the attacking set of default literals. Thus, an
attack between two sets of default literals occurs if there is one or more sets of rules that allow
to derive, from the attacking set of default literals, a positive atom in the attacked set. In other
words, the intuition is that every literal is assumed to be false, until and unless we can derive a
valid counter-argument against this assumption.
                                                                           ⋃︀
Definition 2. Given a logic program 𝒫, we define Ω𝒫 = {∼𝐴 | 𝐴 ∈ 𝑟∈𝒫 𝐵 − (𝑟)}. For some
Δ ⊆ Ω𝒫 , ⊢𝒫 ⊆ ℘(Ω𝒫 ) × (𝒜𝒫 ∪ Ω𝒫 ) is defined inductively as follows:

    • Δ ⊢𝒫 ∼𝐴 iff ∼𝐴 ∈ Δ,
    • Δ ⊢𝒫 𝐴 iff there is some 𝑟 ∈ 𝒫 s.t. 𝐴 = 𝐻(𝑟) and Δ ⊢𝒫 𝜑 for every 𝜑 ∈ 𝐵(𝑟).

Given Θ ∈ ℘(Ω𝒫 ), we say Θ is derivable from Δ by a set of rules Γ ∈ 𝒫 iff Δ ⊢Γ Θ.

Example 2 (Example 1 continued). We see that for 𝒫1 in Example 1, the following derivations
(among others) hold:

    • {∼fever } ⊢𝒫1 ∼fever (in view of the first item of Definition 2).
    • ∅ ⊢𝒫1 tempAbove37 . and ∅ ⊢𝒫1 highTemp. (in view of the second item of Definition 2
      and since tempAbove37 ., highTemp ← tempAbove37 . ∈ 𝒫1 ).
    • {∼fever } ⊢𝒫1 sunstroke (in view of the second item of Definition 2, the previous two items
      and sunstroke ← highTemp, ∼fever . ∈ 𝒫1 ).

Definition 3. Given a logic program 𝒫, AF(𝒫) = ⟨℘(Ω𝒫 ), ↝𝒫 ⟩ is the corresponding argumen-
tation graph of 𝒫 where ↝𝒫 ⊆ ℘(Ω𝒫 )×℘(Ω𝒫 ) s.t. for any Δ, Θ ⊆ Ω𝒫 , Δ ↝𝒫 Θ iff Δ ⊢𝒫 𝐴 for
some ∼𝐴 ∈ Θ. We will also call ∼𝐴 ∈ Ω𝒫 an assumption, and sets of assumptions arguments.

Example 3 (Example 1 continued). The graphical representation of a fragment of the argumen-
tation graph AF(𝒫1 ) can be seen in Figure 1. By way of example, we explain the attack from
{∼fever } to {∼sunstroke} by pointing to the fact that {∼fever } ⊢𝒫1 sunstroke (see Example
2). Notice that we have included only the relevant fragment of the argumentation graph. To avoid
clutter, attacks like {∼fever } ↝𝒫1 {∼sunstroke, ∼stress} were left out of Figure 1.
   Assumption labellings are used to give semantics to argumentation graphs. An assumption
labelling 𝐿 : Ω𝒫 → {T, F, U} assigns to every assumption a truth-value T (true), F (false), or
U (undecided). We denote, for † ∈ {T, F, U}, †(𝐿) = {∼𝐴 ∈ Ω𝒫 | 𝐿(∼𝐴) = †}. For a set
Δ ⊆ Ω𝒫 and an assumption labelling 𝐿, 𝐿(Δ) = min⪯𝑡 {𝐿(∼𝐴) | ∼𝐴 ∈ Δ}.
Definition 4 ([14]). Let an argumentation graph AF(𝒫) = ⟨℘(Ω𝒫 ), ↝𝒫 ⟩ and an assumption
labelling 𝐿 : Ω → {T, F, U} be given. Then 𝐿 is:
    • admissible iff for every ∼𝐴 ∈ Ω𝒫 , it holds that (1) if 𝐿(∼𝐴) = T then for every Δ ⊆ Ω𝒫
      s.t. Δ ↝𝒫 ∼𝐴, there is some ∼𝐵 ∈ Δ s.t. 𝐿(∼𝐵) = F, (2) if 𝐿(∼𝐴) = F then there is
      some Δ ⊆ Ω𝒫 s.t. Δ ↝𝒫 ∼𝐴 and for every ∼𝐵 ∈ Δ, 𝐿(∼𝐵) = T, (3) if 𝐿(∼𝐴) = U
      then for every Δ ⊆ Ω𝒫 s.t. Δ ↝𝒫 ∼𝐴, there is some ∼𝐵 ∈ Δ s.t. 𝐿(∼𝐵) ̸= T.2
    • complete if it is admissible and for every ∼𝐴 ∈ Ω𝒫 , it holds that if 𝐿(∼𝐴) = U then there
      is some Δ ⊆ Ω𝒫 s.t. Δ ↝𝒫 ∼𝐴 and for every ∼𝐵 ∈ Δ, 𝐿(∼𝐵) ̸= F.
    • preferred if it is admissible and T(𝐿) is ⊆-maximal among all admissible labellings.
    • stable if it is admissible and iff U(𝐿) = ∅.
Example 4 (Example 3 continued). For AF(𝒫1 ), there are three complete labellings, 𝐿1 , 𝐿2 and
𝐿3 , characterised by (to avoid clutter we leave out set-brackets):

            𝐿1 (∼fever ) = U              𝐿2 (∼fever ) = T               𝐿3 (∼fever ) = F
            𝐿1 (∼sunstroke) = U           𝐿2 (∼sunstroke) = F            𝐿3 (∼sunstroke) = T
            𝐿1 (∼stress) = T              𝐿2 (∼stress) = T               𝐿3 (∼stress) = T
            𝐿1 (∼workedOut) = T           𝐿2 (∼workedOut) = T            𝐿3 (∼workedOut) = T
            𝐿1 (∼fatigue) = F             𝐿2 (∼fatigue) = F              𝐿3 (∼fatigue) = F
            𝐿1 (∼allergy) = U             𝐿2 (∼allergy) = U              𝐿3 (∼allergy) = U
            𝐿1 (∼flu) = U                 𝐿2 (∼flu) = U                  𝐿3 (∼flu) = U
            𝐿1 (∼cold ) = U               𝐿2 (∼cold ) = U                𝐿3 (∼cold ) = U
            𝐿1 (∼migraine) = U            𝐿2 (∼migraine) = U             𝐿3 (∼migraine) = U

𝐿2 and 𝐿3 are also preferred. It can be noticed that there is no stable labelling for AF(𝒫1 ).
   As shown in [15], complete labellings of the argumentation graph AF(𝒫) actually give an
alternative characterisation of three-valued stable interpretation. To describe this characterisa-
tion, the following method of moving between labellings of AF(𝒫) and interpretations of 𝒫 are
useful:
Definition 5. Given an assumption labelling 𝐿, the corresponding three-valued interpretation
Lab2Int(𝐿) is defined as Lab2Int(𝐿) = ⟨𝐼, 𝐼 ′ ⟩ where 𝐼 = {𝐴 | 𝐿(∼𝐴) = F} and 𝐼 ′ =
{𝐴 | 𝐿(∼𝐴) = T}. Likewise, given a three-valued interpretation, ⟨𝐼, 𝐼 ′ ⟩, the corresponding
assumption labelling Int2Lab(⟨𝐼, 𝐼 ′ ⟩) is defined by:
                                                       ⎧
                                                                   ′
                                                       ⎨T if 𝐴 ∈ 𝐼
                                                       ⎪
                         Int2Lab(⟨𝐼, 𝐼 ′ ⟩)(∼𝐴) = F if 𝐴 ∈ 𝐼
                                                       ⎪
                                                       ⎩
                                                        U otherwise
    2
      Notice that in assumption-based argumentation labellings [14], there is a third condition (3) for admissible
labellings, which does not occur in abstract argumentation labellings.
  The authors in [15] have shown the following representation result:
Proposition 1. Let a normal logic program 𝒫 be given. Then:
    • ⟨𝐼, 𝐼 ′ ⟩ is a three-valued stable interpretation of 𝒫 iff Int2Lab(⟨𝐼, 𝐼 ′ ⟩) is a complete la-
      belling of AF(𝒫), and vice versa: 𝐿 is a complete labelling of AF(𝒫) iff Lab2Int(𝐿) is a
      three-valued stable interpretation of 𝒫.
    • ⟨𝐼, 𝐼 ′ ⟩ is a regular interpretation of 𝒫 iff Int2Lab(⟨𝐼, 𝐼 ′ ⟩) is a preferred labelling of AF(𝒫),
      and vice versa: 𝐿 is a preferred labelling of AF(𝒫) iff Lab2Int(𝐿) is a regular interpretation
      of 𝒫.
    • ⟨𝐼, 𝐼 ′ ⟩ is a stable interpretation of 𝒫 iff Int2Lab(⟨𝐼, 𝐼 ′ ⟩) is a stable labelling of AF(𝒫),
      and vice versa: 𝐿 is a stable labelling of AF(𝒫) iff Lab2Int(𝐿) is a three-valued stable
      interpretation of 𝒫.
   Notice that the above proposition also implies that every preferred interpretation corresponds
to a three-valued stable interpretation.
   The problem of incoherence in abstract argumentation has been studied in [9]. In this work,
incoherence was analysed using the notion of strongly connected component (SCC) [16]. A path
from a set of assumptions Δ to a set of assumptions Θ is a sequence of sets of assumptions
Δ1 , . . . , Δ𝑛 s.t. Δ1 = Δ, Θ = Δ𝑛 and Δ𝑖 ↝𝒫 Δ𝑖+1 for every 1 ≤ 𝑖 < 𝑛. Path-equivalence
between two sets of assumptions Δ and Θ holds iff Δ = Θ or there is a path from Δ to Θ
and from Θ to Δ. The equivalence classes of all sets of assumptions under the relation of
path-equivalence are called the strongly connected components of AF(𝒫). An SCC Δ ⊆ ℘(Ω𝒫 )
is an initial SCC if there is no SCC Θ ⊆ ℘(Ω𝒫 ) s.t. Δ ̸= Θ and there is some Θ ∈ Θ and some
Δ ∈ Δ s.t. Θ ↝𝒫 Δ. Given a set of assumptions Δ ⊆ Ω𝒫 , the restriction of AF(𝒫) to Δ is
defined as AF(𝒫)↓Δ = ⟨Δ, ↝𝒫 ∩(Δ × Δ)⟩.
Definition 6. Given a labelling 𝐿, Δ ⊆ ℘(Ω𝒫 ) is a strongly connected U-part w.r.t. 𝐿 (in short,
SCUP) iff Δ is an initial SCC of AF(𝒫)↓U(𝐿) .
  The authors in [9] show that SCUPs can be seen as the responsible parts of incoherence:
Proposition 2 (cf. [9]). There exists a SCUP w.r.t. the preferred labelling 𝐿 iff 𝐿 is not stable.
Corollary 1 (cf. [9]). 𝒫 is incoherent iff for every preferred labelling 𝐿 of AF(𝒫) there exists a
SCUP.
  They also established a strong connection between SCUPS and odd attack cycles between
arguments, which we will exploit in this paper. In more detail, a direct consequence of the
results in [9] is that every SCUP contains at least one odd-length cycle (see Appendix A.1).
SCUPS are, however, a more precise indication of the “cause” of incoherence, since, as we will
see, incoherence can be resolved by manipulating SCUPs.
Example 5 (Example 4 continued). For AF(𝒫1 ) (with 𝒫1 as in Example 1) and 𝐿2 as in Example
4, let Ω† = {Δ ∈ Ω𝒫1 | Δ ∩ {∼allergy, ∼flu, ∼cold , ∼migraine} ̸= ∅}. Then we see that
AF(𝒫1 )↓U(𝐿) = ⟨Ω† , ↝𝒫1 ∩(Ω† × Ω† )⟩.
   It can be observed that AF(𝒫1 )↓U(𝐿) contains one SCC, namely: Δ = {Δ⊆ Ω𝒫1 | Δ ⊇
{∼allergy} or Δ ⊇ {∼flu, ∼cold , ∼stress, ∼workedOut} or Δ ⊇ {∼migraine, ∼stress,
∼workedOut}}. Thus, Δ is the unique SCUP w.r.t. 𝐿2 .
4. Coherence Restoration
As pointed out before, argumentation graphs provide insight into whether a logic program is
coherent or not. More precisely, SCUPs of an argumentation graph point to the exact sets of
attacks between assumptions that are the cause for the incoherence. For this reason, we will
describe in the following how to manipulate an argumentation graph in order to obtain an
argumentation graph that is free of SCUPs and which, therefore, has a stable labelling. We will
specify suitable SCUP amendment operations, that are basic modifications that can be used (in
combination) to resolve a SCUP and thus restore coherence.

4.1. SCUP Amendment
In the remainder of this paper, we will assume as given an incoherent NLP 𝒫 over 𝒜, its
corresponding argumentation graph AF(𝒫) = ⟨℘(Ω𝒫 ), ↝𝒫 ⟩, and the set SCUPS(𝒫) of all
SCUPs in AF(𝒫) w.r.t. a preferred labelling 𝐿 for AF(𝒫).
Definition 7 (Informativeness). Let 𝐿 be a labelling for AF(𝒫) and 𝐿′ a labelling for an argu-
mentation graph AF○⋆ = ⟨℘(Ω○⋆ ), ↝○⋆ ⟩ with Ω𝒫 =Ω○⋆ . We say 𝐿′ is more informative than 𝐿,
denoted by 𝐿 ≺k 𝐿′ , if the following holds: T(𝐿) ⊆ T(𝐿′ ), F(𝐿) ⊆ F(𝐿′ ), and U(𝐿′ ) ⊊ U(𝐿).
Definition 8 (SCUP Amendment). Given a preferred labelling 𝐿 for AF(𝒫) and a SCUP Δ ∈
SCUPS(𝒫), a SCUP amendment of AF(𝒫) w.r.t. Δ is AF○⋆ = ⟨℘(Ω○⋆ ), ↝○⋆ ⟩ such that
                                       ⋃︀
   • Δ ↝○⋆ Θ iff Δ ↝𝒫 Θ, and Θ ∩ Δ = ∅ for any Δ, Θ⊆Ω𝒫 .
   • there exists a preferred labelling 𝐿○⋆ for AF○⋆ such that
        – for all ∼𝐴 ∈ Ω○⋆ ∖Ω: 𝐿○⋆ (∼𝐴) = T or 𝐿○⋆ (∼𝐴) = F, and
        – 𝐿 ≺k 𝐿○⋆ .
Any such preferred labelling 𝐿○⋆ will be called an amendment labelling of AF○⋆ w.r.t. 𝐿.
   We explain SCUP amendments as follows: these amendments are changes to the argumenta-
tion graph ⟨℘(Ω𝒫 ), ↝𝒫 ⟩ that are induced by either adding or removing attacks on arguments
within the SCUP. A minimal condition for such amendments is that the argumentation graph
can only be manipulated by adding or removing attacks on arguments that have at least one
assumption in common with the SCUP that is the basis of an amendment. Below, we will give
specific methods that lead to SCUP amendments. The amendment should have as a result
that there exists a preferred labelling which is more informative than the preferred labelling
on which the amendment was based and which “resolves” the SCUP in the sense that now
every member of the SCUP gets assigned a definitive label (i.e. a label other than U). From the
perspective of information theory, therefore, SCUP amendments reduce the undecidedness of
the knowledge represented by the argumentation graph.
   As shown in [9], it is not guaranteed that there exists a single SCUP amendment AF○⋆ of
AF(𝒫) such that a corresponding amendment labelling 𝐿○⋆ is a stable labelling.
Definition 9 (Iterated SCUP Amendment). Let AF1 be an argumentation graph with a preferred
labelling 𝐿1 and at least one SCUP Δ w.r.t. 𝐿1 . An iterated SCUP amendment is a sequence
⟨AF1 , L1 ⟩, . . . , ⟨AFn , Ln ⟩(n > 1) such that for all 𝑖 (1 ≤ 𝑖 < 𝑛), AFi+1 is a SCUP amendment of
AFi w.r.t. Δ and 𝐿𝑖+1 is an amendment labelling of AFi+1 w.r.t. 𝐿𝑖 .
   Next, we will propose different methods on how to manipulate a given argumentation graph
in order to obtain a suitable SCUP amendment.

4.2. SCUP Amendment Operations
Informally, a SCUP of an argumentation graph AF contains one or more interdependent odd
cycles such that all preferred labellings label all assumptions of these responsible cycles as
undecided. Notice the importance of the preferred labellings for restoring coherence, as they
are “as close” (according to ≤𝑖 ) to stable labellings as possible. Thus, resolving a SCUP requires
the manipulation of the graph such that there exists a preferred labelling 𝐿○⋆ for the modified
graph that is more informative, i. e., where at least one of the arguments that is part of the cycle
is labelled either true or false by 𝐿○⋆ . Suppose one of the responsible odd cycles contains the
assumption ∼𝑎. The most obvious way to obtain such a preferred labelling 𝐿○⋆ is to force an
assumption of a responsible cycle to be true or false, for example to demand that 𝑎 is true. In
argumentation graphs, such an enforcement operation can be implemented by adding an attack
from the empty set to ∼𝑎 (which, since then ∅ ⊢𝒫 𝑎, in turn corresponds to adding a fact 𝑎.
in logic programs). Other ways to obtain a more informative labelling 𝐿○⋆ and ultimately a
SCUP-free argumentation graph is to modify the responsible odd cycles and manipulate their
attacks such that they contain even subcycles or break up the responsible cycles by removing
one or more attacks of said cycles. These preliminary considerations lead us to the following
SCUP amendment operations.
   Given a SCUP Δ ∈ SCUPS(𝒫) w.r.t. a preferred labelling 𝐿, the following SCUP amendment
operations can be used to (eventually) resolve SCUP Δ:
Enforcement The SCUP amendment operation (SCUP) enforcement consists of the manipu-
lation of AF⋃︀to AF○⋆ = ⟨℘(Ω𝒫 ), ↝○⋆ ⟩ w.r.t. Δ where ↝○⋆ = ↝𝒫 ∪{∅ ↝○⋆ Δ | ∼𝐴 ∈ Δ} such
that ∼𝐴 ∈ Δ.3
Evening Up The SCUP amendment operation (SCUP) evening up consists of the manipulation
of AF to AF○⋆ ⋃︀
              = ⟨℘(Ω𝒫 ), ↝○⋆ ⟩ w.r.t. Δ where ↝○⋆ = ↝𝒫 ∪{Δ ↝○⋆ Θ | ∼𝐴 ∈ Θ} with
Δ ∈ Δ, ∼𝐴 ∈ Δ and ∼𝐴 ̸∈ Δ.
Pacification The SCUP amendment operation (SCUP) pacification consists of the manipulation
of AF to AF○⋆ = ⟨℘(Ω𝒫 ),⋃︀↝○⋆ ⟩ w.r.t. Δ such that ↝○⋆ = ↝𝒫 ∖{Δ′ ↝𝒫 Θ | ∼𝐴 ∈ Θ, Δ′ ⊆ Δ}
with Δ ∈ Δ and ∼𝐴 ∈ Δ.

Proposition 3. There exist argumentation graphs for which: (1) A single application of a SCUP
pacification operation might not always lead to a SCUP amendment; (2) no number of applications
of evening up leads to a SCUP amendment of AF w.r.t. Δ.

Proof. Ad 1: this is shown by use of the following example. Consider the following AF1 drawn
in Figure 2a. This argumentation graph has a single complete extension:

                                     𝐿(∼𝑎) = 𝐿(∼𝑏) = 𝐿(∼𝑐) = U.


    3
     A more fine-grained version of enforcement would be to allow for any attacks from arguments that are labelled
T by the preferred labelling on which the SCUP amendment is based.
                          ∼𝑐                                                     ∼𝑐




                  ∼𝑏              ∼𝑎                                     ∼𝑏             ∼𝑎

                        (a) AF1                                               (b) AF2
Figure 2: Visualization of argumentation graphs used in proof of Proposition 3


  It can be easily checked that any single application of pacification does not result in any
change to the complete labellings. For example, deleting {{∼𝑎} ↝ Δ | ∼𝑏 ∈ Δ} or {{∼𝑏} ↝
Δ | ∼𝑏 ∈ Δ} does not result in a more informative complete labelling.
  Ad 2: this is shown by use of the following example. Consider the following argumentation
graph AF1 drawn in Figure 2a. If we apply evening up as much as possible, we end up with the
argumentation graph AF2 drawn in Figure 2b, which has the same unique complete labelling as
AF1 :
                               𝐿(∼𝑎) = 𝐿(∼𝑏) = 𝐿(∼𝑐) = U.


   However, one can always iterate the amendment operations of enforcement and pacification
to obtain a SCUP amendment.
Proposition 4. For any argumentation graph AF with a preferred labelling 𝐿 and a SCUP w.r.t. 𝐿:
(1) there exists a SCUP amendment of AF w.r.t. Δ that consists of a sequence of SCUP enforcement
operations, and (2) there exists a SCUP amendment of AF w.r.t. Δ that consists of a sequence of
SCUP pacification operations.4
  For a SCUP Δ without self-attacking arguments, evening up is also an adequate amendment
operation:
Proposition 5. Let an argumentation graph AF with a preferred labelling 𝐿 and a SCUP Δ w.r.t.
𝐿 s.t. for no Δ ∈ Δ, Δ ↝ Δ. Then there exists a SCUP amendment of AF w.r.t. Δ that consists
of a sequence of SCUP evening up operations.
Proposition 6. For any finite argumentation graph AF with a preferred labelling 𝐿 and at least
one SCUP w.r.t. 𝐿, there exists an iterated SCUP amendment ⟨AF, L⟩, . . . , ⟨AFn , Ln ⟩ s.t. 𝐿𝑛 is a
stable labelling.
Corollary 2. For any incoherent NLP 𝒫 and a preferred labelling 𝐿 of AF(𝒫), there exists an
iterated SCUP amendment ⟨AF(𝒫), L⟩, . . . , ⟨AFn , Ln ⟩ s.t. any NLP 𝒫 𝑛 that induces AFn is coher-
ent.
    4
    In view of spatial limitations, proofs and further details have been left out but can be found in an online
appendix under http://tinyurl.com/thki2021-appndx.
           ∅
                   ∼cold , ∼flu,                   ∼cold , ∼flu,                    ∼cold , ∼flu,
       ∼allergy     ∼stress,            ∼allergy    ∼stress,             ∼allergy    ∼stress,
                   ∼workedOut                      ∼workedOut                       ∼workedOut

       ∼migraine                       ∼migraine                        ∼migraine

         ∼cold      ∼migraine,           ∼cold      ∼migraine,            ∼cold      ∼migraine,
                   ∼workedOut,                     ∼workedOut,                      ∼workedOut,
         ∼flu        ∼stress             ∼flu        ∼stress               ∼flu       ∼stress

 (a) AF(𝒫1 ) after SCUP enforce-   (b) AF(𝒫1 ) after SCUP evening   (c) AF(𝒫1 ) after SCUP pacifica-
     ment                              up                               tion

Figure 3: Visualization of SCUP amendment operations in Example 6


Example 6 (Example 4 continued). Consider the NLP 𝒫1 , again. AF(𝒫1 ) has the unique SCUP

                Δ = {Δ⊆ ℘(Ω𝒫1 ) | Δ ⊇ {∼allergy} or
                                    Δ ⊇ {∼flu, ∼cold , ∼stress, ∼workedOut} or
                                    Δ ⊇ {∼migraine, ∼stress, ∼workedOut}}.

   Adding the set of attacks Γ1 = {∅ ↝○⋆ Δ | ∼migraine ∈ Δ, Δ ∈ Δ} to AF(𝒫1 ) would
constitute a SCUP enforcement operation and thus AF(𝒫1○⋆ ) = ⟨℘(Ω𝒫1 ), ↝○⋆ ⟩ would be a SCUP
amendment w.r.t. Δ where ↝○⋆ = ↝ ∪Γ1 .
   Similarly, adding the set of attacks Γ2 = {{∼allergy} ↝○⋆ Δ | ∼flu ∈ Δ, Δ ∈ Δ} to AF(𝒫1 )
would constitute a SCUP evening up operation. Again, AF(𝒫1○⋆ ) = ⟨℘(Ω𝒫1 ), ↝○⋆ ⟩ would be a
SCUP amendment w.r.t. Δ where ↝○⋆ = ↝ ∪Γ2 .
   Finally, Γ3 = {{∼cold , ∼flu, ∼stress, ∼workedOut} ↝○⋆ Θ | ∼allergy ∈ Θ, Θ ∈ Δ}
being removed from AF(𝒫1 ) constitutes a SCUP pacification operation. Here, AF(𝒫1○⋆ ) =
⟨℘(Ω𝒫1 ), ↝○⋆ ⟩ would be a SCUP amendment w.r.t. Δ where ↝○⋆ = ↝ ∖Γ1 . The resulting changes
in AF(𝒫1 ) illustrated in Figure 3.
   Thus, the following methodology for resolving incoherence in an NLP 𝒫 has been introduced:
first, the argumentation framework AF(𝒫) is constructed. An iterated SCUP amendment is then
applied to this argumentation framework, which consists of a number of SCUP amendments,
each of which on its turn consists of a series of applications of SCUP amendment operations of
the user’s choice. Thus, SCUP amendment operations can be seen as the basic building blocks
in our framework for coherence restoration. In the next section, we show how these SCUP
amendment operations correspond to changes of the logic program 𝒫. With Corollary 2, such
changes to the logic program 𝒫 can then be iterated to restore coherence of 𝒫.

4.3. NLP Amendments
By definition, an NLP 𝒫 induces a unique argumentation graph AF(𝒫), whereas AF(𝒫) can
correspond to a vast number of logic programs. We have shown how one can modify an
argumentation graph AF(𝒫) of an incoherent NLP 𝒫 via iterated SCUP amendment such that
the final argumentation graph AFn has a stable labelling. This means, any NLP 𝒫 𝑛 that induces
AFn is coherent. In this section, we will show how the execution of each amendment operation
in AF(𝒫) can be implemented in 𝒫 accordingly.                                     ⋃︀
   Let 𝒫Δ denote the set of rules corresponding
                                      ⋃︀          to Δ ∈  SCUPS(𝒫),   i. e., 𝒫Δ =    {Ψ | Δ ⊢Ψ
𝐴 for some Δ ∈ Δ and some ∼𝐴 ∈ Δ}, and let 𝒫𝜏 = 𝒫∖𝒫Δ be the set of all other rules in
𝒫.
Enforcement in 𝒫 Enforcement in 𝒫 modifies 𝒫 = 𝒫Δ ∪ 𝒫𝜏 to 𝒫 ○⋆ = 𝒫Δ′ ∪ 𝒫𝜏 such that
𝒫Δ′ = 𝒫Δ ∪ {𝐿.} and there exists a rule 𝑟 ∈ 𝒫Δ with 𝐿 ∈ 𝐵 − (𝑟). In that case we also say
that 𝒫 ○⋆ is obtained by application of the program amendment operation enforcement.
Evening Up in 𝒫 Let 𝐴 be an atom such that there exists a set Θ ∈ Δ with ∼𝐴 ∈ Θ, and
let Δ ∈ Δ be a set in Δ such that ∼𝐴 ∈       / Δ. Evening up in 𝒫 modifies 𝒫 = 𝒫Δ ∪ 𝒫𝜏 to
𝒫 ○⋆ = 𝒫Δ′ ∪ 𝒫𝜏 such that 𝒫Δ′ = 𝒫Δ ∪ {𝑟} with 𝐻(𝑟) = 𝐴 and 𝐵(𝑟) = Δ. In that case we
also say that 𝒫 ○⋆ is obtained by application of the program amendment operation evening up.
Pacification in 𝒫 Let 𝑟 ∈ 𝒫Δ be a rule in 𝒫Δ such that 𝐻(𝑟) = 𝐴 and ∼𝐴 an assumption
in 𝒫Δ . Let, furthermore, Γ = {Γ ⊆ 𝒫Δ | Δ ⊢Γ 𝐴} with Δ ∈ 𝒫Δ be the set of all possible
derivations of 𝐴 from some Δ in 𝒫Δ . Pacification in 𝒫 modifies 𝒫 = 𝒫Δ ∪𝒫𝜏 to 𝒫 ○⋆ = 𝒫Δ′ ∪𝒫𝜏
by removing at least one rule of every derivation Γ ∈ Γ , i. e. 𝒫Δ′ = 𝒫Δ ∖𝐶, where 𝐶 is a
hitting set of Γ (𝐶 contains at least one rule of every set in Γ).5 In that case we also say that
𝒫 ○⋆ is obtained by application of the program amendment operation pacification.

Proposition 7. Let a program 𝒫, a preferred labelling 𝐿 w.r.t. AF(𝒫), a SCUP Δw.r.t. AF(𝒫)
and 𝐿 be given, and let 𝒫 ○⋆ be obtained by application of the program amendment operation
enforcement, evening up or pacification w.r.t. Δ. Then AF(𝒫 ○⋆ ) constitutes an application of the
respective SCUP amendment operation to AF(𝒫) w.r.t. Δ. Conversely, for every application of
the SCUP amendment operation enforcement, evening up or pacification to AF(𝒫) w.r.t. Δ, there
exists an application of the respective program amendment operation to 𝒫 resulting in a program
𝒫 ○⋆ such that AF○⋆ = AF(𝒫 ○⋆ ), where AF○⋆ is the argumentation graph resulting from applying
the mentioned SCUP amendment operation to AF(𝒫).

Definition 10. Given a program 𝒫, an iterated program amendment of 𝒫 is a sequence of
programs ⟨𝒫 1 , 𝒫 2 , . . . , 𝒫 𝑛 ⟩ s.t. 𝒫 1 = 𝒫 and for every 1 ≤ 𝑖 < 𝑛, 𝒫 𝑖+1 is obtained by application
of the program amendment operation enforcement, evening up or pacification.

Corollary 3. For any incoherent NLP 𝒫 there exists an iterated program amendment
⟨𝒫, 𝒫 1 , . . . , 𝒫 𝑛 ⟩ s.t. 𝒫 𝑛 is coherent.

Example 7 (Example 6 continued). Consider the NLP 𝒫1 , again. Let 𝒫Δ = {𝑟2 , 𝑟5 , 𝑟6 , 𝑟7 , 𝑟8 }
be the set of rules corresponding to the unique SCUP Δ in 𝒫1 (see Example 6).
  Adding the fact migraine. would then constitute a program enforcement operation in 𝒫1 . Let
ℱ= {soreThroat, headache, pollenSeason, lowEnergy, tempAbove37 }. With 𝒫1○⋆ = 𝒫1 ∪
{migraine.}, we get 𝐴𝑆(𝒫1○⋆ ) = {ℱ ∪ {highTemp, fatigue, migraine, allergy, sunstroke}}.

    5
      A more fine-grained way to alter 𝒫Δ would be to subsequently replace the removed rule 𝑟 with a modified
rule 𝑟′ where 𝐻(𝑟′ ) = 𝐻(𝑟) and 𝐵(𝑟′ ) ̸= 𝐵(𝑟). An analysis and thorough description of the properties that a
new rule 𝑟′ should possess such that the addition of 𝑟′ eventually leads to a SCUP amendment would be beyond
the scope of this paper and will thus be examined in future work.
   Similarly, adding the rule 𝑟: flu ← tempAbove37 , ∼allergy. to 𝒫1 constitutes a program
evening up operation in 𝒫1 . With 𝒫1○⋆ ′ = 𝒫1 ∪ {𝑟}, we get 𝐴𝑆(𝒫1○⋆ ′ ) = {ℱ ∪ {highTemp,
fatigue, fever , flu, migraine}, ℱ ∪ {highTemp, fatigue, sunstroke, flu, migraine}}.
   Now, let 𝒫1○⋆ ′′ = 𝒫1 ∖{𝑟5 } be the program 𝒫1 without rule 𝑟5 . This constitutes a program
pacification in 𝒫1 . We get 𝐴𝑆(𝒫1○⋆ ′′ ) = {ℱ ∪ {highTemp, fatigue, migraine, fever }, ℱ ∪ {
highTemp, fatigue, migraine, sunstroke}}.

  In contrast to the program amendment operations pacification and enforcement, evening up
was only defined in a purely declarative way. It is easy to see, that given incoherent NLP 𝒫,
there can exist a vast amount of ways to apply evening up in 𝒫 in order to obtain a coherent
program 𝒫 ○⋆ . In order to illustrate the principle behind the evening up operation, we now
propose the constructive definition of one possible evening up implementation.
Evening Up by Contraposition The contraposition of a default rule 𝑟 is a rule 𝑟′ where
𝐻(𝑟′ ) = 𝐴 such that ∼𝐴 ∈ 𝐵(𝑟), and 𝐵(𝑟′ ) = 𝐵(𝑟) ∖ {∼𝐴} ∪ {∼𝐵} such that 𝐻(𝑟) = 𝐵.
Evening up by contraposition consists of adding such a contrapositional rule 𝑟′ of a rule 𝑟 ∈ 𝒫Δ
to 𝒫Δ .

Example 8 (Example 6 continued). For 𝒫1 , the rule 𝑟8′ : allergy ←headache, ∼migraine. would
be a possible contrapositional rule for 𝑟8 and adding 𝑟8′ to 𝒫Δ would be a SCUP amendment that
would lead to a coherent program.


5. Using Amendments in Applications
Given an incoherent program 𝒫, the presented approach can lead to a vast amount of possible
solutions to obtain a coherent program 𝒫 ○⋆ . As mentioned before, deciding which solution is
the most adequate for a given application context requires expert knowledge. We, therefore,
propose that the SCUP resolution approach is implemented as part of an interactive framework
similar to the framework for conflict resolution in [17]. Such a framework can then be used to
resolve all SCUPs in 𝒫 in interaction with an expert on the knowledge that is modelled in the
given program. This expert does not necessarily have to be familiar with logic programming and
with coherence in logic programs in particular. Thus, the implementation of such a framework
has to perform two main functions: On the one hand, it has to be able to explain the exact
causes of the incoherence to the expert in a way that is understandable without the technical
knowledge surrounding the concept of coherence in logic programs. On the other hand, the
framework has to gradually assess in interaction with the expert what part of the knowledge
was initially modelled wrongly or insufficiently respectively in order to choose the most suitable
solution. The interactive aspect of the framework should consist of asking the user the right
questions such that they can make the most informed decision. For this, we propose the usage
of argumentative dialogue theory (see e.g. [18, 19, 20]). Both the causes and possible solutions
for incoherence can be explained in an interactive way using argumentative dialogue theory.
In these proof theories, the label of an argument can be explained in a dialogue held between
the computer and the human-user, where the human-user can ask questions about the status
of an argument (e.g. “why is fatigue not rejected”?) which the computer then answers by
pointing to a counter-argument (e.g. “since we can derive fatigue in view of 𝑟2 ). Formally,
these dialogue games consist of a proponent (the computer) and an opponent (the human-user)
exchanging arguments and counter-arguments based on the argumentation graph AF(𝒫). One
possible implementation would be to generate not only the possible solutions regarding the
SCUP resolution but also a corresponding dialogue tree where each path represents a possible
dialogue between the framework and the expert and eventually leads to a coherent program.


6. Related Work
The presented approach is similar to methods developed and investigated in the area of ASP
debugging. Essentially, debugging approaches in [21, 22, 23] aim to modify knowledge bases
of any (not necessarily inconsistent) logic programs such that they represent the intended
expert knowledge, i. e., they intend to remedy a mismatch between the actual semantics of
the program and the semantics intended by the modeller. Generally, the ability to identify the
errors in a given program and to compute suggestions crucially depends on information by the
expert that is given on top of the original input program. Our approach, however, focuses on a
specific class of inconsistent programs and exploits the properties of incoherence. Here, the
original program is by itself sufficient to identify the problem causes and to generate suitable
solution suggestions. Once possible solutions are available, both, the presented method as well
as debugging approaches like those based on the meta-programming [21] technique can be
used to successively obtain the most suitable solution in interaction with the user.


7. Discussion
We have shown how argumentation theory can be used to establish coherence in an NLP. The
presented approach shows different options regarding how the responsible parts of the program
can be modified in order to gradually obtain a coherent program. Such an approach is not only
useful to analyze the different properties of the possible solutions that resolve the incoherent
parts of the program. It can also serve as a motivation to consider using logic programs in
real-life applications in numerous areas where not only complex decision processes take place
but where the required knowledge is often subject to changes and updates. Embedding the
presented approach in a suitable framework as discussed in Section 5 would, therefore, provide
a useful extension for decision support systems that are based on logic programs [24], but it also
opens up the possibility to use logic program in areas where one is faced with highly contrained
problems and continously evolving knowledge like logistics or the medical sector.


References
 [1] T. Eiter, M. Fink, G. Sabbatini, H. Tompits, On properties of update sequences based on
     causal rejection, Theory Pract. Log. Program. 2 (2002) 711–767.
 [2] F. Buccafurri, W. Faber, N. Leone, Disjunctive logic programs with inheritance, in: D. D.
     Schreye (Ed.), Logic Programming: The 1999 International Conference, Las Cruces, New
     Mexico, USA, November 29 - December 4, 1999, MIT Press, 1999, pp. 79–93.
 [3] J. A. Leite, L. M. Pereira, Generalizing updates: From models to programs, in: J. Dix, L. M.
     Pereira, T. C. Przymusinski (Eds.), Logic Programming and Knowledge Representation,
     Third International Workshop, LPKR ’97, Port Jefferson, New York, USA, October 17, 1997,
     Selected Papers, volume 1471 of Lecture Notes in Computer Science, Springer, 1997, pp.
     224–246.
 [4] V. W. Marek, M. Truszczynski, Revision programming, Theor. Comput. Sci. 190 (1998)
     241–277.
 [5] C. Sakama, K. Inoue, Updating extended logic programs through abduction, in: M. Gelfond,
     N. Leone, G. Pfeifer (Eds.), Logic Programming and Nonmonotonic Reasoning, 5th Inter-
     national Conference, LPNMR’99, El Paso, Texas, USA, December 2-4, 1999, Proceedings,
     volume 1730 of Lecture Notes in Computer Science, Springer, 1999, pp. 147–161.
 [6] Y. Zhang, N. Y. Foo, Updating logic programs, in: H. Prade (Ed.), 13th European Conference
     on Artificial Intelligence, Brighton, UK, August 23-28 1998, Proceedings., John Wiley and
     Sons, 1998, pp. 403–407.
 [7] S. Costantini, B. Intrigila, A. Provetti, Coherence of updates in answer set programming,
     in: In Proc. of the IJCAI-2003 Workshop on Nonmonotonic Reasoning, Action and Change,
     2003, pp. 66–72.
 [8] S. Costantini, On the existence of stable models of non-stratified logic programs, Theory
     Pract. Log. Program. 6 (2006) 169–212.
 [9] C. Schulz, F. Toni, On the responsibility for undecisiveness in preferred and stable labellings
     in abstract argumentation, Artif. Intell. 262 (2018) 301–335.
[10] M. Gelfond, V. Lifschitz, Classical negation in logic programs and disjunctive databases,
     New Gener. Comput. 9 (1991) 365–386.
[11] T. C. Przymusinski, The well-founded semantics coincides with the three-valued stable
     semantics, Fundam. Inform. 13 (1990) 445–463.
[12] J.-H. You, L. Y. Yuan, Three-valued formalization of logic programming: is it needed?, in:
     Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of
     database systems, 1990, pp. 172–182.
[13] P. M. Dung, R. A. Kowalski, F. Toni, Assumption-based argumentation, in: Argumentation
     in artificial intelligence, Springer, 2009, pp. 199–218.
[14] C. Schulz, F. Toni, Labellings for assumption-based and abstract argumentation, Interna-
     tional Journal of Approximate Reasoning 84 (2017) 110–149.
[15] M. Caminada, C. Schulz, On the equivalence between assumption-based argumentation
     and logic programming, Journal of Artificial Intelligence Research 60 (2017) 779–825.
[16] P. Baroni, M. Giacomin, On the role of strongly connected components in argumentation,
     in: Proceedings of the 10th International Conference on Information Processing and
     Management of Uncertainty inKnowledge-Based Systems (IPMU 2004), Perugia, Italy, 2004,
     p. 1887–1894.
[17] A. Thevapalan, G. Kern-Isberner, Towards interactive conflict resolution in asp programs,
     in: M. Martinez, I. Varcinczak (Eds.), Proceedings of the 18th International Workshop on
     Non-Monotonic Reasoning, NMR 2020, 2020, pp. 29–36.
[18] S. Modgil, M. Caminada, Proof theories and algorithms for abstract argumentation frame-
     works, in: Argumentation in artificial intelligence, Springer, 2009, pp. 105–129.
[19] M. Caminada, Argumentation semantics as formal discussion, Journal of Applied Logics 4
     (2017) 2457–2492.
[20] D. Walton, E. C. Krabbe, Commitment in dialogue: Basic concepts of interpersonal reason-
     ing, SUNY press, 1995.
[21] M. Gebser, J. Pührer, T. Schaub, H. Tompits, A meta-programming technique for debugging
     answer-set programs, in: D. Fox, C. P. Gomes (Eds.), Proceedings of the Twenty-Third
     AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17,
     2008, AAAI Press, 2008, pp. 448–453.
[22] J. Oetsch, J. Pührer, H. Tompits, Stepping through an answer-set program, in: J. P.
     Delgrande, W. Faber (Eds.), Logic Programming and Nonmonotonic Reasoning - 11th
     International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings,
     volume 6645 of Lecture Notes in Computer Science, Springer, 2011, pp. 134–147.
[23] K. M. Shchekotykhin, Interactive query-based debugging of ASP programs, in: B. Bonet,
     S. Koenig (Eds.), Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelli-
     gence, January 25-30, 2015, Austin, Texas, USA, AAAI Press, 2015, pp. 1597–1603.
[24] A. Thevapalan, G. Kern-Isberner, D. Howey, C. Beierle, R. G. Meyer, M. Nietzke, Decision
     support core system for cancer therapies using ASP-HEX, in: K. Brawner, V. Rus (Eds.),
     Proceedings of the Thirty-First International Florida Artificial Intelligence Research Society
     Conference, FLAIRS 2018, Melbourne, Florida, USA. May 21-23 2018, AAAI Press, 2018, pp.
     531–536.