The first step in reasoning using an approach such as ASPIC+ requires all arguments to be generated, and doing so is computationally intensive when encountering large or frequently updated defeasible theories. In this paper, we introduce the informative partial argumentation framework that enables us to control and customise the argument construction process, potentially improving computational efficiency. In our framework, arguments are constructed in a lazy manner; and through the modularisation of our framework, it is possible to restrict the amount of computation to only the necessary information.
The ASPIC+ framework describes how arguments can be constructed from a knowledge base, and
allows for reasoning to take place over the resultant argumentation system. However, generating
all arguments is computationally expensive [
We begin this paper by describing the ASPIC+ framework and the intuition behind our approach (Sec. 2). Section 3 forms the core of our work, introducing informative partial arguments and demonstrating how these can be used to compute the justification status of a literal. In Section
of Yun et al. [
The body of r is the rule’s set of antecedents {φ1, ...φn}, and is denoted body(r); head(r) = Φ is called r’s head, while name(r) returns the name of r, which is assumed to be in L . Axioms (resp. ordinary premises) are strict (resp. defeasible) rules with empty bodies. The implication of r is ⇝ ∈ {⇒, →} and is denoted imp(r). A defeasible theory T is a pair (S , D ) where S ⊆ R is a set of strict rules and D ⊆ R is a set of defeasible rules. Based on the knowledge contained in a given set of rules, we can identify support relations between pairs of propositions as follows. Definition 1 (Support Between Propositions). Given R ⊆ R and a logical language L , a proposition p ∈ L is supported by p′ ∈ L , denoted as p′ →↦−R p, if (1) there exists a rule r ∈ R such that head(r) = p and p′ ∈ body(r) or (2) there is a sequence of propositions (p0, p1, . . . , pn) R such that for all 0 ≤ i ≤ n, pi ∈ L , p0 = p′, pn = p such that for all 0 ≤ i ≤ n − 1, pi →↦− pi+1.
p ∈ L such that p →↦−R p.
ment A is either:
We say that R ⊆
R is circular iff there is a proposition
Given a defeasible theory T = (S , D ), an ASPIC+ arguPrem(A) = ⋃︁ Prem(Ai).
1≤ i≤ n 1. 0/ ⇝ φ ∈ S ∪ D , Conc(A) = φ , Sub(A) = {A}, Prem(A) = {φ }; or 2. A1, . . . , An ⇝ φ where for all 1 ≤ i ≤ n, Ai are arguments, Conc(A) = φ , and there exists a rule {Conc(A1), . . . ,Conc(An)} ⇝ φ in S ∪ D , Sub(A) = ⋃︁ Sub(Ai) ∪ {A}, and 1≤ i≤ n
from the axioms or ordinary premises and working forwards towards conclusions. Observe that concepts such as attack or defeat, which are built on arguments, have no effect on the arguments constructed using forward chaining. Clearly, this has the potential to be computationally inefficient as arguments which are known to not affect the literals we are interested in may still be generated.
process through the introduction of informative partial arguments. Since backwards chaining potentially gives many choice points when selecting what to expand, in the next section, we describe a modular framework where different approaches for expansion selection can be used.
graph is a pair G = (V, E), where V is a set of nodes and E ⊆ V × V is the set of directed edges. A directed path from node v0 to node vn is a sequence (v0, v1, . . . , vn) such that for all i ∈ {0, . . . , n − 1}, (vi, vi+1) ∈ E. We say that an acyclic directed graph G = (V, E) is a directed rooted tree iff there exists a unique r ∈ V , called the root of G such that for all v′ ∈ V \ {r}, there is exactly one directed path from r to v′. Given a directed rooted tree G = (V, E), for all (v1, v2) ∈ E we define fst((v1, v2)) = v1, snd((v1, v2)) = v2. If (v′, v) ∈ E, we say that v′ is the parent of v, denoted as parentv. The node v ∈ V is a leaf of G if ∀e ∈ E, v ̸= fst(e). The set of all leaves of G is denoted as LEAVES(G).
Our approach for efcfiiently reasoning within ASPIC+ is based on the concept of backwards chaining which involves expanding a conclusion by selecting some applicable rules (i.e., those whose conclusion is the literal we are hoping to prove). During the expansion process, the objects we are manipulating are not arguments (as they are not rooted in axioms or ordinary premises). We therefore introduce informative partial arguments (Definition 11) which include the conclusion of an argument and a subset of the rules necessary to infer it, as well as context information gathered during the expansion. We begin by introducing some basic concepts which are key components of the backward chaining process (Definition 4 to Definition 10). We introduce this process through an illustrative example.
Example 1. Let us consider T = (S , D ), where S = {b → a, a → b, f → c, e → c, 0/ → g} and D = {{c, d} ⇒ b, n ⇒ b, g ⇒ d, h ⇒ f , 0/ ⇒ e, 0/ ⇒ h}. Assume that we want to build the arguments that conclude the target proposition a.
• Step 0: At the beginning of the construction, we have only ‘a’. We need to find all rules from T that have head ‘a’, and observe there is only one such rule b → a. From this rule, we see that there must be a proposition ‘b’ that supports ‘a’. • Step 1: Now, since we have the rule b → a, we need to find all rules from T that have head ‘b’.There are three such rules, a → b, {c, d} ⇒ b and n ⇒ b, these are evidence that b could be minimally supported in three different ways. • Step 2: We have three sets of rules that indicate our target proposition ‘a’ could be supported in these different ways, {a → b, b → a}, {{c, d} ⇒ b, b → a}, and {n ⇒ b, b → a}.
Although we only highlighted three steps in Example 1, we can make the following observations:
• The necessary information for backward chaining: At each step, the input data consists
of a set of rules and a set of propositions. Furthermore, it is possible to collect some
information during the backward chaining process. For example, we could collect the
preference information of defeasible rules as described in [
partial argument framework. We encode the (abstract) data structure of our framework via
Definition 4 (The P-structure). Given a logical language L , a defeasible theory T = (S , D ) and an arbitrary set of elements I, a P-structure is a triple ⟨L, R, i⟩ where L ⊆ L , R ⊆ S ∪ D and i ∈ I.
The set I is used to encode specific contextual information about the backward chaining process. Thus I may be different if we record the number of rules used in an argument or if we record the set of attacks against an argument. Returning to Example 1, we can encode its data as follows. The initial input at step 0 is a P-structure ⟨{a}, 0/ , i0⟩, the input at step 1 is a P-structure ⟨{b}, {b → a}, i1⟩, and there are three P-structures as inputs at step 2: • p1 = ⟨{a}, {a → b, b → a}, i′2⟩, • p2 = ⟨{c, d}, {{c, d} ⇒ b, b → a}, i′′2⟩, and • p3 = ⟨{n}, {n ⇒ b, b → a}, i′′′2⟩.
Definition 5 (Status of a P-structure). Given a P-structure ⟨L, R, i⟩ and a defeasible theory T = (S , D ), the status of a P-structure is • Complete iff L = 0/. • Enrichable iff R is not circular and ∀φ ∈ L , ∃r ∈ (S ∪ D ) s.t. head(r) = φ . • Pending if it is not complete or enrichable.
At step 2 in Example 1, p1 = ⟨{a}, {a → b, b → a}, i′2⟩, and p3 = ⟨{n}, {n ⇒ b, b → a}, i′′′2⟩ are pending, because the former has a circular set of rules whereas the literal part of the latter has no support from the defeasible theory.
Definition 6 (Support Function). Given T = (S , D ), we define a function supportT that takes as input a P-structure p = ⟨L, R, i⟩ and returns a set S ∈ 2(2S ∪D) such that if p is enrichable then for all s ∈ S, we know that {head(r)|r ∈ s} = L, and each r1 ∈ s, there is no r2 ∈ s such that head(r1) = head(r2) , and S is maximal (w.r.t. set inclusion). If p is not enrichable, then supportT (p) = 0/. In Example 1, given the input data p2 = ⟨{c, d}, {{c, d} ⇒ b, b → a}, i′′2⟩, supportT (p2) = {{ f → c, g ⇒ d}, {e → c, g ⇒ d}}. These two sets indicate that p2 can be enriched in two different ways.
takes as input a P-structure, a set of rules and returns a new P-structure that can be obtained by combining all these elements. The link function utilises two other functions: the control function that specifies how the status of the new P-structure is controlled and the extraction function that specifies how context information is extracted .
Definition 7 (Link Function). Given a defeasible theory T = (S , D ), rules Re ∈ 2S ∪D , a set of context information I, a P-structure p = ⟨L, R, i⟩, and a binary operator ▷◁: I × I → I which specifies how context information is accumulated 1, A link function is a function of the form ΣEXTR,CONT,▷◁(p, Re) = ⟨L′, R′, i′⟩, where: • L′ = CONT(p, Re) (see Definition 8), • i′ = EXTR(p, Re) ▷◁ i (see Definition 9), and • R′ = R ∪ Re.
of rules in Re. • CONT2(p, Re) =
r∈Re,r̸∈D bodies of strict rules in Re.
Definition 8 (Control Function). A control function CONT takes a P-structure p and a set of rules (evidence returned by support function) as inputs and returns a set of literals, i.e., CONT : (2L × 2S ∪D × I) × 2S ∪D → 2L .
Example 2. Given a P-structure p = ⟨L, R, i⟩ and Re ∈ 2S ∪D . We provide two examples of control functions, CONT1 and CONT2, such that: • CONT1(p, Re) = ⋃︂ body(r). This control function returns all propositions in the bodies r∈Re ⋃︂
body(r). This control function returns all propositions in the Note that while these two control functions are basic and do not make use of the P-structure p, more complex control functions can be defined.
After applying the control function to a P-structure, we have a set of propositions which require rules to support them within the new P-structure. We must decide which propositions to support so as to obtain new P-structures. Given that many strategies exist for doing so, we may apply different heuristics accordingly. An extraction function takes as input a P-structure and returns the information needed by our heuristic. For example, we may need to determine the number (or indeed the set) of all propositions which could be used by the rules supporting a P-structure.
are provided in Example 3. Definition 9 (Extraction Function). The function EXTR takes a P-structure p and a set of rules (the evidence returned by the support function) as input and returns an element of I, i.e., EXTR : (2L × 2S ∪D × I) × 2S ∪D → I.
Example 3. Given a P-structure p = ⟨L, R, i⟩ and Re ∈ 2S ∪D . We provide two examples of extraction functions, EXTR1 and EXTR2, such that: • EXTR1(p, Re) = {r|r ∈ Re, r ∈ D }. This extraction function returns all defeasible rules in Re. Here, I = 2S ∪D . • EXTR2(p, Re) = 2 × | R ∩ S | − | Re ∩ D |. This extraction function returns 2 times the number of strict rules in R minus the number of defeasible rules in Re. Here, I = N.
• naiveLink = ΣEXTR,CONT1,▷◁. This link function makes use of CONT1 (see Example 2) and assume the computational context ignores information I, thus EXTR and ▷◁ can be defined in an arbitrary way. • weakestLink = ΣEXTR1,CONT1,∪. This link function makes use of CONT1 (see Example 2),
EXTR1 (see Example 3), and ▷◁= ∪. • lastLink = ΣEXTR1,CONT2,∪. This link function makes use of CONT2 (see Example 2),
EXTR1 (see Example 3), and ▷◁= ∪.
The use of different types of context information (I) will be discussed in Example 4. When definitions of the control/extraction functions and ▷◁ are clear from the context, we will simplify ΣEXTR,CONT,▷◁ by writing Σ. We can now give the formal definition of the operations described in the steps of Example 1.
Definition 10 (Enrich Function π). Given T = (S , D ), a P-structure p = ⟨L, R, i⟩, and a link function Σ, the enrich function w.r.t. T and Σ is πT ,Σ : 2L × 2S ∪D × I → 2(2L × 2S ∪D× I) such that, when supportT (p) ̸= 0/: otherwise: πT ,Σ(p) = {Σ(p, e)|e ∈ supportT (p)}
πT ,Σ(p) = p The notation πT ,Σ(p) can be written as π(p) if T and Σ are known from the context. Now, all components that are necessary to describe the backward construction of the partial arguments have been formally defined, we can finally introduce the informative partial arguments that integrates all these concepts.
Definition 11 (Informative Partial Arguments). Given T = (S , D ), a link function Σ, an initial context information i ∈ I, a target proposition φ ∈ L , and a natural number z ∈ N, we define the directed rooted tree Gz,Σ,T = (Vzφ , Ezφ ) = ΠT ,Σ((Vzφ− 1, Ezφ− 1)), where G0,Σ,T = φ φ (V0φ , E0 ) = ({⟨{φ }, 0/, i⟩}, 0/), and ΠT ,Σ is defined as: φ ΠT ,Σ(G) = ((
⋃︂ v∈LEAVES(G) π(v)) ∪ V,
⋃︂ v∈LEAVES(G) {(v, v′)|v′ ∈ π(v)}) Symbols Σ and T can be omitted when they are known from the context. Each element of Vzφ is a P-structure, and it is referred to as an informative partial argument for φ . The root V0φ is the set containing the initial informative partial argument that wraps the target proposition φ together with the initial context information i. Gzφ is known as the tree of informative partial argument of φ at step z, it encodes the history of these z steps backward enrichment process starting from G0φ . If for all v ∈ LEAVES(Gzφ,Σ,T ), π(v) = {v} then we call Gzφ the terminal tree of informative partial argumentφfor φ . We denote the terminal tree as Gφ⊥ = (V⊥φ , E⊥φ), and the set {v|v ∈ V⊥φ , v is complete} as AΣ,T .
Example 4 (Cont’t Example 1). To demonstrate how trees of informative partial argument are indexed by different link function instantiations, we define a dummy-link function as followed: dummyLink = ΣEXTR2,CONT1,K where for every two natural numbers x, y ∈ N, K(x, y) = x. As shown in Table 1, a tree of informative partial argument for a is indexed by the link function and enrich steps. We choose 0/ a and 0 as initial context information respectively. G2,lastLink is a terminal tree, because ⟨{a}, {a → b, b → a}, 0/⟩ are of pending status and (⟨0/ , {c, d ⇒ b, b → a}, {c, d ⇒ b}⟩ is complete. z 0 1 2 3
LEAV ES(Gza,lastLink)
⟨{a}, 0/, 0/⟩ ⟨{b}, {b → a}, 0/⟩ ⟨{a}, {a → b, b → a}, 0/ ⟩ ⟨0/ , {c, d ⇒ b, b → a}, {c, d ⇒ b}⟩ ⟨ 0/, {n ⇒ b, b → a , n ⇒ b}⟩
} { Same as above (Terminated) LEAV ES(Gza,dummyLink)
⟨{a}, 0/ , 0⟩ ⟨{b}, {b → a}, 0⟩ ⟨{a}, {a → b, b → a}, 2⟩ ⟨{c, d}, {c, d ⇒ b, b → a}, 1⟩
⟨{n}, {n ⇒ b, b → a}, 1⟩ ⟨{ f , g}, { f → c, g ⇒ d, {c, d} ⇒ b, b → a}, 1⟩ ⟨{e, g}, {e → c, g ⇒ d, {c, d} ⇒ b, b → a}, 1⟩
Proposition 1. Given a defeasible theory T , Σ ∈ {naiveLink, weakestLink}, if AΣα,T ̸= 0/ , then, α for each A = ⟨L, R, i⟩ ∈ AΣ,T , based on T ′ = (S ′, D ′), S ′ ∪ D ′ = R, there is an unique ASPIC+ argument A′ that concludes α. Proof 1. According to the Definition 5 and Definition 11, we know that there is a natural number z such that A = ⟨ 0/, Rz, _⟩ ∈ Vzα . As defined in Example 2 and Example 3, naiveLink and weakestLink do not make selection on propositions that need to be supported in the next step, therefore, according to Definition 6, we know that for each 1 ≤ n ≤ z − 1, there exist Ren ∈ supportT (vn) such that R(n+1) = Ren ∪ Rn and {head(r)|r ∈ Ren} = Ln. Given A = {0/ , Rz, _}, for each r ∈ R(ez− 1), body(r) = 0/, therefore, each r ∈ Rze− 1 is an ASPIC+ argument (the base case of Definition 3) that concludes a unique l ∈ L(z− 1), the set of these ASPIC+ arguments is denoted as A′(z− 1). According to Definition 3 (inductive case (2)) we know that A′(z− 1) and Re (z− 2) forms a set of ASPIC+ argument A′(z− 2) such that each ASPIC+ argument in A′(z− 2) concludes a unique e l ∈ L(z− 2). Similarly, we can say that the set of ASPIC+ arguments A′n and R(n− 1) forms the set of ASPIC+ arguments A′(n− 1), each ASPIC+ argument in A′(n− 1) concludes a unique l ∈ L(n− 1), and we know L0 = {α}. So we have A′n ∪ · · · ∪ A′0 are all sub arguments of A′. Assuming that given T ′, there are more than one ASPIC+ arguments concludes α (A′′ and A′), it indicates that there are at least two sub-arguments of A′ and A′′ respectively, that concludes some proposition β (it is possible that β = α), in this case, according to Definition 6, R = S ′ ∪ D ′ will lead to more than one informative partial arguments, thus contradict to the assumption.
Definition 12 (Attack). Given T = (S , D ) and two trees of informative partial arguments Gzφ11,Σ1 = (V1, E1), Gzφ22,Σ2 = (V2, E2) for φ1 and φ2. An informative partial argument v1 = ⟨Lv1 , Rv1 , in f ov1 ⟩ ∈ V1 is attacked by v2 ∈ V2 if one of the following item holds: • ¬φ2 = φ where φ ∈ {head(r)|r ∈ Rv1 ∩ D }. We say v2 rebuts v1 on φ .
• ¬φ2 = φ where φ ∈ {name(r)|r ∈ Rv1 ∩ D }. We say v2 undercuts v1 on φ .
Proposition φ and φ2 = ¬φ are referred as the attacked proposition and the attacking proposition respectively. This definition indicates that attackers rely on attacking propositions only , so Gzφ22,Σ2 represents a family of attackers in which each family member is indexed by the choice of z2 and Σ2. Similarly, an argument is attacked only when an attacked proposition is included in its structure, so Gzφ11,Σ1 also represents a family of attacked arguments in which each family member is indexed by the choice of z1 and Σ1 such that ¬φ2 is included.
framework [
• b rebuts v on ¬φ2, b ∈ AφΣ22 and ∀a ∈ AΣ¬2φ2 we know that infoa ⪯ infob .
To determine if a rebut leads to a successful attack or not, we rely on an instantiation (Σ2) of the link function to indicate what information is required for comparison.
ified by Σ2 from all conflicting arguments. Σ2 and Σ1 are not necessarily the same, implying that the objective of constructing an argument could be independent from the process of determining whether or not an argument is defeated.
of query answering on a defeasible theory. The purpose of querying a defeasible theory is to determine if a statement is justified by the information contained in it. Being justified could be defined in a variety of ways, such as “there is a naive-complete argument of the query proposition and it is not attacked” or “ all naive-complete arguments of the query proposition are not attacked”. Example 5. Assume that a query proposition is justified if there is a naiveLink-complete argument of this query and it is not Σ-defeated by any other argument. Then given T = (S , D ), where S = {b → a, → e, f → ¬b, → g, h → ¬c, → i, j → ¬d, → k} and D = {c ⇒ b, d ⇒ c, e ⇒ d, g ⇒ f , i ⇒ h, k ⇒ j}, is ‘a’ justified and how much computation is necessary for drawing this conclusion?
The necessary computation for the construction all attackers are constrained by the instantiation of Σ. When adopting Σ = lastLink , the axioms in {→ e, → k, → j, → g} are not necessary for drawing the conclusion of this query whereas with Σ = weakestLink, we would require all rules in T .
a optimisation options: (1) Should we compute the AnaiveLink first then compute the Σ-defeat relation of each attacker; or (2) Should we compute the Σ-defeat relation whenever an attacker is identified a at each enrich step toward AnaiveLink ?
Option 1 puts us at the risk that the partial argument of proposition ¬b could be a defeater, if Σ = lastLink then all computations involving rules {d ⇒ c, e ⇒ d, → e} are not necessary. Option
Assume that there is no rule ( 0/ → e) in the given defeasible theory in Example 5, then all computation of the Σ-defeat relation would be not necessary.
Example 5 shows that there are two types of heuristic information: (1) The argument-level heuristic information (I) which has the scope of a path in a tree of informative partial arguments. (2) The defeasible-theory-level heuristic information which has the scope of the entire defeasible theory. Because we do not explore defeasible-theory-level heuristic information in this paper, we will focus on demonstrating the optimization brought about by adopting different link functions in the next section.
between using the lastLink and weakestLink. The implementation of weakestLink is the baseline and could be thought of as a close approximation to the calculation necessary to generate an
To evaluate the performance with larger size benchmarks and control the complexity, we reuse the justification criterion and dataset structure as shown in Example 5. The proposition a is justified in all benchmarks. The only leaf of GφΣ, φ ∈ L is denoted as leaf (GφΣ). The scale of our benchmarks3 is controlled by three parameters as shown in Figure 1. Here, Target-Depth (td) is the length of the path from the root to leaf (GanaiveLink). The Attacker-Depth (ad) is the target-depth of an attacker argument. Finally, the LastLink-Info-Depth (lid) is the length of the path from the root to leaf (GaΣ) for a given Σ. There are 10 attackers, and the values of ad and lid of all attackers are the same.
• Benchmark Asymptote: Set td and ad to be control variables and increase the value of lid at a given step 4. The benchmark includes 99 defeasible theories. As shown in Figure 2, in this case, the length of all attacker arguments is a constant. Adopting weakestLink requires the construction of a complete ASPIC+ argument, so the computational performance is relatively stable. Adopting lastLink would require only the computation necessary to meet the first defeasible rules, so the computation would take more time as the depth of the first defeasible increased, and in the worst case it will achieve the same performance level as adopting weakestLink.
and using criterion library for evaluation. Implementation details could refer to https://bitbucket.org/wuhao29/ informative-partial-argument/src/master/. 4td = 20, ad = 100, lid ∈ {10, . . . , 500} • Benchmark Overhead: Set td and lid to be control variables and increase the value of ad at a given step5. The benchmark includes 100 defeasible theories. As shown in Figure 3, the depth of the first defeasible rule in all attackers is a constant. The x-axis is the length of all attackers, while the y-axis is the time required to complete the computation. As the value of attacker depth increases, the performance of using weakestLink is increasing considerably compared to using lastLink. When the attacker depth is small enough, it is possible that adopting lastLink will take more computational time than adopting weakLink due to the overhead brought by extra operation defined by lastLink, However, this overhead is negligible as shown in figure 3. 5td = 20, ad ∈ {5, . . . , 500}, lid = 5.
The idea of constructing argument by backward chaining can be seen in works such as [
and provides modules for improving the expressiveness and the computational efficiency. Based on this framework, a solver could be further developed for tasks such as the ICCMA structured