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 become 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.
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 [
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.
In this paper, we look at non-disjunctive normal logic programs (NLPs)1 [
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 if ∈ , ⟨, ′⟩( ) = F if ∈ ′, 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 if 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:
⟨, ′⟩ = { ( ) ← +( ). | ∈ , −( ) ⊆ ′}∪
{ ( ) ← +( ), U. | ∈ , −( ) ∩ = ∅ and −( ) ∖ ′ ̸= ∅}.
(1)
(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 if is the ⪯ -minimal
1Albeit the presented approach aims to be used with answer set programs, for the proof of concept in this paper
normal logic programs will sufice.
interpretation of . is a regular interpretation [
Definition 1 (Coherence). Let be an NLP. is coherent if
has at least one answer set.
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 interpretations 1, 2 and 3, where: ℱ 1 =⟨ℱ ∪ { fatigue}, {stress , workedOut }⟩
={soreThroat , headache, pollenSeason, lowEnergy , tempAbove37 } 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 .
In this section, we introduce assumption-based argumentation [
∼stress, ∼workedOut ∼migraine, ∼workedOut, ∼stress ∼cold ∼flu ∼fever
∼sunstroke ∼stress, ∼workedOut ∼fatigue
Given a logic program , we define Ω = {∼ | Δ ⊆ Ω , ⊢ ⊆ ℘(Ω ) × ( ∪ Ω ) is defined inductively as follows: ∈ ︀⋃ ∈ −( )}. For some • Δ ⊢ ∼ if ∼
∈ Δ, • Δ ⊢ if there is some ∈ s.t. = ( ) and Δ ⊢ for every ∈ ( ). Given Θ ∈ ℘(Ω ), we say Θ is derivable from Δ by a set of rules Γ ∈ if Δ ⊢Γ Θ. (among others) hold: Example 2 (Example 1 continued). We see that for 1 in Example 1, the following derivations and sunstroke ← highTemp, ∼fever . ∈ 1).
and since tempAbove37 ., highTemp ← tempAbove37 . ∈ 1). • {∼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 • {∼fever } ⊢ 1 sunstroke (in view of the second item of Definition 2, the previous two items Definition 3. tation graph of some ∼
Given a logic program , AF( ) = ⟨℘(Ω ), ↝
⟩ is the corresponding argumenwhere ↝ ⊆ ℘(Ω )×℘(Ω ) s.t. for any Δ, Θ ⊆ Ω , Δ ↝ Θ if Δ ⊢ for ∈ Θ. 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}, †( ) = {∼ Δ ⊆ Ω and an assumption labelling , (Δ) = min⪯ { (∼ ) | ∼ ∈ Ω
∈ Δ}.
|
(∼ ) = †}. For a set
labelling : Ω → {T, F, U} be given. Then is:
Definition 4 ([
∼ s.t. Δ ↝
some Δ ⊆ Ω s.t. Δ ↝
then for every Δ ⊆ Ω
∼ , there is some ∼ ∈ Ω , it holds that (1) if (∼ ) = T then for every Δ ⊆ Ω ∈ Δ s.t. (∼ ) = F, (2) if (∼ ) = F then there is ∼ and for every ∼ s.t. Δ ↝ ∼ , there is some ∼ ∈ Δ, (∼ ) = T, (3) if (∼ ) = U
∈ Δ s.t. (∼ ) ̸= T.2 ∈ Ω , it holds that if (∼ ) = U then there • stable if it is admissible and if U( ) = ∅.
is some Δ ⊆ Ω s.t. Δ ↝ ∼ and for every ∼ ∈ Δ, (∼ ) ̸= F.
• preferred if it is admissible and T( ) is ⊆-maximal among all admissible labellings. 3, characterised by (to avoid clutter we leave out set-brackets): Example 4 (Example 3 continued). For AF( 1), there are three complete labellings, 1, 2 and 1(∼fever ) = U 1(∼sunstroke) = U 1(∼stress ) = T 2(∼fever ) = T 2(∼sunstroke) = F 2(∼stress ) = T 3(∼fever ) = F 3(∼sunstroke) = T 3(∼stress ) = T 1(∼workedOut ) = T 2(∼workedOut ) = T 3(∼workedOut ) = T 1(∼fatigue) = F 1(∼allergy ) = U 1(∼flu ) = U 1(∼cold ) = U 2(∼fatigue) = F 2(∼allergy ) = U 2(∼flu ) = U 2(∼cold ) = U 3(∼fatigue) = F 3(∼allergy ) = U 3(∼flu ) = U 3(∼cold ) = U 1(∼migraine) = U 2(∼migraine) = U 3(∼migraine) = U useful: 2 and 3 are also preferred. It can be noticed that there is no stable labelling for AF( 1).
As shown in [
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 Int2Lab(⟨, ′⟩)(∼ ) = ⎪ ⎨ ⎧ T
F
⎪⎩ U
if
if
∈ ′
∈
otherwise
2Notice that in assumption-based argumentation labellings [
The authors in [
three-valued stable interpretation of . • ⟨, ′⟩ is a three-valued stable interpretation of if Int2Lab(⟨, ′⟩) is a complete labelling of AF( ), and vice versa: is a complete labelling of AF( ) if Lab2Int( ) is a • ⟨, ′⟩ is a regular interpretation of if Int2Lab(⟨, ′⟩) is a preferred labelling of AF( ), and vice versa: is a preferred labelling of AF( ) if Lab2Int( ) is a regular interpretation • ⟨, ′⟩ is a stable interpretation of if Int2Lab(⟨, ′⟩) is a stable labelling of AF( ), and vice versa: is a stable labelling of AF( ) if Lab2Int( ) is a three-valued stable of .
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 [
∩(Δ × Δ)⟩. Δ1, . . . , Δ s.t. Δ1 = Δ, Θ = Δ and Δ ↝ Δ +1 for every 1 ≤ < . Path-equivalence between two sets of assumptions Δ and Θ holds if Δ = Θ 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
Definition 6.
The authors in [
Corollary 1 (cf. [
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 [
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 ∩(Ω† × Ω†)⟩. ∼workedOut }}. Thus, Δ is the unique SCUP w.r.t. 2.
It can be observed that AF( 1)↓U( ) contains one SCC, namely: Δ = {Δ⊆ Ω 1 | Δ ⊇ {∼allergy } or Δ ⊇ {∼flu , ∼cold , ∼stress , ∼workedOut } or Δ ⊇ {∼migraine, ∼stress ,
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.
SCUPs in AF( ) w.r.t. a preferred labelling for AF( ).
In the remainder of this paper, we will assume as given an incoherent NLP corresponding argumentation graph AF( ) = ⟨℘(Ω ), ↝ ⟩, and the set SCUPS( ) of all over , its 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( ). SCUPS( ), a SCUP amendment of AF( ) w.r.t. Δ is AF○⋆ = ⟨℘(Ω○⋆ ), ↝○⋆ ⟩ such that Definition 8 (SCUP Amendment). Given a preferred labelling for AF( ) and a SCUP Δ ∈ • Δ ↝○⋆ Θ if Δ ↝
︀⋃ Θ, and Θ ∩ • there exists a preferred labelling ○⋆ for AF○⋆ such that
Δ = ∅ for any Δ, Θ⊆Ω . – ≺k ○⋆ .
– for all ∼ ∈ Ω○⋆ ∖ Ω: ○⋆ (∼ ) = T or ○⋆ (∼ ) = F, and 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 [
Next, we will propose diferent methods on how to manipulate a given argumentation graph in order to obtain a suitable SCUP amendment.
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. operations can be used to (eventually) resolve SCUP Δ:
Given a SCUP Δ ∈ SCUPS( ) w.r.t. a preferred labelling , the following SCUP amendment Enforcement The SCUP amendment operation (SCUP) enforcement consists of the manipulation of AF to AF○⋆ = ⟨℘(Ω ), ↝○⋆ ⟩ w.r.t. Δ where ↝○⋆ = ↝ ∪{∅ ↝○⋆ Δ | ∼ ∈ Δ} such that ∼ ∈ ︀⋃
Δ.3 Δ ∈ Δ, ∼ Pacification ∈ ︀⋃
Δ and ∼ ̸∈ Δ.
Evening Up The SCUP amendment operation (SCUP) evening up consists of the manipulation of AF to AF○⋆ = ⟨℘(Ω ), ↝○⋆ ⟩ w.r.t. Δ where ↝○⋆ = ↝ ∪{Δ ↝○⋆ Θ | ∼ ∈ Θ} with
The SCUP amendment operation (SCUP) pacification consists of the manipulation with Δ ∈ Δ and ∼ ∈ ︀⋃
Δ. of AF to AF○⋆ = ⟨℘(Ω ), ↝○⋆ ⟩ w.r.t. Δ such that ↝○⋆ = ↝ ∖{ Δ′ ↝ Θ | ∼ ∈ Θ, Δ′ ⊆ Δ} 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.
3A 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
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 coherent.
4In 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.
∅ ∼migraine, ∼workedOut, ∼stress (a) AF( 1) after SCUP enforce- (b) AF( 1) after SCUP evening ment up (c) AF( 1) after SCUP pacification 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: ifrst, 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 .
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 that ○⋆ is obtained by application of the program amendment operation enforcement. Δ′ = Δ ∪ {. } and there exists a rule ∈ Δ with ∈ −( ). In that case we also say Enforcement in modifies = Δ ∪ to ○⋆ = Δ′ ∪ such that 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 ○⋆ = Δ′ ∪ 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 derivations of from some Δ in Δ. Pacification in modifies in Δ. Let, furthermore, Γ = {Γ ⊆ Δ | Δ ⊢Γ } with Δ ∈ Δ be the set of all possible = Δ∪ to ○⋆ = Δ′ ∪ AFn is coherent. In this section, we will show how the execution of each amendment operation in AF( ) can be implemented in
accordingly. for some Δ ∈ Δ and some ∼ ∈
Δ}, and let = ∖ ︀⋃ Let Δ denote the set of rules corresponding to Δ ∈ SCUPS( ), i. e., Δ = ⋃︀ {Ψ | Δ ⊢Ψ Δ be the set of all other rules in
there exists an iterated program amendment of the program amendment operation enforcement, evening up or pacification. be the set of rules corresponding to the unique SCUP Δ in 1 (see Example 6). Example 7 (Example 6 continued). Consider the NLP 1, again. Let Δ = { 2, 5, 6, 7, 8} ⟨ , 1, . . . , ⟩ s.t. ⋆ ℱ = {soreThroat , headache, pollenSeason, lowEnergy , tempAbove37 }. With 1○ Adding the fact migraine. would then constitute a program enforcement operation in 1. Let = 1 ∪ {migraine.}, we get
( 1○⋆ ) = {ℱ ∪ { highTemp, fatigue, migraine, allergy , sunstroke}}. .
Enforcement in
is coherent.
Definition 10. programs ⟨ 1 , the SCUP amendment operation enforcement, evening up or pacification to respective SCUP amendment operation to AF( ) w.r.t. Δ. Conversely, for every application of AF( ) w.r.t. Δ, there the mentioned SCUP amendment operation to AF( ). 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 enforcement, evening up or pacification w.r.t. and Proposition 7. Let a program , a preferred labelling w.r.t. AF( ), a SCUP Δw.r.t. AF( ) be given, and let ○⋆ be obtained by application of the program amendment operation 2, . . . ,
⟩ s.t. Given a program , an iterated program amendment of is a sequence of 1 = and for every 1 ≤ < , +1 is obtained by application by removing at least one rule of every derivation Γ ∈ Γ , i. e. Δ′ = Δ∖ , where hitting set of Γ ( contains at least one rule of every set in Γ).5 In that case we also say that is a ○⋆ is obtained by application of the program amendment operation pacification . Δ. Then AF( ○⋆ ) constitutes an application of the = Δ ∪ to 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.
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 [
The presented approach is similar to methods developed and investigated in the area of ASP
debugging. Essentially, debugging approaches in [
We have shown how argumentation theory can be used to establish coherence in an NLP. The
presented approach shows diferent 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 diferent 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 [