Assumption-based argumentation for extended disjunctive logic programming and its relation to nonmonotonic reasoning

1.1.Background

Disjunctive information is often required in reasoning and argumentation to solve problems in our daily life. In nonmonotonic reasoning, Gelfond et al. [16] proposed disjunctive default logic as a generalization of Reiter’s default logic [27] to overcome problems of default logic in handling disjunctive information. To this end, they use the symbol “|” as the connective of disjunction in a disjunctive default theory instead of the classical “∨” used in a default theory, where P∨Q means “P∨Q is known”, while P|Q means “P is known or Q is known”.11 They also showed that an extended disjunctive logic program (EDLP) [15] which may include disjunction using the connective “|” in rule head as well as two kinds of negation (i.e. classical negation “¬” and negation-as-failure “not”) can be translated into a disjunctive default theory. In contrast, in the context of formal argumentation, Beirlaen et al. [2,3] presented the extended ASPIC+ framework where disjunctive reasoning is integrated in structured argumentation with defeasible rules [25] by incorporating reasoning by cases inference scheme [2]. In their framework, an argument is allowed to have a disjunctive conclusion, while disjunction is expressed by using the classical connective “∨”. However, they did not show the relationship between their framework and other approaches in nonmonotonic reasoning such as a disjunctive default theory. Consider the following example [3] shown by them.

In regard to the relation between assumption-based argumentation and (disjunctive) default logic, Bondarenko et al. firstly showed in [5, Theorem 3.16] that there is a one-to-one correspondence between extensions of Reiter’s default theory and stable extensions of the corresponding assumption-based framework (ABF,22 for short). This denotes that the expected result k of the Kyoto protocol problem shown above is never obtained from stable extensions of their ABF corresponding to D1 based on their theorem. Besides, Bondarenko et al. [5] showed nothing about the relationship between ABA and disjunctive default logic. Hence, to solve such problems of ABFs corresponding to default theories in handling disjunctive information, it is required to find the relationship between ABFs and disjunctive default theories.

Recently, Heyninck and Arieli [18] proposed a generalized assumption-based framework induced by a disjunctive logic program (DLP), where disjunction using the connective “∨” in rule head as well as one kind of negation, i.e. negation-as-failure (NAF) are allowed to appear. Hence though their ABF induced by a DLP has a contrariness operator ¯¯ such that notp‾=p for every atom p, its language does not contain explicit negation. Then they showed a one-to-one correspondence between the stable models of a DLP [26] and the stable assumption extensions of the ABF induced by a DLP. In their work, however, there are several open problems left to be explored. First, the semantic relationship between their ABF induced by a DLP and approaches of nonmonotonic reasoning such as a disjunctive default theory is not considered in [18]. Second, they did not show how to construct an argument from disjunctive rules in a DLP nor took account of argument extensions in their ABF.

In logic programming, EDLPs [15] were proposed by Gelfond and Lifschitz to extend DLPs for knowledge representation by not only allowing classical negation (i.e. explicit negation) along with negation-as-failure but also using “|” instead of “∨”. At the same time, it is shown in [16] that an EDLP can be embedded into a disjunctive default theory (ddt, for short) which uses “|” as the connective of disjunction. In contrast, in formal argumentation, generally an assumption-based framework is capable of containing explicit negation in its language [9,10,12], but the ABFs corresponding to Reiter’s default theories have difficulties in handling disjunctive information. To our best knowledge, however, there is no study to show the relationship between ABFs and EDLPs as well as the relationship between ABFs and ddts to overcome such difficulties of ABFs discussed above.

1.2.Purpose of this paper

The purpose of this paper is first to investigate the semantic relationship between ABFs and EDLPs as well as the relationships between ABFs and other approaches in nonmonotonic reasoning (e.g. disjunctive default logic [16], prioritized circumscription [20,23]) that have not been studied, and second to show how to construct an argument in ABFs from disjunctive rules in (E)DLPs. We use the answer set semantics [15] and the paraconsistent stable model semantics [28] of EDLPs neither of which is two-valued for characterizing stable extensions of ABFs translated from EDLPs.

Regarding ABFs whose languages contain explicit negation, however, we should pay attention to avoid consistency problems which sometimes have occurred in applications of argumentation due to explicit negation contained in the language. To this end, so far, rationality postulates [6] were proposed as principles which rule-based argumentation systems should satisfy to avoid anomalous outcomes. In fact, in structured argumentation systems such as ASPIC+ and ABA frameworks whose languages contain explicit negation, conditions under which each system satisfies rationality postulates were proposed [1,12,24,25].

As for recent ABA applications containing explicit negation, Schulz and Toni [31] proposed the approach of justifying answer sets of an extended logic program (ELP) using argumentation. In their approach, they used the ABA framework ABAP instantiated with an ELP P. Though an ELP may contain classical negation, they took account of neither rationality postulates [6,12] nor consistency in ABA, and they claimed in their theorems [31, Theorem 1 and Theorem 2] that there is a one-to-one correspondence between answer sets of a consistent ELP P and the stable extensions of ABAP. In other words, their theorems claim that any ABA framework instantiated with a consistent ELP will never produce inconsistent stable extensions. However, there exist counterexamples to their theorems as shown in [33]. This means that anomalous outcomes may be obtained in applications of argumentation based on their theorems (e.g., there exists the inconsistent stable extension in ABAP instantiated with the given consistent ELP P which expresses the knowledge of the slightly modified Married John Example [33, Example 1], [6]).

Therefore, to achieve the above-mentioned purpose of this study, this paper proposes an assumption-based framework translated from an EDLP, which incorporates explicit negation as well as the connective “|” instead of “∨” in Heyninck and Arieli’s ABF induced by a DLP while avoiding consistency problems that arise in Schulz and Toni’s approach. Contributions of this study are as follows:

First, we define an argument in the ABF translated from a given EDLP which is constructed from disjunctive rules of the EDLP based on three inference rules provided in our ABF. Second, we show not only a one-to-one correspondence between p-stable models of an EDLP P and stable argument extensions (resp. stable assumption extensions) of the ABF translated from P but also a one-to-one correspondence between answer sets of an EDLP P and stable argument extensions (resp. stable assumption extensions) of the ABF translated from P with trivialization rules. Third, since our ABF incorporates explicit negation ¬, we define rationality postulates and consistency in our ABFs to avoid anomalous outcomes. Then we show answer sets of a consistent EDLP can be captured by consistent stable extensions of the translated ABF with no trivialization rules. This is useful for ABA applications containing explicit negation. Fourth, we show the new results about the relationship between ABA and disjunctive default logic [16] which enables us to overcome the difficulties of the ABF corresponding to a default logic in handling disjunctive information as well as the relationship between ABA and prioritized circumscription [20,23]. These results have not been shown so far to the best of our knowledge. Finally, we show how the possible model semantics of EDLPs [30] which is different from answer set semantics [15] is also captured by our ABFs translated from EDLPs. Appendix shows the correspondence between the semantics of ELPs [15,28] and stable assumption extensions of the associated ABA frameworks.

This paper is an extended and revised version of the paper [34], where not only Theorems 13, 14 and 15 in Section 4.1 but also Section 4.2, Section 5 and Appendix are newly introduced. Every proof sketch in [34] is replaced with a full proof while introducing new propositions, lemmas and two tables in this paper. Revisions are made throughout the paper and new considerations33 are often added. The rest of this paper is organized as follows. Section 2 shows preliminaries where new propositions proved in Appendix are mentioned. Section 3 presents an ABF translated from an EDLP, the definition of its argument, the semantic relationship between an EDLP and the corresponding ABF, the notion of consistency in ABFs, and the semantic relationship between a consistent EDLP and the corresponding consistent ABF. Section 4 shows the relationships between our proposed ABFs and nonmonotonic reasoning formalisms such as disjunctive default logic and prioritized circumscription. Section 5 shows the correspondence between the possible model semantics of EDLPs and ABA semantics of our ABFs. Section 6 discusses related work. Section 7 presents conclusions. Appendix contains new propositions relating ELPs and ABFs.

2.1.Assumption-based argumentation

An ABA framework [5,9,10] is a tuple ⟨L,R,A,¯¯⟩, where (L,R) is a deductive system, consisting of a formal language (a set of sentences) L and a set R of inference rules of the form: b0←b1,…,bm(bi∈Lfor0⩽i⩽m), A⊆L is a (non-empty) set of assumptions, and ¯¯ is a total mapping from A into L, which we call a contrariness operator. α‾ is referred to as the contrary of α∈A. For a rule r∈R of the form b0←b1,…,bm, let the head be head(r)=b0 and the body be body(r)={b1,…,bm}. We enforce that ABA frameworks are flat, namely assumptions in A do not appear in the heads of rules in R. In an ABA framework, arguments and attacks are defined as follows.

A set of arguments Args is conflict-free iff ∄A,B∈Args such that AattacksB. Args defends an argument A iff each argument that attacks A is attacked by an argument in Args. On the other hand, a set of assumptions Δ is conflict-free iff Δ does not attack itself. Δ defends α∈A iff each Δ′⊆A that attacks α is attacked by Δ.

Let AFF=(AR,attacks) be the abstract argumentation (AA) framework [8] generated from an ABA framework F, where AR is the set of all arguments such that a∈AR iff an argument a:K⊢c is in F, and (a,b)∈attacks in AFF iff a attacks b in F [11].

Let σ∈{complete,preferred,grounded,stable,ideal} be the name of the argumentation semantics. The ABA semantics is given by σ argument extensions as well as by σ assumption extensions. A σ argument extension Args⊆AR and a σ assumption extension Δ⊆A are defined respectively as follows.

Args⊆AR is:  admissible iff Args is conflict-free and defends all its elements;  a complete argument extension iff Args is admissible and contains all arguments it defends;  a preferred (resp. grounded) argument extension iff it is a (subset-)maximal (resp. (subset-)minimal) complete argument extension;  a stable argument extension iff it is conflict-free and attacks every argument in AR∖Args; an ideal argument extension iff it is a (subset-)maximal complete argument extension that is contained in each preferred argument extension.  In contrast, Δ⊆A is: admissible iff Δ is conflict-free and defends all its elements; a complete assumption extension iff Δ is admissible and contains all assumptions it defends; a preferred (resp. grounded) assumption extension iff it is a (subset-)maximal (resp. (subset-)minimal) complete assumption extension;  a stable assumption extension iff it is conflict-free and attacks every ψ∈A∖Δ; an ideal assumption extension iff it is a (subset-)maximal complete assumption extension that is contained in each preferred assumption extension.

There is a one-to-one correspondence between σ argument extensions and σ assumption extensions.

Let claim(Ag) be the conclusion (or claim) of an argument Ag. The conclusion of a set of arguments E is defined as Concs(E)={c∈L|c=claim(Ag)for an argumentAg∈E}.

Rationality postulates [6] are stated in terms of ABA in [12] as follows.

In [6], rationality postulates are defined using notions such as direct consistency, indirect consistency and closure-property. If we use the notions, it may be said that under σ argumentation semantics, AFF satisfies closure iff for each σ-extension E of AFF, Concs(E)=CNR(Concs(E)); AFF satisfies direct consistency iff for each σ-extension E, Concs(E) is not contradictory; and AFF satisfies indirect consistency iff for each σ-extension E, Concs(E) is consistent, that is, CNR(Concs(E)) is not contradictory.

Heyninck and Arieli [18] proposed (generalized) assumption-based frameworks as follows. Let L be a propositional language, p,pi∈L be atomic formulas (or atoms, for short), ψ,ϕ∈L be compound formulas and Γ,Γ′,Λ⊆L be sets of formulas. L contains conjunction “,” disjunction “∨”, implication “→”, a negation operator “∼”, and a propositional constant T for truth.

A (propositional) logic for a language L [17,18] is a pair L=(L,⊩), where ⊩ is a (Tarskian) consequence relation for L [36], which is a binary relation between sets of formulas and formulas in L satisfying the conditions such that it is reflexive (if ψ∈Γ then Γ⊩ψ), monotonic (if Γ⊩ψ and Γ⊆Γ′, then Γ′⊩ψ), and transitive (if Γ⊩ψ and Γ′∪{ψ}⊩ϕ, then Γ∪Γ′⊩ϕ). The L-based transitive closure of a set Γ of L-formulas is CnL(Γ)={ψ∈L|Γ⊩ψ} [17]. Let ℘(·) be the powerset operator.

The usual semantics in AA frameworks [8] is adapted to their ABFs as follows.

2.2.Disjunctive logic programs

A disjunctive logic program (DLP) [26] is a finite set of rules of the form44

In [18], stable models of a DLP P are defined based on A(P)⊆HBP, where A(P) is the set of atomic formulas that appear in P, and the symbol ∼ is used instead of not to denote NAF. Heyninck and Arieli [18] denoted by L=⟨LDLP,⊩⟩ the logic for the language LDLP consisting of disjunctions of atoms (p1∨⋯∨pn, for n⩾1), NAF-atoms (notp) and rules of the form (1) of a DLP, where ⊩ is constructed for LDLP by three inference rules: Modus Ponens (MP), Resolution (Res) and Reasoning by Cases (RBC). (The precise form of these inference rules will be described later in Remark 1.)

The ABF induced by a DLP P is defined by ABF(P)=⟨L,P,∼A(P),−⟩ [18], where L=⟨LDLP,⊩⟩, ∼A(P)={notp|p∈A(P)}, and −notp={p} for every p∈A(P). All the ABFs induced by DLPs are based on the same core logic L=⟨LDLP,⊩⟩. Heyninck and Arieli showed a one-to-one correspondence between stable models of a DLP P and stable assumption extensions of ABF(P) as follows.

2.3.Extended disjunctive logic programs

We consider a finite propositional extended disjunctive logic program (EDLP) [15] in this paper. An EDLP is a finite set of rules of the form:

The semantics of an EDLP is given by answer sets [15].

The following example illustrates the difference between “|” and “∨” in logic programming.

The semantics of an EDLP is also given by (four-valued) paraconsistent stable models (or p-stable models66) [28], which are regarded as answer sets defined without the condition (ii) in Definition 5, denoting that we don’t get the trivialization or deductive explosion of inconsistent (p-stable) models.

Gelfond et al. [16] proposed a disjunctive default theory (ddt, for short), which is a set of disjunctive defaults whose form is α:β1,…,βmγ1|γ2|…|γn. The semantics of a ddt is given by extensions which are generalization of Reiter’s extensions for a default theory [27]. Regarding logic programming, they showed in the following theorem that a propositional EDLP P can be translated into a disjunctive default theory emb(P) by replacing every rule in P of the form (2) with the disjunctive default

The intuition behind the disjunctive default can be “if each of Lk+1,…,Lm is believed and if each of ¬Lm+1,…,¬Ln can be consistently believed, then Li is believed for some i (1⩽i⩽k)”.

The disjunctive defaults of this form are used to compute extensions of the ddt emb(P). There exists the correspondence between answer sets of an EDLP P and extensions of emb(P) as follows.

Let F(P)=⟨LP,P,AP,¯¯⟩ be the ABA framework translated from an ELP P, where NAFP={notL|L∈LitP}, LP=LitP∪NAFP, AP=NAFP, and notL‾=L for each notL∈AP. Given M⊆LitP, let ΔM={notL|L∈LitP∖M}.77 Let Ptr=defP∪{L←p,¬p|p∈LitP,L∈LitP} be the ELP obtained from an ELP P by incorporating the trivialization rules [28]. It was shown that answer sets (resp. paraconsistent stable models) of an ELP P can be captured by stable argument extensions of the ABA framework translated from the ELP Ptr (resp. P) as follows.

For a consistent ELP, the following theorem holds.

Notice that ΔM in Theorem 2 (resp. ΔS in Theorem 3) is a stable assumption extension of the ABA framework F(P) (resp. F(Ptr)), while ΔS in Theorem 4 is a consistent stable assumption extension of the ABF F(P) due to Proposition 12, Proposition 13 and Proposition 14 as proved in Appendix respectively.

3.1.Assumption-based frameworks translated from EDLPs

We propose an assumption-based framework (ABF) translated from an EDLP, which incorporates explicit negation along with | instead of ∨ in Heyninck and Arieli’s ABF induced by a DLP to achieve our purpose shown in the introduction. An ABF translated from an EDLP is based on the logic constructed by three inference rules: Modus Ponens (MP), Resolution (Res) and Reasoning by Cases (RBC):

Σ⊩φ holds iff φ is either in Σ or is derived from Σ using the three inference rules above. According to Definition 3, Σ⊩φ iff φ∈CnL(Σ), where CnL(Σ) is the L-based transitive closure of Σ (namely, the ⊆-smallest set that contains Σ and is closed under [MP], [Res] and [RBC]). Notice that for any φ∈CnL(Σ), if φ is not of the form ℓ1|…|ℓn, then φ∈Σ.

For a special ABF =⟨L,Γ,Λ,−⟩ such that each defeasible assumption from Λ has a unique contrary (i.e. |−α|=188 for ∀α∈Λ), we may denote such an ABF by a tuple ⟨L,Γ,Λ, ¯¯⟩, where ¯¯ is a total mapping from Λ into L, and α‾∈L is the contrary of α∈Λ.

In what follows, let NAFP={notℓ|ℓ∈LitP} and LP=LitP∪NAFP for an EDLP P. We are now ready to define an ABF translated from an EDLP.

In the following, we show the ABF translated from an EDLP P is always flat.

In ABF(P), the semantics is given by assumption extensions as follows.

In ABF(P), consistency of a set of literals and NAF-literals X⊆LP is defined using a consequence operator CNP which is adapted from the CNR operator found in standard ABA.

3.2.Correspondence between answer sets of an EDLP and stable assumption extensions

Proposition 1 for a DLP [18] is generalized to Proposition 4 and Proposition 5 for an EDLP shown below. To this end, firstly as the extension of Proposition 1, we prepare the following corollary for a DLP whose stable models are defined based on HBP.

Next, Corollary 1 for a DLP is mapped to Proposition 3 for an NDP based on two lemmas about DLPs and NDPs as follows.

Though Lemma 1 holds, the difference between NDPs and DLPs appears when considering their relation to (disjunctive) default logic as shown in the following example. This implies that an NDP can be transformed to a disjunctive default theory but a DLP can never be done so.

The following lemma is also needed to obtain Proposition 3 for an NDP.

Now, we show that p-stable models (resp. answer sets) of an EDLP P are captured by stable assumption extensions of the ABF translated from P (resp. Ptr). To this end, the notation “+” [15,28] is used.

A positive form of an EDLP P [28] is the NDP P+ which is obtained by replacing each negative literal ¬L in P (where L is an atom) with a corresponding newly introduced atom L′ (called the positive form of ¬L [15]) in P+. Let M+ be an answer set of such P+. Then the following lemma holds by definition.