Strong equivalence between knowledge bases ensures the possibility of replacing one with the other without afecting reasoning outcomes, in any given context. This makes it a crucial property in nonmonotonic formalisms. In particular, the fields of logic programming and abstract argumentation provide primary examples in which this property has been subject to vast investigations. However, while (classes of) logic programs and abstract argumentation frameworks are known to be semantically equivalent in static settings, this alignment breaks in dynamic contexts due to difering notions of update. As a result, strong equivalence does not always carry over from one formalism to the other. In this paper, we carefully investigate this discrepancy and introduce a new notion of strong equivalence for logic programs. Our approach preserves strong equivalence under translation between certain classes of logic programs and both Dung-style and claim-augmented argumentation frameworks, thus restoring compatibility across these formalisms.
In the field of Knowledge Representation and Reasoning, the concept of equivalence between knowledge
bases has been the subject of extensive studies. A primary motivation behind this research is the potential
to exploit the equivalence between two knowledge bases to achieve a compact representation of the
same information. Furthermore, the possibility to substitute a specific component of a given knowledge
base with an equivalent yet simplified alternative has been shown to ease the computational cost of
reasoning over . While this advantageous behavior can be taken for granted in monotonic formalisms
(e.g. classical logic), it is usually not the case in non-monotonic ones. For this, the notion of strong
equivalence has been introduced for non-monotonic formalisms, to capture the idea of equivalence in a
dynamic environment, under any possible update [
In this paper, we consider two families of non-monotonic formalisms, namely logic programming and
abstract argumentation. Logic programming is a declarative programming paradigm where a reasoning
problem is specified by means of a so-called logic program (LP). This consists of a set of inference rules
made of atoms, possibly preceded by a negation-as-failure operator. Negative literals are assumed to be
true as long as their corresponding positive atom cannot be proven to hold. Abstract argumentation
is a sub-field of symbolic Artificial Intelligence [
Several semantics have been proposed for both of these formalisms, with the common purpose of
extracting solutions for the given program or argumentation framework. These are respectively sets of
atoms that satisfy each rule in the program (called answer-sets), and sets of arguments that are able
to defend themselves against possible counter-arguments (called extensions). For the purpose of this
work, we restrict our attention to the stable model semantics for LPs [
Previous work has shown a one-to-one mapping between Dung-style AFs and (a resticted class of)
LPs under the stable model semantics [
However, such a semantic correspondence does not necessarily carry over to dynamic contexts, where strong equivalence is required. It is possible for two logic programs that are strongly equivalent to induce argumentation frameworks that do not share this property, due to the incongruous notions of update (or expansion) in the two realms. To acknowledge such mismatch, consider the following example:
means of forensic analysis it has been established that the crime has been committed by one person alone.
= { ← not , not ., ← not , not ., ← .} where means “has an alibi" and (resp. ) means “X (resp. Y) is the murder". After some time, however, a second witness shows up and testifies that Z was drunk the entire evening on the same night, thereby falsifying the alibi of the two suspects. This information update is captured via: ′ ′ = { ← not ., ← .} where means “Z was drunk".
In accordance with equivalence results between logic programs and argumentation frameworks, the two ways of modeling our knowledge base are consistent with each other when taken individually. However, this does not happen when they are combined. Incorporating the second pair of knowledge bases ( ′ and ′) into the first one (resp. and ) yields diferent result: in the case of and ′, their union returns the expected result in the form of two possible extensions {, } and {, }. Indeed, as far as the detective knows, the witness Z was drunk and this is compatible with either X or Y being the murder. On the other hand, the union of the two logic programs and ′ yields an unexpected prediction: the alibi ‘ ← ’ is not overwritten by Z being drunk ‘ ← ’, leaving {, } as the only possible solution.
The discrepancy illustrated above reveals that updating an existing logic program by simply adding rules may produce unexpected outcomes. Facts (e.g. ‘ ← ’ in ) cannot be overwritten by incoming information, while their corresponding arguments (e.g. ∈ ) can. This behavior of logic programs is fundamentally in contrast with the way in which non-monotonicity is encoded in abstract argumentation: an argument can always be attacked by new ones.
In this work, we carefully analyze the relationship between logic programming and abstract argumentation, with a particular interest in dynamic contexts. As a first step, we recall and extend equivalence results for classes of logic programs and abstract argumentation frameworks. Subsequently, motivated by the mismatch above, we introduce a novel notion of update for a restricted class of LPs, called Rule Refinement, that resolves the issue by mimicking precisely the existing notion for Dung-style AFs. We further extend Rule Refinement to the wider class of atomic logic programs (where no positive literal occurs in the body). Within this class, Rule Refinement in LPs captures strong equivalence in claim-augmented AFs.
Logic Programming We consider normal logic programs with negation-as-failure not. Such programs consist of rules of the form ‘ : ← 1, . . . , , not 1, . . . , not .’ read as ‘ if 1 and . . . and and not 1 and . . . and not ’. Here, ∈ N is the identifier of the rule in the program; we refer to with () = . Further, , and are ordinary atoms; ℒ( ) is the set of all atoms occurring in . The atoms are called positive atoms and the atoms are called negated atoms, respectively denoted by () = {1, . . . , } and () = {1, . . . , }. We use ℎ() = and () = {1, . . . , , not 1, . . . , not } for the head and body of . With a slight abuse of notation, we extend previous predicates , , ℎ, to sets of rules, e.g. ℎ() = {ℎ() | ∈ }. Given a set of atoms , we write not = {not | ∈ }. The indices , can be equal to zero (that is, rules can have an empty body or only positive or negative literals in the body). A rule is called: constraint if ℎ() = ∅; fact if = = 0; atomic if = 0. A logic program is atomic if all the rules in are atomic.
The semantics of normal logic programs is defined in terms of answer sets, also called stable models. Whenever a program consists of positive atoms only, its (unique) stable model consists of the minimal set of atoms closed under the rules. If not, the procedure to extract answer sets from a program is performed in two steps: first a set of atoms is guessed as a candidate answer set; then, the program is modified accordingly, by propagating information relative to the candidate set. The result of this modification is a program with no negated atoms called reduct. Formally:
the negation-free program obtained from by: (i) deleting all rules ∈ with not in the body for some ∈ , (ii) deleting all negated atoms from the remaining rules. is an answer set of if is the minimal model of . The collection of answer sets of a program is ( ).
Throughout the entire paper, we will focus on the class of atomic LPs. Whenever we write program we mean an atomic one. Moreover, we will restrict our attention to a sub-classes of atomic programs. In particular, we call strict (resp. h-unique) a logic program where each atom ∈ ℒ( ) occurs at least (resp. at most) once in the head of a rule.
Abstract Argumentation We fix a infinite background set of arguments . A strict argumentation framework (strict AF1) is a directed graph = (, ) where ⊆ is a finite set of arguments and ⊆ × an attack relation between them. The union of any two strict AFs = (, ) and = (′, ′) is defined as ∪ = ( ∪ ′, ∪ ′). For two arguments , ∈ we say that attacks if (, ) ∈ . Moreover, a set of arguments ⊆ attacks if (, ) ∈ for some ∈ . Analogously, attacks if (, ) ∈ for some ∈ and for a set ′ ⊆ we say that ′ attacks if ′ attacks some ∈ . We use + = { ∈ | attacks } and − = { ∈ | attacks } to denote the set of arguments respectively attacked by and attacking . Further, the range of (with respect to ), denoted ⊕ , is the set ∪ + . For a singleton {} we use +, − and ⊕.
is conflict-free in ( ∈ cf( )) if for no , ∈ , (, ) ∈ . defends an argument if
attacks every argument attacking . Based on these two notions, [
In recent years, more expressive abstract formalisms have been proposed that extend Dung-style
AFs. Among these, claim-augmented argumentation frameworks (or CAFs) add claims to the abstract
representation [
is a triple ℱ = (, , ) such that = (, ) is a strict AF and : ↦→ is a function that assigns claims to arguments.
For a set of arguments , we use () = { () | ∈ } to denote the associated set of claims. The main advantage of CAFs lies in the fact that they allow to represent situations where diferent arguments have the same claim. In this paper we focus on a particular type of CAFs, called well-formed CAFs, for which arguments with same claim attack the same arguments. A given CAF ℱ = (, , ) is well formed if for any two arguments , , () = () implies + = +. Stable semantics for a well-formed CAF ℱ = (, ) can be defined as taking the claim-sets () inherited from every stable extension .
Definition 4. Let ℱ = (, ) be a well-formed CAF. We call a set a stable (claim-)extension of ℱ ( ∈ stb(ℱ )) if there is an ∈ stb( ) such that = ().
Strong Equivalence Strong equivalence notions for logic programs and argumentation frameworks
have been presented to capture equivalence under any possible updates. In the case of LPs, updates
consist of expanding the original program with a set of rules. Two LPs and are said to be equivalent,
denoted ≡ whenever ( ) = (). Further, and are strongly equivalent, denoted
≡ , if, for any LP , the programs ∪ and ∪ are equivalent, i.e. ∪ ≡ ∪ [
written ≡ Π , if for every program : either (1) ∪ ∈/ Π and ∪ ∈/ Π or (2) ∪ ≡ ∪ .
More recently, the notion of strong equivalence has been studied for other non-monotonic formalisms,
in the field of abstract argumentation [
Definition 6. Let = (, ) be an strict AF. The stable kernel of is = (, ) with = ∖ {(, ) | ̸= , (, ) ∈ }.
The definition of kernels is a key step in obtaining a characterization of strong equivalence.
Proposition 1 (Oikarinen and Woltran [
The idea of strong equivalence has been investigated for CAFs as well. In the literature only expansions
among compatible CAFs are considered. Informally, two CAFs are compatible if and only if the arguments
they share have the same claim. Moreover, AF kernels characterize strong equivalence for CAFs as well.
Proposition 2 (Baumann et al. [
This kernel characterization applies when ℱ and are well-formed, for any common update ℋ (possibly not well-formed). In Section 5.2 we will follow a diferent approach, since CAFs translated from logic programs are always guaranteed to be well-formed and the requirement of compatibility for expansions is not natural for logic programs.
In this section we introduce translations between increasingly larger classes of logic programs and
increasingly more expressive abstract argumentation frameworks. In particular, we recall the fact that
strict h-unique atomic programs correspond to strict AFs [
Definition 7 (Caminada et al. [
not 1, . . . , not . | ∈ and {1, . . . , } = − } Notice that by definition is atomic, strict and h-unique. Consider the following example: Example 2. Consider the following strict AF = (, ) depicted below with = {, , } and = {(, ), (, ), (, ), (, )} and its corresponding LP : not ., 3 : ←
For the other direction, the transformation only takes strict h-unique programs as input. For each rule, the head atom is associated to an argument with the same name and each negated atom (called vulnerability) in the body is associated with an attacker of the argument corresponding to the rule-head.
argumentation framework = ( , ) is defined by: • = { | ∈ ℎ(), ∈ }, • = {(, ) | ∈ ℎ(), ∈ (), ∈ }.
It is easy to see that under translation, the program in Example 2 generates exactly the strict AF . Indeed, the presented translation is a bijection.
Proposition 3 (Caminada et al. [
Moreover, the transformation preserves equivalence in both directions: the answer sets for a (strict
h-unique) program correspond exactly to the stable extensions of its transformed strict AF.
Proposition 4 (Caminada et al. [
Given a certain program , the attacks that are generated in depends on two factors: the
vulnerabilities and head-atoms. Caminada et al. [
Example 3. The two h-unique programs = { ← not .} and ′ = { ← answer set {}. However, when they are simultaneously updated with ′′ = { ← diferent: ( ∪ ′′) = {{}} and ( ′ ∪ ′′) = {{, }}. .} have the same unique .}, their answer sets are
Motivated by these considerations, we relax the notion of strictness for logic program. That is, we consider programs with negative literals that never occur as head-atoms. Indeed, the previously shown translation would relate non-strict programs to strict AFs only at the cost of losing the one-toone mapping: several non-strict LPs correspond to the same strict AF. In order to maintain an exact mapping, we also relax the definition of attack relation, allowing incoming attacks from elements in the universe outside of . We use ungrounded attacks to refer to these relations. Further, we simply call argumentation framework (AF) any framework with possibly ungrounded attacks. Definition 9 (AF). An AF = (, ) is a directed graph where ⊆ is a (non-empty) set of arguments and ⊆ × is an conflict relation. We say that ↓ = ∩ ( × ) is the set of (proper) attacks, whereas ∖ ↓ is the set of ungrounded attacks.
It is easy to see that the strictness notion of logic programs and argumentation frameworks are connected: every non-strict AF can be mapped to exactly one non-strict LP. Indeed, the isomorphism of Proposition 3 between strict h-unique atomic LPs and strict AFs can be lifted to possibly non-strict programs and AFs.
Remark 1. For any AF and corresponding logic program , = . Conversely, for any h-unique atomic LP and corresponding AF , = .
Example 4. Let = (, ) be the AF below and its corresponding LP. The ungrounded attack (, ) ∈ ∖ ↓ is represented by the vulnerability ∈ ( ).
The notions of defense, conflict-freeness as well as stable semantics for AFs are defined over the attack relation ↓ and are therefore identical to those introduced for strict AFs.
Definition 10. Let = (, ) be an AF. A set ⊆ is conflict-free in if for no , ∈ , (, ) ∈ ↓. Further, is a stable extension of if ⊕↓ = .
Notice that the notion of stable-kernel trivially characterizes strong equivalence between AFs. This follows straightforwardly from the fact that we fixed ⊆ × . Therefore, no ungrounded attack generates from a self-attacking argument. Moreover, ungrounded attacks have no influence on the evaluation of an AF.
Proposition 5. For an AF = (, ) and its strict correspondent ↓ = (, ↓), stb( ) = stb(↓).
For h-unique programs we observe a similar behavior. We can identify a set ⊆ ( ) of ungrounded vulnerabilities that make a program non-strict. Formally, the set of ungrounded vulnerabilities for is ( ) = {not | ∈ ( ) ∖ ℎ( )}. By removing such vulnerabilities, we obtain the strict program ↓ℎ, defined as ↓ℎ = {() : ℎ() ← () ∖ ( ). | ∈ }. Notice that transforming a non-strict atomic program into the corresponding strict one yields equivalent answer-sets, and vice-versa. Ungrounded vulnerabilities have no semantic impact, similarly to ungrounded attacks. Thus, answer-sets are preserved when restricting to strict programs. Proposition 6. For an atomic program and its strict correspondent ↓ℎ, ( ) = (↓ℎ).
To show that semantic equivalence can be lifted to AFs and h-unique programs, we introduce the following lemma.
Lemma 1. For any h-unique atomic logic program , ↓ℎ = ( )↓ . For any AF , ↓ = ( )↓ℎ.
Proposition 7. For any h-unique atomic program and the corresponding AF , it holds that ( ) = stb( ). Conversely, for any AF and its corresponding program , we have that stb( ) = ( ). Proof. From propositions and lemmas above, it can be easily constructed the following chain of equivalences: ( ) = (↓ℎ) = stb(↓ℎ ) = stb(( )↓ ) = stb( ). In a similar way, it is easily proven that stb( ) = stb(↓) = (↓ ) = (( )↓ℎ) = ( ). 3.2. Logic Programs and well-formed CAFs We can now move one step forward and focus on the wider class of atomic LPs and their relation to well-formed CAFs. Within this class of frameworks, attacks are not arbitrary pairs of arguments, but depends on the attacker’s claim. A translation has been introduced for strict atomic LPs from and to well-formed CAFs. In our setting, we are able to provide a slightly more general translation that considers possibly non-strict programs. To do so, we present a definition of well-formed CAFs more suitable for a dynamic setting.
Definition 11. A well-formed CAF is a triple ℱ = (, , ) where is a finite set of arguments, ⊆ × is a set of claim-attacks with the universe of claims and : ↦→ the claim function.
One can easily retrieve the original definition of CAF by fixing = {(, ) | , ∈ , () = and (, ) ∈ }. As a result, we can utilize the definition of stable semantics for well-formed CAFs by means of this translation. By appealing to the universe of claims , we have a formulation that encompasses claim attacks from claims which do not label any argument, i.e. ungrounded attacks. Any atomic LP exactly corresponds to some well-formed CAF by taking an argument for each rule, a set of claims for each atom occurring as the head of some rule and attacks defined from claims to arguments. Definition 12.
Given an atomic program , we obtain the well-formed CAF ℱ = ( , , ) via: • = { | () = , ∈ }, • = {(, ) | ∈ (), () = }, • () = ℎ() with () = .
Example 5. Consider the following atomic LP below and its corresponding well-formed CAF. Notice that the claim-attack (, 2) is realized by an ungrounded attack.
= {1 : ← not ., 2 : ← not ., 3 : ← not .}
ℱ 1 3 2 *
From a well-formed CAF, each argument corresponds to a rule r with () = and head (). Further, for each claim ∈ attacking the argument , not appears in the body of the rule. Definition 13. Let ℱ = (, , ) be a well-formed CAF with = {1, . . . , }. The corresponding LP is ℱ = { : () ← not 1, . . . not . | ∈ , {1, . . . , } = (− )}.
Indeed, the possibility of having diferent arguments with the same claim in
h-unique program. As for AFs, also CAFs are isomorphic to atomic LPs.
ℱ could make ℱ a non
Proposition 8 (König et al. [
For well-formed CAFs and LPs, equivalence is preserved under translation in a static setting.
Proposition 9 (König et al. [
In their original formulation, the propositions above consider only strict well-formed CAFs and atomic programs. However, they can be carefully adapted to our context based on the our relaxed notion of well-formed CAF. 3.3. Equivalence from Static to Dynamic Setting Until now, we have considered semantic equivalence within a static setting and provided translations that preserve it. We point out that such a semantic correspondence does not carry over to dynamic scenarios, already within the smaller class of strict AFs. Two strongly equivalent LPs may have corresponding AFs that are not strongly equivalent.
Proposition 10. For two LPs and it holds that ≡ does not imply ≡ .
= { ← not , not ., ← not , not ., ← .} = { ← not ., ← not , not ., ← .} Since both and contain the fact ← and ∈ () for every other rule in both programs, occurs in any answer-set of ∪ and ∪ for any . Hence, they are strongly equivalent. The associated strict AFs are:
Both and have no self-attacking arguments. Hence, and coincide to their own kernels.
As previously shown, equivalence among LPs and AFs does not carry over to strong equivalence: due to the incongruous definitions of update in the two realms, their evaluation changes when moving from a static to a dynamic setting. To solve this mismatch we look at LPs through the lenses of abstract argumentation. From the LP perspective, adding attackers on the corresponding AF means adding vulnerabilities to the rule whose head identifies the attacked argument. We call this operation rule refinement , defined as follows.
refine(, ′) := {() : ℎ() ← () ∪ (′).} to express that is refined by means of ′.
In the remainder of the section, we introduce a novel notion of strong equivalence for the class of (h-unique) atomic programs based on the rule refinement operator. 4.1. Rule Refinement for h-unique LPs We first consider the class of h-unique atomic programs. Within this class, talking about rules or their respective head-atoms is identical. Consequently, we can omit the explicit identifiers from rules and use the head-atoms instead. We can now introduce a novel notion of LP update, that we call Rule Refinement (RR, for brevity). Updating a program with a rule ′ via RR consists of two possible operations: in the case where ℎ(′) ∈/ ℎ( ), the update is a simple set-union; otherwise, the rule-body of ∈ for which ℎ() = ℎ(′) is merged with that of ′.
⊎-update (or simply update) of by means of a new atomic rule ′ as: ⊎ ′ = if ℎ(′) ∈/ ℎ( ) Example 7. The ⊎-update of = { ← ⊎ = { ← not ., ← not ., ←
not ., ← not .}.
not ., ← .} via the rule = ← not . is:
Towards the generalization of ⊎ between sets of rules, we notice that the consecutive applications of ⊎ preserve the result independently of the order in which they are executed.
Lemma 2. For an atomic program and two rules 1 and 2 it holds that ( ⊎ 1) ⊎ 2 = ( ⊎ 2) ⊎ 1.
Updating an h-unique program with another program = {1, . . . , } results in ⊎ = ⊎ 1 ⊎ · · · ⊎ . Moreover, ⊎ is guaranteed to be atomic and h-unique.
under Rule Refinement results in ⊎ being a h-unique and atomic.
We are now able to introduce RR strong equivalence in the class of h-unique atomic programs Ξ .
in Ξ , written ≡ Ξ , if for any program : either (1) ⊎ ∈/ Ξ and ⊎ ∈/ Ξ or (2) ( ⊎ ) = ( ⊎ ).
By the definition of RR-update, whenever ∈ Ξ , condition (1) is never satisfied. Moreover, strongly equivalent programs under standard expansions are not guaranteed to be RR strong equivalent in Ξ .
• ≡ Ξ does not imply ≡ Ξ ; • ≡ does not imply ≡ Ξ .
= { ← not , not ., ← not , not ., ← .} = { ← not , not ., ← not ., ← .}
in every answer-set of both programs. Thus, all the other rules in and do not fire, making and strongly equivalent, i.e. ≡ and ≡ Ξ . However, for the program ′ = { ← not ., ← .}, we derive: (1) ⊎ ′ ∈ Ξ and ∪ ′ ∈ Ξ as well as (2) ( ⊎ ′) ̸= ( ⊎ ′) since {, } is an answer-set of the former, but not of the latter. Thus, ̸≡ Ξ . 4.2. Rule Refinement for LPs In this section we consider a notion of strong equivalence under rule refinement for the whole class Λ of atomic LPs by dropping the requirement of h-uniqueness. We deal with (possibly non-strict) atomic programs, in which several rules with the same head might occur. Here, the information provided by rule identifiers becomes relevant when considering possible updates: identifiers allow to distinguish among updates that involve rules already contained in or new ones. Indeed, updating a program with a new rule ′ may result in the addition or refinement, irrespective of the head of ′. We then introduce a diferent notion of update.
simply update) of by means of a new rule ′ as: ⊔+ ′ =
Identifiers guide the update either towards the addition of the new rule or the refinement of an old rule with the same identifier.
Example 9. The ⊔+ -update of = {1 : ← not ., 2 : ← not ., 3 : ← .} by means of the rule = 3 : ← not . is: ⊔+ = {1 : ← not ., 2 : ← not ., 3 : ← not .}.
As before, to generalize the definition of ⊔+ -updates between sets of rules, we note that associativity is preserved.
Lemma 3. For an atomic program and two rules 1 and 2 it holds that ( ⊔+ 1) ⊔+ 2 = ( ⊔+ 2) ⊔+ 1.
Moreover, ⊔+ is atomic whenever and are.
We are now able to define strong equivalence between atomic programs under rule refinement.
class Π , written ≡ Π+ , if for any program : either (1) ⊔+ ∈/ Π and ⊔+ ∈/ Π or (2) ( ⊔+ ) = ( ⊔+ ).
In the following we will consider Π = Λ . Then, in case and are atomic, condition (1) is false if ∈ Λ , i.e., it is suficient to check condition (2) for ∈ Λ . For atomic programs, we inherit results from Proposition 12, i.e. ≡ Λ does not imply ≡ Λ+ (see Example 8). Further this notion faithfully generalizes RR strong equivalence for h-unique programs.
Proposition 14. For the class of h-unique atomic programs Ξ and , ∈ Ξ , it holds that ≡ Ξ+ implies ≡ Ξ .
In the present section, we show that the notion of strong equivalence under Rule Refinement introduced
for logic programs matches the one for abstract argumentation frameworks. We first consider h-unique
LPs and AF strong equivalence. In this setting, a syntactic characterization of RR-strong equivalence
can be reached via the notion of ASP kernel. Further, we see that our result generalizes to the full class
of atomic programs and well-formed CAFs.
5.1. AFs and h-unique Logic Programs
Inspired by the syntactic characterization of strong equivalence for strict AFs [
Example 10. In what follows, we represent a program and its kernel .
= { ← not , not ., ← not , not ., = { ← ← not , not ., ← not , not .} ← not , not ., ← ., not , not ., ← .}
As a sanity check, we show that our notions of LP and AF kernel carry over under transformation: the order in which we apply the translation and construct the kernel does not matter. Proposition 15. For a h-unique atomic program , it holds that ( ) = . Analogously for an AF , it holds that ( ) = .
Combining two programs and through Rule Refinement and transforming the resulting program into an AF yields the same framework as taking the AF union of the transformed programs. Lemma 4. For two h-unique atomic programs and , it holds that ⊎ = ∪ . Vice-versa, for two AFs and , it holds that ∪ = ⊎ .
As illustrated for AFs, we show that ASP kernels are semantically equivalent to the original instance. Proposition 16. For any h-unique atomic program it holds that ( ) = ( ).
Further, two programs and maintain the same kernel under any common update. Proposition 17. Let and be two h-unique atomic programs with = . Then for any h-unique atomic program , it holds that ( ⊎ ) = ( ⊎ ) .
Finally, we can prove that RR strong equivalence for LPs characterizes strong equivalence for AFs.
1. and have the same kernel, i.e. = . 2. The AFs corresponding to and have the same stable-kernel, i.e. ( ) = () .
4. and are strongly equivalent under RR, i.e. ≡ Ξ .
Proof. We initially show the equivalence from 1. to 4. and then the other way around. From = we derive = via Definition 8. Further, via Proposition 15 we obtain ( ) = () . This is equivalent to ≡ from the characterization of strong equivalence for AFs. From the definition of strong equivalence, we derive that for any AF , stb( ∪ ) = stb( ∪ ) and ( ∪ = (∪ ) by Proposition 4. Now, given Lemma 4, we can rewrite the previous equivalence as ( ⊎ ) = ( ⊎ ). Since the transformation between AFs and h-unique atomic programs is an isomorphism (Remark 1), it holds that ( ⊎ ) = ( ⊎ ). Therefore, for any program ′ = associated to the AF we get ( ⊎ ′) = ( ⊎ ′). Since is an AF, is guaranteed to be h-unique. Further, since and are also h-unique by hypothesis, we derive ⊎ ′ ∈ Ξ and ⊎ ′ ∈ Ξ , concluding ≡ Ξ .
We now prove the other direction. By definition, ≡ entails ( ⊎ ) = ( ⊎ ) for any hunique atomic program . Thus under translation we get ⊎ and ⊎ s.t. stb( ⊎) = stb(⊎). Then, via Lemma 4, we rewrite the previous equivalence as stb( ∪ ) = stb( ∪ ) for any program . Let us call the unique AF corresponding to each , we write stb( ∪ ) = stb( ∪ ) for any . Thus, ≡ , by definition of strong equivalence. From Proposition 1 the two frameworks have the same stable kernel: ( ) = () . We transform back to programs, obtaining ( ) = () and ( ) = ( ) via Proposition 15. Finally, Remark 1 brings us to = .
In light of Propositions 5 and 6, the result above immediately applies to the smaller class of strict AFs. Remark 2. For two strict h-unique atomic programs and , ≡ Ξ if and only if ≡ where and are strict AFs. 5.2. Atomic Programs and Well-Formed CAFs We first show that the ASP-kernel from Definition 19 is not helpful to characterize strong equivalence under Rule Refinement for atomic programs.
Example 11. Take two programs and with = .
It is easy to see that ( ) ̸= ( ). Hence, ASP-kernels do not characterize strong equivalence for atomic programs. Thus, we provide a direct characterization of RR strong equivalence for atomic programs. Later we will connect this characterization with strong equivalence for well-formed CAFs. We show that two programs are RR strongly equivalent if their rules’ identifiers, heads and bodies pairwise coincide, with the possible exception of loop-rules. In fact, two programs are strongly equivalent under RR irrespective of whether the head-atoms of corresponding loop-rules coincide.
for any ∈ ( ).
≡ Λ+ , if it holds that: 1. () = (′) implies () = (′) for all rules ∈ and ′ ∈ ; 2. () = (′) implies ℎ() = ℎ(′) for all rules ∈/ ( ) and ′ ∈/ ().
As before, we analyze how this new notion of update is understood in terms of CAFs. On the one hand, simply adding a rule to a program amounts to augmenting ℱ with an argument and possibly new attacks. On the other hand, refining a rule corresponds to adding claim-attacks to
Updating an atomic program with an atomic rule might result in a violation of compatibility in the corresponding CAFs. For instance, in Example 12 the argument 3 is labelled with two diferent claims in ℱ and ℱ. For such incompatible expansions, we operate a choice between the claim functions, prioritizing 1. This ensures that whenever two CAFs are incompatible with respect to some arguments, we choose the original claim as it is done with the rule-head of any rule that is refined via an ⊔+ -update. We can now define strong equivalence between well-formed CAFs.
Definition 21. Given any two well-formed CAFs ℱ and , we say that ℱ ≡ if and only if (ℱ ∪ ℋ) = ( ∪ ℋ) for any well-formed CAF ℋ.
This notion difers from the original in two respects: (1) it does not restricts to compatible updates only and (2) it requires updates to be well-formed. This notion of strong equivalence for CAFs corresponds to strong equivalence under rule refinement for atomic LPs. To show this, we use of the following lemma. Lemma 6. Given any two atomic programs and , it holds that ℱ ⊔+ = ℱ ∪ ℱ. Conversely, given two well-formed CAFs ℱ and ℋ, it holds that ℱ∪ℋ = ℱ ⊔+ ℋ.
• The CAFs corresponding to and are strongly equivalent for stable semantics, i.e. ℱ ≡ ℱ. • and are strongly equivalent under Rule Refinement, i.e. ≡ Λ+ .
Proof. We prove the two statements from top to bottom and viceversa. Assume ℱ ≡ ℱ. By definition, for any well-formed CAF ℋ, stb(ℱ ∪ ℋ) = stb(ℱ ∪ ℋ). From Proposition 9, we can rewrite the previous as (ℱ ∪ℋ) = (ℱ∪ℋ). Thanks to Lemma 6, we derive (ℱ ⊔+ ℋ) = (ℱ ⊔+ ℋ). We transform this via the isomorphism in Proposition 8 into ( ⊔+ ℋ) = (⊔+ ℋ). Thus, for any ′ = , we get ⊔+ ′ = ⊔+ ′. Since ℋ is a well-formed CAF, is guaranteed to be an atomic program. Further, since and are also atomic by hypothesis, we derive ⊔+ ′ ∈ Λ and ⊔+ ′ ∈ Λ . Finally, we conclude ≡ Λ+ . Assume now ≡ Λ+ . Hence, either (i) ( ⊔+ ) = ( ⊔+ ) for any program or (ii) ⊔+ ∈/ Λ and ⊔+ ∈/ Λ . If (ii) is the case, then is not atomic. If (i) is the case, then we can translate the corresponding programs, deriving stb(ℱ ⊔+ ) = stb(ℱ⊔+ ) by Proposition 9. Through Lemma 6, we then obtain stb(ℱ ∪ ℱ) = stb(ℱ ∪ ℱ) for any well-formed CAF ℱ. We fix the well-formed CAF ℋ = ℱ and rewrite the previous equivalence as stb(ℱ ∪ ℋ) = stb(ℱ ∪ ℋ), which by definition means ℱ ≡ ℱ.
From Theorems 2 & 3 we obtain a characterization of strong equivalence on well-formed CAFs. Corollary 1. For two well-formed CAFs ℱ = (ℱ , , ℱ ) and = ( , , ), we have ℱ ≡ if ℱ 1. ℱ = and ℱ = , and
2. for each ∈ , either ℱ () = () or ( ℱ (), ) ∈ ℱ ∧ ( (), ) ∈ ℱ holds.
Finally, having a characterization for strong equivalence under rule refinement, we now prove that it generalizes the standard notion of strong equivalence for atomic programs.
Proposition 18. For any two atomic programs and , ≡ Λ+ implies ≡ .
The notion of strong equivalence has been extensively investigated in both logic programming and
argumentation. For logic programs, strong equivalence has been characterized using SE -models [
Besides aforementioned works for strong equivalence in Dung-style AFs and CAFs, more fine-grained
notions of strong equivalence have been introduced, see e.g. [
In this paper, we analyzed the correspondence between certain classes of logic programs and abstract
argumentation frameworks. In the static setting, we extended existing semantic equivalence results
from strict to non-strict programs and AFs, by appealing to the concept of ungrounded attack. Further,
we adapted the definition of well-formed CAFs to align precisely with (possibly non-strict) atomic
programs. We then examined equivalence in dynamic contexts, demonstrating how the correspondence
between strongly equivalent programs and argumentation frameworks gets lost in translation. We
identified the source of such misalignment in the diverging representations of expansions. To overcome
the issue, we proposed a new notion of update for (h-unique) atomic programs, called rule refinement.
Based on this, we then defined the novel notion of strong equivalence under Rule Refinement for
(h-unique) atomic programs and investigated its relations with the standard one. We have proven that
RR strong equivalence for (strict) h-unique programs characterizes strong equivalence for (strict) AFs.
Finally, we considered the class of atomic programs. In this setting, we provided a direct characterization
for RR strong equivalence and showed that it captures strong equivalence between well-formed CAFs.
In future research, we aim at providing a characterization of RR strong equivalence for the entire class of
normal logic programs, and connect this to possibly more expressive type of argumentation frameworks.
We anticipate that this could be achieved by encoding positive dependencies among atoms via some
notion of support in the corresponding framework, as for Bipolar AFs [
This work has been supported by the European Union’s Horizon 2020 research and innovation programme (under grant agreement 101034440).
The author(s) have not employed any Generative AI tools.