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 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.

Preliminaries

Normal Logic Programs

In this paper, we look at non-disjunctive normal logic programs (NLPs) 1 [10] under the (threevalued) 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 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]. It can be easily checked that 𝐽 1 is the ⪯ 𝑡 minimal interpretation of 𝒫 𝐽 1 1 .

Definition 1 (Coherence

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) 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 Δ ⊢ Γ Θ., Δ ↝ 𝒫 Θ 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 argumentation 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 characterisation, 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:

Int2Lab(⟨𝐼, 𝐼 ′ ⟩)(∼𝐴) = ⎧ ⎪ ⎨ ⎪ ⎩ T if 𝐴 ∈ 𝐼 ′ F if 𝐴 ∈ 𝐼 U otherwise

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 labelling 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 .

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.

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 argumentation 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 argumentation 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 AF 1 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 ⟨AF 1 , L 1 ⟩, . . . , ⟨AF n , L n ⟩(n > 1) such that for all 𝑖 (1 ≤ 𝑖 < 𝑛), AF i+1 is a SCUP amendment of AF i w.r.t. Δ and 𝐿 𝑖+1 is an amendment labelling of AF i+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.

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 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 manipulation of AF to

AF ○ ⋆ = ⟨℘(Ω 𝒫 ), ↝ ○ ⋆ ⟩ w.r.t. Δ where ↝ ○ ⋆ = ↝ 𝒫 ∪{∅ ↝ ○ ⋆ Δ | ∼𝐴 ∈ Δ} such that ∼𝐴 ∈ ⋃︀ Δ.○ ⋆ = ⟨℘(Ω 𝒫 ), ↝ ○ ⋆ ⟩ 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 AF 1 drawn in Figure 2a. This argumentation graph has a single complete extension: Ad 2: this is shown by use of the following example. Consider the following argumentation graph AF 1 drawn in Figure 2a. If we apply evening up as much as possible, we end up with the argumentation graph AF 2 drawn in Figure 2b, which has the same unique complete labelling as

𝐿(∼𝑎) = 𝐿(∼𝑏) = 𝐿(∼𝑐) = U. ∼𝑐 ∼𝑎 ∼𝑏 (a) AF 1 ∼𝑐 ∼𝑎 ∼𝑏 (b) AF 2AF 1 : 𝐿(∼𝑎) = 𝐿(∼𝑏) = 𝐿(∼𝑐) = 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. 4For a SCUP Δ without self-attacking arguments, evening up is also an adequate amendment operation: 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 𝒫.

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 AF n has a stable labelling. This means, any NLP 𝒫 𝑛 that induces AF n 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.

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.

Related Work

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 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.

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.