# quantitative_claimcentric_reasoning_in_logicbased_argumentation__d0f3c388.pdf

Quantitative Claim-Centric Reasoning in Logic-Based Argumentation

Markus Hecher1 , Yasir Mahmood2 , Arne Meier3 , Johannes Schmidt4

1CSAIL, Massachusetts Institute of Technology, United States 2DICE group, Department of Computer Science, Paderborn University, Germany 3Institut f ur Theoretische Informatik, Leibniz Universit at Hannover, Germany 4Department of Computer Science and Informatics, J onk oping University, Sweden hecher@mit.edu, yasir.mahmood@uni-paderborn.de, meier@thi.uni-hannover.de, johannes.schmidt@ju.se

Argumentation is a well-established formalism for nonmonotonic reasoning with popular frameworks being Dung s abstract argumentation (AFs) or logic-based argumentation (Besnard-Hunter s framework). Structurally, a set of formulas forms support for a claim if it is consistent, subsetminimal, and implies the claim. Then, an argument comprises a support and a claim. We observe that the computational task (ARG) of asking for support of a claim in a knowledge base is brave , since many claims with a single support are accepted. As a result, ARG falls short when it comes to the question of confidence in a claim, or claim strength. In this paper, we propose a concept for measuring the (acceptance) strength of claims, based on counting supports for a claim. Further, we settle classical and structural complexity of counting arguments favoring a given claim in propositional knowledge bases (KBs). We introduce quantitative reasoning to measure the strength of claims in a KB and to determine the relevance strength of a formula for a claim.

1 Introduction

Argumentation is a nonmonotonic formalism in artificial intelligence around which an active research community has evolved [Atkinson et al., 2017; Amgoud and Prade, 2009; Rago et al., 2018; Baroni et al., 2018]. The popular frameworks dealing with the theory of argumentation include the abstract [Dung, 1995] and the logic-based [Besnard and Hunter, 2001; Besnard and Hunter, 2008; Chesnevar et al., 2000; Prakken and Vreeswijk, 2002] approach. The abstract setting, also known as Dung s theory of argumentation, focuses on formalizing the interaction between arguments in a graph-theoretic way. In other words, arguments are nodes in a directed graph, and the attack relation determines the interaction between arguments. Given such a framework, one is interested in computing the sets of arguments (called extensions) simultaneously accepted under a given semantics. In the logic-based setting, one starts with a knowledge base (KB) and searches for inclusion-minimal and consistent sets of formulas Φ (the support) that logically entail a

claim α. The pair (Φ, α) is then called an argument for the claim α. The computational problem of interest is the existence of an argument supporting a claim (ARG), and the relevance problem (ARG-Rel) is to determine whether a formula ψ is relevant to the claim α. Formally, ARG asks, given a set of formulas (the knowledge base) and a formula α, whether there exists a subset Φ such that (Φ, α) is an argument in , and ARG-Rel asks, whether there is an argument (Φ, α) in such that ψ Φ. The complexity of both reasoning problems is well understood for KBs formulated in propositi onal logic [Parsons et al., 2003] as well as in fragments thereof [Creignou et al., 2011; Creignou et al., 2014]. In addition, a structural complexity analysis has recently been employed to better understand the source of intractability [Mahmood et al., 2023] using different parts of the input as parameters. Despite the significant interest in the reasoning problems for logic-based argumentation, no prior research has explored the associated counting complexity. We argue that counting the number of arguments in support of a given claim is a logical choice when investigating the extent to which a claim is favored within the given knowledge base.

Example 1. We want to evaluate the arguments for and against candidates in an election. The argument A favors candidate X based on her education policy, which leads us to accept that X is favorable . Another argument (B) opposes this claim targeting the health care policy. Therefore, both claims are equally likely and have an acceptance strength of 50%. Subsequently, an argument C supports X in foreign policy. This increases the probability and thus the strength of the claim that X is indeed a favorable candidate.

Reasoning problems focusing on claims (instead of arguments) have received growing interest in abstract argumentation [Dvor ak and Woltran, 2020; Dvoˇr ak et al., 2023; Bernreiter et al., 2023; Baumann et al., 2023]. Specifically, claim-augmented argumentation frameworks (CAF) [Dvor ak and Woltran, 2020] extend Dung s AF by employing a conclusion-oriented perspective. Further, with the aim of exploring the justification status of claims, Fichte et al. (2023) introduced a quantitative measure of extensions supporting a particular claim. The increasing interest in the abstract setting focused on claim-based reasoning naturally motivates the exploration of claim strength in logic-based argumentation.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

This leads to the definition of a quantitative measure of the arguments supporting a given claim in the knowledge base. Contributions. As our first contribution, we categorize the classical and parameterized complexity of counting arguments to a claim (#ARG), as well as counting arguments where a given formula is also relevant (#ARG-Rel). We prove that both these problems are intractable and # co NPcomplete. Then we turn to parameterized complexity, which considers different parameters. We observe that both problems become FPT when parameterized by the number of variables in or the treewidth of the primal graph [Flum and Grohe, 2006] of the input KB. Table 1 gives a summary. For omitted proof details (marked by ), we refer to the appendix. We introduce a quantitative measure to determine the strength or likelihood of a claim in the given KB. Note that the argument existence problem (ARG) concerns only whether a claim is accepted in a given argument, and does not convey any further information about the given claim, such as how likely it is to be accepted within a given KB. As the following example illustrates, in certain corner cases, the problem ARG in logic-based argumentation can accommodate disputing claims that may not be acceptable even under the most lenient (admissible: defended against all attacking arguments) argumentation semantics. Accepting claims based solely on support in a knowledge base leads to the undesirable consequence of being unable to distinguish between weak and unlikely claims and those that are more likely. Example 2. Let = {x} { x ϕi | i n} be a KB where each ϕi is a CNF. Then the claim x is accepted since A = ({x}, x) is an argument. Now, for y = x, any argument that supports y in also supports y x. In other words, a single argument A over claims x and every other argument B claims x. Consequently, while both x and x are acceptable (as per ARG), x is clearly more likely than x. The main ingredient for our quantitative reasoning involves counting the arguments for a claim. Then, counting the relevant arguments for a claim with respect to a formula ψ informs how relevant ψ is for the given claim. We establish that one can also determine the claim strength in FPT-time when parameterized by the treewidth of an extended primal graph. Related Work. Probabilistic argumentation [Hunter and Thimm, 2017; Fazzinga et al., 2015; Alfano et al., 2020] focuses on weighting arguments with probabilities. Furthermore, a similar work in logic-based argumentation [Hunter, 2012; Hunter, 2013; Riveret et al., 2007] provides a probability distribution for arguments to model the degree of an argument being true. This whole research area is orthogonal to our setting, since we focus on the (conditional) plausibility of claims, as in the Bayesian setting. Further, our approach does not focus on the uncertainty of arguments, since we evaluate the strength of claims corresponding to certain arguments. Existing research on the justification status of arguments [Wu and Caminada, 2010; Baroni et al., 2016; Baroni and Riveret, 2019] explores different levels of acceptance or rejection for arguments. In addition, Baroni et al. (2016) also emphasized statement justification as a topic of independent interest. Nevertheless, their approach explores the status of an argument (or statement) in different extensions by finding all

Parameter Problem Complexity Ref.

#ARG(-Rel) # co NP-c. T. 12, C. 13 | var( )| #ARG(-Rel) FFPT C. 14 | var(α)| #ARG(-Rel) #W[1]-h. C. 14

Problem Runtime UB Runtime LB Ref.

#ARG(-Rel) exp(2, O(k)) exp(2, o(k)) T. 19, C. 20/22

Table 1: Results overview. For the runtime bounds, k = tw(Ge I) and the polynomial factors in | var( ) var(α)| have been omitted.

the acceptance labels for an argument (statement). Recently, Fichte et al. (2023) introduced a fine-grained mode between credulous and skeptical reasoning (some, respectively, any extension covering a claim) for the acceptability of claims. They propose assigning a probability value in [0, 1] depending on how many extensions in an AF cover the given claim. In this work, our focus lies (as the name suggests) in the quantitative aspect of claim justification in logic-based setting. There exists research aiming to assess the strength of an argument based on the number of attackers and defenders of the target argument. Besnard & Hunter (2001) proposed aggregation functions to evaluate the relative strength of an argument, considering its (recursive) argument tree (attackers, their attackers, etc.). Although the authors suggest counting arguments for and against a claim, a complexity analysis for counting arguments is still missing. Similarly, Pu et al. (2015) considered the problem of counting the number of attackers and defenders for a topic argument in the abstract setting. This distinguishes their work from our logicbased approach. Gradual semantics [Amgoud et al., 2018; Amgoud and Doder, 2018] are methods for evaluating the overall strength of arguments in a (weighted) argumentation framework, which assumes a set of arguments, the relationship between them, and an initial weight of each argument. Finally, Amgoud et al. (2008) presented an approach to compare different arguments with the goal of evaluating the status for each claim (option in their terminology). Their proposed system takes as input a set of arguments together with an attack and a preference relation between arguments, and returns a status for each option. While our approach determines the acceptance status for each claim, we do not consider argumentation semantics from the AFs and focus on the logic-based approach instead. So, we assume a KB and a set of claims as input, rather than the set of arguments and the interaction between them, as required by the former.

2 Preliminaries We assume familiarity with basic notions in complexity theory (cf. [Sipser, 1997]) and use complexity classes P, NP, co NP, NPNP = ΣP 2. For a set S, we write |S| for its cardinality. Abusing notation, we will use |w|, for a string w, to denote its length. If φ is a formula, var(φ) denotes its set of variables. Symbols and denote the constants 1 and 0, respectively. Further, we assume a reasonable encoding computable in polynomial time encoding variables in binary. Quantified Boolean Formulas. For a Boolean formula F, we write F(X1, . . . , Xl) to indicate that

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

X1, . . . , Xl var(F). A quantified Boolean formula (q Bf) ϕ (in prenex normal form) is of the form ϕ = Q1X1.Q2X2. QℓXℓ.F(X1, . . . , Xℓ), where for 1 i ℓ(ℓis the (quantifier) rank), we have Qi { , } and Qi = Qi+1, the Xi are disjoint, nonempty sets of Boolean variables, and F is a Boolean formula. We let matrix(ϕ) := F and say that ϕ is closed if var(matrix(F)) = S i ℓXi. The semantics are defined as x.ϕ ϕ[x 7 1] ϕ[x 7 0] and x.ϕ ϕ[x 7 1] ϕ[x 7 0] for a variable x. W.l.o.g., assume that matrix(ϕ) = ψCNF ψDNF, where ψCNF is in CNF (conjunctive normal form) and ψDNF is in DNF (disjunctive normal form). Note that, depending on Qℓ, either ψCNF or ψCNF is optional, more precisely, ψCNF might be , if Qℓ= , and ψDNF is allowed to be , otherwise. The problem ℓ-QBF asks for a closed q Bf ϕ = X1.ϕ of rank ℓ, whether ϕ 1. The problem #ℓ-QBF asks for a closed q Bf X1.ϕ of rank ℓ, to count assignments α to X1 such that ϕ[α] 1. For brevity, we sometimes omit ℓ.

Counting Complexity. A witness function w is a mapping w: {0, 1} P <ω({0, 1} ), i.e., mapping to a finite subset of {0, 1} (note that this notion can easily be generalized to arbitrary alphabets, not just the binary one). Such functions associate with the counting problem given x Σ , find |w(x)| . If C is a decision complexity class then # C is the class of all counting problems whose witness function w satisfies (1.) there is a polynomial p such that for all y w(x), we have that |y| p(|x|), and (2.) the decision problem given x and y, is y w(x)? is in C. A parsimonious reduction between two problems #A, #B preserves the cardinality between the witness sets and is computable in P. Typical counting complexity classes associated with hard counting problems are # P and # co NP. Both classes comprise complete problems that are believed not to be polynomial time solvable. For more background on counting complexity classes we refer the reader to [Durand et al., 2005].

Parameterized Complexity. We give a brief introduction to parameterized complexity [Downey and Fellows, 1999]. A parameterized problem (PP) is a subset of Σ N for some alphabet Σ. For an input (x, k) of a PP, we call k the parameter of that input. The parameterized complexity class FPT is the class of all parameterized problems that can be solved in time f(k) |x|c for some computable function f and constant c. An FPT-reduction from a parameterized problem A to a parameterized problem B is a FPT-time computable function f such that (i) (x, k) A if and only if f(x, k) B, and (ii) if there exists some computable function g such that for all f(x, k) = (x , k ) we have k g(k). The complexity class W[1] is defined as the set of all problems that can be accepted by a tail-nondeterministic and kbounded Turing machine1.

Parameterized Counting. The area of parameretized counting complexity has been initiated by Flum and

1A tail-nondeterministic TM reads all nondet. bits at the end of the computation while for a k-bounded one, the number of nondet. bits is limited to f(k) log |x| many for all inputs (x, k).

Grohe [Flum and Grohe, 2004] as well as Mc Cartin [Mc Cartin, 2006]. Similarly, as on the decision side, the complexity class #W[1] is the class of all parameterized counting problems reducing to counting k-cliques in a given graph. Two good surveys in this area are [Curticapean, 2019; Haak et al., 2023]. A parameterized function is a function F : {0, 1} N N. If C is a complexity class and a parameterized function F belongs to C, we say that F is Ccomputable. Intuitively, we count the number of solutions of a parameterized function F and associate them directly with the function value F(x, k). We let FFPT be the class of parameterized functions that are computable in FPT-time. Tree Decompositions (TD) and Treewidth. We use rooted (directed) trees T = (N, A) with a root root(T) and a node t N. Here, we denote by children(t) the set of all nodes t , which have an edge (t, t ) A. Let G = (V, E) be a graph. A tree decomposition (TD) of a graph G is a pair T = (T, χ), where T is a rooted tree, and χ is a mapping assigning to each node t of T a set χ(t) V , called bag, s.t.: 1. V = S t of T χ(t) and E S t of T {{u, v} | u, v χ(t)} 2. for each s lying on any r-t-path: χ(r) χ(t) χ(s). Then, define width(T ) := maxt of T |χ(t)| 1. The treewidth tw(G) of G is the minimum width(T ) over all tree decompositions T of G. Notice that for all v V , we have a unique node t with v χ(t ) such that either t = root(T) or there is a node t of T with children(t) = {t } and v / χ(t). Denote the node t by last(v). Finally, notice that for any fixed w 1, one can decide in linear time if a graph has treewidth at most w and, if so, to compute a TD of width w [Bodlaender, 1996]. Here, we assume only TDs (T, χ), where for every node t of T, we have that |children(t)| 2. Such a TD, while maintaining the same width, can be computed from any TD in linear time [Bodlaender and Koster, 2008]. Treewidth and q Bfs. For a q Bf ϕ with matrix(ϕ) = ψCNF ψDNF, define the primal graph Gϕ := Gmatrix(ϕ), whose vertices are var(matrix(ϕ)). Two vertices of Gϕ are adjoined by an edge, whenever the corresponding variables share a clause/term of ψCNF/ψDNF. Let exp(i, p) be exp(i 1, 2p) if i > 0 and p otherwise. For the following result, assume that poly(n) is any polynomial for given positive integer n. Proposition 3 (Chen, 2004). For any arbitrary q Bf ϕ of quantifier rank ℓ> 0, the problem ℓ-QBF can be solved in time exp(ℓ, O(tw(Gφ))) poly(|var(ϕ)|). Note that, under the exponential time hypothesis (ETH) [Impagliazzo et al., 2001], one cannot significantly improve this runtime: ETH implies that SAT = 1-QBF can not be decided in time better than 2o(|var(φ)|) for a formula φ. Proposition 4 (Fichte et al., 2020). Under ETH, for any arbitrary q Bf φ of quantifier rank ℓ> 0, problem ℓ-QBF cannot be solved in time exp(ℓ, o(tw(Gφ))) poly(|var(φ)|). Logic-based Argumentation (LBA). Formulas are propositional; we follow the notion of Creignou et al. [2014]. Definition 5 (Besnard and Hunter [2001]). Given a set of formulas Φ and a formula α, one says that (Φ, α) is an argument (for α) if (1) Φ is consistent, (2) Φ |= α, and (3) Φ is subsetminimal w.r.t. (2). In case of Φ , (Φ, α) is an argument

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

in . We call α the claim, Φ the support of the argument, and the knowledge-base. We consider two problems from the area of logic-based argumentation, namely ARG, and ARG-Rel. The problem ARG asks, given a set of formulas and a formula α, is there a set Φ such that (Φ, α) is an argument in ? The problem ARG-Rel asks, given a set of formulas , and formulas ψ and α, is there a set Φ with ψ Φ such that (Φ, α) is an argument in ? Given a KB and formula α, then Args(α, ) denotes the set of all arguments for α in . Further, given a formula ψ, then Rel-Args(ψ, α, ) denotes the set of (relevant) arguments for α in containing ψ. We define the counting problem #ARG of computing |Args(α, )| for input ( , α) and the counting variant of #ARG-Rel to compute |Rel-Args(ψ, α, )|. TDs for LBA. If φ is a formula in CNF, then the primal graph Gφ is the undirected graph G = (V, E) such that the vertex set V is var(φ) and {u, v} E if and only if the variables u, v share a clause in φ. Similarly, if φ is in DNF, then the edges are drawn w.r.t. shared term variables instead. For a graph G = (V , E ), we also write V (G) for V and E(G) for E . For an LBA-instance ( , α) the primal graph G( ,α), is defined as the union of the primal graphs of each formula from {α}. That is, the vertex set V (G( ,α)) = S φ {α} V (Gφ) and E(G( ,α)) = S φ {α} E(Gϕ).

Decomposition-Guided Reductions. Inspired by work of Fichte et al. (2021), a decomposition-guided (DG) reduction R is a function that takes both a problem instance I and a TD T = (T, χ) of GI, and returns a q Bf φ with matrix(ϕ) := F. A DG reduction has to yield a TD T = (T, χ ) of GF . Such a reduction has to construct φ from a TD node s point of view. In that point of view, for any node t of T, the constructed bag χ (t) functionally depends on the original bag χ(t), but also on the constructed bags χ (t1), . . . , χ (to) of its child nodes {t1, . . . , to} = children(t). This results in a function f with an input of a TD node t, its bag χ(t), and a set χ (children(t)) = { χ (ti) | ti children(t) } of constructed bags for the child nodes of t. It follows that, as the width(T ) is bounded by O(maxt of T (|χ(t)|)), also the treewidth of the resulting q Bf is at most O(maxt of T {|f(t, χ(t), χ (children(t))|}).

2.1 Quantitative Claim-Centric Reasoning We propose a mode of reasoning that captures the quantitative (probabilistic) aspects of claim acceptance in logic-based argumentation. Accordingly, rather than asking whether a claim is accepted or not, a natural reasoning problem is to inquire how strongly (or how likely) the claim is supported in the KB. This mode of reasoning in argumentation allows to draw reasonable conclusions about claims, rather than just deciding whether a claim is accepted or not. Furthermore, this quantitative reasoning also allows us to directly compute a justification score or probability for claims at the level of KBs. The question we pose is: given a claim α (for simplicity, a literal), how strongly (or likely) is α acceptable in . We observe that counting supports (Φ) for a claim (α) has not been considered (up to our knowledge). We first characterize its computational complexity.

Example 6 (Counting Arguments). Let C consist of all the candidates in an election, α := X be our favorite candidate, and the KB contain poll results appropriately encoded in propositional logic. For example, a proposition xs encodes that candidate X promotes policy s, along with ps (participant p desires s) and ds (s is desirable), where s {education, health, taxes, welfare}. Then for each participant p and candidate X, contains formulas of the form (xs ds X) and ps ds. Clearly, {xed, ped, ped ded, (xed ded X)} yields a support for X if contains both xed and ped. Then |Args(X, )| counts the number of arguments from all participants in favor of X and |Rel-Args(ded, X, )| gives the number of arguments in favor of X relevant to their education policy.

We want to point out some interesting properties concerning the counting of (relevant) arguments for claims in propositional KBs. Notice that the support for a claim is a subset of the KB , and there are at most exponentially many of them (precisely, 2n many where n is the number of formulas in ). It is easy to construct examples where the number of arguments for a claim is indeed exponential.

Example 7. Let = {xi (yi zi), yi xi+1, zi xi+1 | 0 i n} and α = (x0 xn). Then, a support for α contains each xi (yi zi) and at least one of yi xi+1 or zi xi+1 for i n. Clearly, there are exponentially many (minimal) supports for α in total.

Also note that counting relevant arguments is indeed an interesting problem, since certain formulas in a KB may be more essential than others when constructing support for a claim. This phenomenon is further highlighted next.

Example 8. Let = {x yi, (y1 . . . yn) z, | i n} and α = (x z). Then, a support for α contains the formula (x yi) for some i n and the formula (W i yi) z. Clearly, the formula (W i yi) z is more relevant than any other formula in for α.

While the number of supports is an interesting measure for claims, it falls short when it comes to assessing and comparing the likelihood of different claims. Consequently, one would like to compute the strength or likelihood of a claim compared to other claims in a given knowledge base.

Claim Strength and Likelihood. We assume a set C of possible claims is given as input. This is indeed a reasonable assumption, since in the abstract setting for AFs and claimaugmented AFs [Dvor ak and Woltran, 2020], a set of arguments and their claims is always given. The set C can be all the claims for which arguments can be constructed in , or only the claims we want to compare against the given α. Furthermore, if we do not restrict the set of claims, one can construct infinitely many arguments from a finite KB, since an argument for x also yields an argument for x x, and so on. Indeed, it seems natural to consider all claims and compare the strength of justification relative to each other. Given a KB , claim α and a set C of claims, we denote βC = W c C c. Then, the following formula allows us to compute the strength of α relative to all the claims in C:

str(α, , C) = |Args(α, )| |Args(βC, )|.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Moreover, we define the likelihood of α relative to claims in C via the following formula:

lhd(α, , C) = |Args(α, )| Σc C|Args(c, )|.

The term in the denominator is a notable factor that distinguishes the strength of a claim from its likelihood. Interestingly, the presence of the disjunction (βC) in Args(βC, ) results in an undercount of arguments for claims due to the minimality of the supports. In contrast, summing over all arguments for claims in set C, expressed as Σc C|Args(c, )|, leads to overcounting. This is further emphasized below.

Example 9. Let = {x, x c, c zi, zi d | i 3} and C = {c, d}. Then Args(c) = {({x, x c}, c)} and Args(d) contains ({x, x c, c zi, zi d}) for i 3. Now, Args(c d) = {({x, x c}, c)} since arguments corresponding to d are not subset-minimal. As a result, str(d, , C) = 3 str(c, , C). Intuitively, arguments supporting claim d inherently serve as arguments for d c, establishing d as a stronger claim than c.

Example 10. Let = {c d} and C = {c, d}. Then, Args(c) = {({c d}, c)} and Args(d) = {({c d}, d)}. Now, lhd(c, , C) = 0.5 = lhd(d, , C). Both claims are equally likely and equally strong as str(c, , C) = str(d, , C). Intuitively, both claims are acceptable with a likelihood of 50%.

Indeed, both measures are valuable for comparing the justification of claims within logic-based argumentation. In addition, the probability of a claim is further motivated from a fact-checking perspective: the truth value of a fact is calculated by considering the number of arguments in favor of the fact and then determining the ratio of all possible arguments over the given knowledge base [Syed et al., 2019]. The relevance strength of a formula ψ for a claim α is based on counting relevant arguments (|Rel-Args(ψ, α, )|):

str(ψ, α, ) = |Rel-Args(ψ, α, )| |Args(α, )|.

Example 11 (Claim Strength & Likelihood). We count all the arguments in favoring X and take the ratio with the count of arguments favoring any candidate in C. This indicates how much X is favored in our KB compared to other candidates in C. Similarly, the ratio of |Args(X, )| and Σy C|Args(y, )| gives the probability that X is the favorite among C. Interestingly, the two measures for each candidate X coincide in . Finally, str(ded, X, ) informs the impact of the policy on education (ded) behind X being the favorite.

3 Complexity of Counting Arguments

We now establish the complexity of counting arguments for knowledge bases formulated in propositional logic.

3.1 Classical Complexity We characterize the classical complexity of counting (resp., relevant) arguments for a claim (with respect to a formula).

Theorem 12 ( ). #ARG is # co NP-complete.

Note that the relevance problem (ARG-Rel) has higher complexity than the existence problem (ARG) due to the reduction ( , α) 7 ( {x}, α x, x), where x is a new

proposition that does not appear in {α}. It turns out that this is in fact a parsimonious reduction, preserving the number of supports Φ for α in and relevant supports for α x in {x}. Furthermore, the membership in # co NP can also be established in a similar way as for #ARG, resulting in the same complexity of counting the relevant supports for the claim given a formula. This leads to the following corollary. Corollary 13. The problem #ARG-Rel of counting relevant arguments is # co NP-complete.

3.2 Parameterized and Structural Complexity We derive various parameterized complexity results.

Parameters: Size of Claim and KB Mahmood et al. (2023) explored the parameterized complexity of the decision problems ARG and ARG-Rel. For parameter | var( )| both problems are FPT (Thm 5.13) and the algorithm can be easily extended to count the number of solutions. For | var(α)| both problems are W[1]-hard (Lem 5.8, Thm 5.10). Close inspection reveals that the employed reductions are parsimonious, yielding the following corollary. Corollary 14 ( ). #ARG and #ARG-Rel parameterized by | var( )| are in FFPT, and by | var(α)| are #W[1]-hard.

Parameter: Treewidth We derive treewidth-aware reductions between #ARG and #2-QBF to count the extensions as well as compute the claim strength and likelihood in FPT-time when parameterized by treewidth of a suitable graph representation of the input. To achieve this, we reduce an instance ( , α) of ARG to an instance of 2-QBF using a similar idea as employed by Fichte et al. (2021). Note that the known-reductions between ARG and 2-QBF (given below) are restricted to the case when includes clauses and do not preserve the number of solutions for the two instances. DG-reductions for Clausal KBs. Let = {Ci, | 1 i n} be a collection of clauses and α be a Boolean formula in DNF. Towards the reductions, a variable ei for each Ci encodes whether Ci is contained in the support, resulting in the set E := {ei | 1 i n} of support variables. Then, let M denote the set of variables over var( ) = S i n var(Ci). Moreover, let N := var( {α}) and let N denote the renaming of variables in N. That is N := { xi | xi N} and each xi is a fresh variable. Finally, β denotes each β {C, α, } over renamed variables N. Then, let cons (E, M) := V Ci ( ei Ci) and ent ,α(E, N) := W Ci (ei Ci) α. To preserve the treewidth linearly, both subformulas are split into a conjunction from each node s perspective in the tree-decomposition. To achieve this, let T = (T, χ) be a TD of G( ,α). Then, define a labeled TD (LTD) T = (T, χ, δ) of T , where labeling δ: T is such that δ(t) t and = S t of T {δ(t)}. An LTD can be easily obtained from any TD without changing the width by copying nodes accordingly. The labeling function guarantees that δ(t) contains Ci if, and only if, Ci t. Next, assume such an LTD T = (T, χ, δ) of T and construct the following formula RARG 2-QBF(I, T ) :=

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

x, y p, q, z

Figure 1: A TD for from Example 15 (left) together with the clause-labeling for each bag (right)

E, M. N.φARG(E, M, N), where φARG is built for every node t of T by cons{δ(t)}(E, M) ent{δ(t)}(E, N). We extend the DG-reductions from above in three folds. First, the KB includes formulas in CNF, not just clauses. Second, the presented reduction is a bijection and hence the number of solutions to the resulting 2-QBF-instance is same as the number of arguments for the given claim in . Third, the reduction incorporates the minimality of supports and therefore only counts valid arguments as presented in Definition 5.

Generalization to CNFs. The first extension poses a nontrivial challenge, since the clauses of a formula can be spread over multiple bags. Recall that (by definition) in the clausal KBs, for each clause C and a TD T for , there is a node t T such that the bag χt covers C. Then, the labeling (δ) of T relates each bag in T to the clauses it contains. However, if contains formulas ϕ in CNF, then it is not guaranteed that all clauses of ϕ are contained in a bag. This challenge can alternatively be attributed to the graph representation (G ) of the KB . If G is considered as the union of primal graphs Gϕ for each formula ϕ , the graph encodes only the connectivity of variables in clauses. However, it does not represent the participation of variables or clauses in a formula. The following example further illustrates this issue.

Example 15. Let := {ϕ, ψ, β} where each γ is a CNF with clauses named as γi for i 3. Precisely, let ϕ1 = (x y), ϕ2 = (y z p), ϕ3 = (r s t), ψ1 = (y z p q), ψ2 = (p q z), β1 = ( y p q), β2 = (y r s) and β3 = ( r s t). Now, consider the TD for G depicted in Figure 1. For clarity, we label bags with corresponding clauses it covers (2nd TD on right). Then, the bag covering ϕ3 (variables r, s, t) is disconnected from the bags covering the remaining clauses (ϕ1 and ϕ2) of ϕ.

As Example 15 shows, clauses within the same formula can be covered by unrelated bags. Now, following a similar strategy as for the clausal KBs, one would use a support variable ei for i 3. Then additionally the bags covering clauses β1 and β2 in the TD must contain e1. But this is undesirable due to the resulting blow-up in the treewidth of the primal graph if contains many formulas stretched in this way. To overcome this limitation, we extend the graph representation for by considering the extended primal graph denoted as Ge . More precisely, each formula ϕi contains a new proposition fi (called formula name), so that the variables in ϕi are also connected to fi. This extension of the primal graph encodes the participation of variables in a formula and the relationship between variables that do not share a clause but a formula. This yields a set F = {fi | 1 i n} of variables encoding the formula names for a KB . Additionally, the label (δ) in a LTD can be extended to guarantee

that δ(t) contains part of the formula ϕi if and only if fi t. This way, we can still access a formula ϕi from a TD even if there is no single bag that covers entire ϕi. Note also that connecting fi to each var(ϕi) increases the treewidth for ϕi by at most one over the treewidth for ϕ (simply add fi to each bag for the TD of ϕ). To incorporate the addition of these variables into our reduction, we use fi for ϕi to also encode whether ϕi is contained in the support, and use the set F := {fi | 1 i n} to serve the support variables. As before, let M denote the set of variables over var( ) = S ϕ var(ϕ). Moreover, let N := var( {α}) and let N := { xi | xi N} denote the renaming of variables in N. Finally, by β, we denote each β {ϕ, C, α, } over renamed variables. Then, we let cons (F, M) := V ϕi ( fi ϕi) and ent ,α(F, N) := W ϕi (fi ϕi) α. Equivalently, we have cons (F, M) := V ϕi V Cij ϕi( fi Cij), and

ent ,α(F, N) := W ϕi W Cij ϕi(fi Cij) α. Then,

ψ ARG = F, M. N.(cons (F, M) ent ,α(F, N)) yields the desired (intermediate) 2-QBF. If we consider the extended primal graph for ( , α), ψ ARG already preserves the treewidth linearly. This is due to the additional edges between fi and var(ϕi) of each ϕi . However, this linear preservation of treewidth will break down when imposing the minimality condition over arguments. Thus, we split the two formulas. Let T = (T, χ) be a TD of Ge ( ,α). Moreover, let ϕt i (resp., αt) denote the clauses of ϕi (terms of α) contained in bag t and t denote the collection of all such ϕt i. We define a labeled TD (LTD) T = (T, χ, δ) of T , where labeling δ: T is such that δ(t) t {αt}. Finally, we let δ(t1) δ(t2) denote the set {ϕt1 i ϕt2 i | ϕi }, then = t T {δ(t)}. An LTD can be easily obtained from any TD without changing the width by copying nodes accordingly. Furthermore, our labeling function also guarantees that δ(t) contains ϕt i if, and only if, fi t. Next, we assume such an LTD T = (T, χ, δ) of T , and let E = F {et i | i n, t T}, L = {ℓt | t T}, S = {st i | i n, t T} sets of variables. Then, we construct the formula

ψARG:= E( M.φcons(E, M) L S N.φent(E, L, S, N)),

where φcons(E, M) is built for every node t of T as the conjunction of Formulas (1) (2), which can be converted into CNF. Formula φent(E, L, S, N)) is built for every t of T as the disjunction of (3) (6), which can be converted into DNF. To obtain CNF and DNF as claimed, one can use Tseitin [Tseitin, 1983] or assume each bag considers at most one clause in ϕt i (easily obtainable by, e.g., just duplicating bags). This does not increase the treewidth and only increases TD size linearly.

t children(t) et i

for ϕt i t, t T (1)

fi elast(i) i for ϕi (2)

(st i et i ϕt i _

t children(t) st i ) for ϕt i t, t T (3)

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

t children(t) ℓt for t T (4)

slast(i) i for ϕi (5)

ℓlast(α) (6)

The purpose of Eqs. (1) (2) is to guide along the TD whether a formula ϕi is taken in the support or not. Then Eq. (3) guides a contradiction along the TD, which together with Eqs. (4) (6) guarantee that each term of α is indeed explained. Lemma 16 (Correctness, ). Let ( , α) be an instance of ARG. Then, there is a support Φ such that (Φ, α) is an argument in if and only if ψARG is true. Since ψARG is constructed for each node of T, it is easy to see that the DG reduction preserves the treewidth linearly. Lemma 17 (TW-Awareness, ). Let I = ( , α) be an instance of ARG and T = (T, χ, δ) be an LTD of a TD T of Ge ( ,α) of width k. Then, the reduction RARG 2-QBF(I, T ) constructs a q Bf ψARG that linearly preserves the width. More precisely, we have that tw(Gmatrix(ψARG)) O(k). Counting Arguments. Our reductions work for the decision variant, but when it comes to runtime upper bounds for counting, double exponential bounds are not guaranteed since only E includes free variables in ψARG. Nevertheless, observe that if we do not have full quantifier alternations, the validity of quantified Boolean formulas is easier than in the general case. This still holds for treewidth (under ETH) and counting, which we will utilize afterwards. Proposition 18 ( ). Let Q be a QBF over free variables V and with ℓalternating quantifier blocks such that the innermost formula is of the form ( M.C) ( N.D) with C being in CNF and D being in DNF. There is an algorithm for counting the number of assignments θ over V such that Q[θ] evaluates to true, in time exp(ℓ+2, O(k)) poly(| var(Q)|), where k is the treewidth of the primal graph GC D. Clearly, in ψARG, there is no quantifier alternation between variables M of φcons and L, S, N of φent (except those over E). Consequently, we apply Proposition 18 and reduction RARG 2-QBF above, where E is not existentially quantified, but the set of free variables, to obtain an upper bound exp(2, O(k)) poly(| var(Q)|) for counting solutions. Theorem 19 (Runtime UB, ). Let I = ( , α) be an instance of ARG. Then, #ARG can be solved in time exp(2, O(k)) poly(|var( ) var(α)|), where k = tw(Ge I). Unluckily, this can probably not be significantly improved. This follows from the runtime lower bounds for the decision problem ARG [Fichte et al., 2021, Thm. 12]. Corollary 20 (Runtime LB, ). Let I=( , α) be an instance of ARG. Then, under ETH, the problem #ARG cannot be solved in time exp(2, o(tw(Ge I)) poly(|var( ) var(α)|). One cannot expect to significantly improve the DG reduction. Corollary 21 (TW-LB, ). Let I = ( , α) be an instance of ARG. Under ETH, there is no reduction R from ARG to 2-QBF yielding a q Bf ψARG in time exp(2, o(tw(Ge I))) poly(| var( ) var(α)|) with tw(GψARG) o(tw(Ge I)).

Adding Minimality. Next, we modify our reductions such that only subset-minimal supports are selected and counted. The idea is to use an additional formula ensuring that, whenever E provides a support, then for all other sets ˆE: either ˆE is not a support for α, or ˆE E. To achieve this, we use variables ˆE = {ˆet i | i n, t T} and ˆ M. Moreover, we use Q = {qt, qi | t T, ϕi }, called equality variables to guide along the TD whether E and ˆE are (un)equal. Let ψm(E) denote the formula ˆE, ˆ M, Q, L, S, N( φcons( ˆE, ˆ M) φent( ˆE, L, S, N) φ ˆ E E(E, ˆE, Q)), where formulas φcons and φent are built for

every node t of T as before, and φ ˆ E E(E, ˆE, Q) a collection of DNF formulas: ˆfi fi for ϕi (7)

(qi fi ˆfi) for ϕi (8)

ϕt i δ(t) qi _

t children(t) qt for t T (9)

qroot(T ) (10)

Eq. (7) allows a support given by ˆE to contain a formula not in E, then Eq. (8) defines inequality and Eq. (9) guides the inequality along TD. Finally, Eq. (10), allows equal supports over E and ˆE. Then our reduction yields the formula E(ψARG(E) ψm(E)). Again, since the additional formulas are constructed for each node of T, it is easy to see that the DG reduction is correct and preserves the treewidth linearly. Counting Relevant Arguments. In order to compute #ARG-Rel(ψ, α, ) for a formula ψ and claim α in , we force a support to contain ψ by simply plugging-in the formula name (say f0) for ψ in RARG 2-QBF(I, T ). This achieves that only those supports are counted that contain ψ. Corollary 22 (Tight runtime bounds for #ARG-Rel, ). Let I = ( , ψ, α) be an instance of ARG-Rel. Then #ARG-Rel can be solved in time exp(2, O(k)) poly(|var( ) var(α) var(ψ)|), where k = tw(Ge I). Under ETH, the problem #ARG-Rel cannot be solved in time exp(2, o(tw(Ge I)) poly(|var( ) var(α) var(ψ)|).

4 Conclusion We explored the classical and structural complexity for counting arguments in propositional knowledge bases. To the best of our knowledge, this is the first paper to address the complexity of counting in logic-based argumentation. Regarding the structural complexity, we established tight runtime bounds for #ARG and #ARG-Rel under the parameter treewidth. The upper bounds were determined using a technique described in Proposition 18, which is interesting and useful in itself for solving QBFs. Finally, we proposed and motivated quantitative reasoning for claims to determine their relative strength and likelihood in a given knowledge base.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Acknowledgments

The work has received funding from the Austrian Science Fund (FWF), grants J 4656 and P 32830, the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation), grants TRR 318/1 2021 438445824 and ME 4279/31 (511769688), the European Union s Horizon Europe research and innovation programme within project ENEXA (101070305), the Society for Research Funding in Lower Austria (GFF, Gesellschaft f ur Forschungsf orderung N O), grant Exz F-0004, the Swedish Research Council (VR), grant 2022-03214, as well as the Vienna Science and Technology Fund (WWTF), grant ICT19-065. Further, parts of this work have been carried out while Hecher was visiting the Simons institute for the theory of computing at UC Berkeley.

[Alfano et al., 2020] Gianvincenzo Alfano, Marco Calautti, Sergio Greco, Francesco Parisi, and Irina Trubitsyna. Explainable acceptance in probabilistic abstract argumentation: Complexity and approximation. In KR 20, pages 33 43. IJCAI Organization, 2020.

[Amgoud and Doder, 2018] Leila Amgoud and Dragan Doder. Gradual semantics for weighted graphs: An unifying approach. In Sixteenth International Conference on Principles of Knowledge Representation and Reasoning, 2018.

[Amgoud and Prade, 2009] Leila Amgoud and Henri Prade. Using arguments for making and explaining decisions. Artificial Intelligence, 173(3-4):413 436, 2009.

[Amgoud et al., 2008] Leila Amgoud, Yannis Dimopoulos, and Pavlos Moraitis. Making decisions through preference-based argumentation. KR, 8:963 970, 2008.

[Amgoud et al., 2018] Leila Amgoud, Elise Bonzon, J erˆome Delobelle, Dragan Doder, S ebastien Konieczny, and Nicolas Maudet. Gradual semantics accounting for similarity between arguments. In Sixteenth International Conference on Principles of Knowledge Representation and Reasoning, 2018.

[Atkinson et al., 2017] Katie Atkinson, Pietro Baroni, Massimiliano Giacomin, Anthony Hunter, Henry Prakken, Chris Reed, Guillermo Simari, Matthias Thimm, and Serena Villata. Towards artificial argumentation. AI magazine, 38(3):25 36, 2017.

[Baroni and Riveret, 2019] Pietro Baroni and R egis Riveret. Enhancing statement evaluation in argumentation via multi-labelling systems. J. Artif. Intell. Res., 66:793 860, 2019.

[Baroni et al., 2016] Pietro Baroni, Guido Governatori, Ho Pun Lam, and R egis Riveret. On the justification of statements in argumentation-based reasoning. In KR 16, pages 521 524. The AAAI Press, 2016.

[Baroni et al., 2018] Pietro Baroni, Dov Gabbay, Massimiliano Giacomin, and Leendert van der Torre, editors. Handbook of Formal Argumentation. College Publications, 2018.

[Baumann et al., 2023] Ringo Baumann, Anna Rapberger, and Markus Ulbricht. Equivalence in argumentation frameworks with a claim-centric view: Classical results with novel ingredients. Journal of Artificial Intelligence Research, 77:891 948, 2023. [Bernreiter et al., 2023] Michael Bernreiter, Wolfgang Dvor ak, Anna Rapberger, and Stefan Woltran. The effect of preferences in abstract argumentation under a claimcentric view. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 6253 6261, 2023. [Besnard and Hunter, 2001] Philippe Besnard and Anthony Hunter. A logic-based theory of deductive arguments. Artificial Intelligence, 128(1-2):203 235, 2001. [Besnard and Hunter, 2008] Philippe Besnard and Anthony Hunter. Elements of argumentation, volume 47. MIT press Cambridge, 2008. [Bodlaender and Koster, 2008] Hans L. Bodlaender and Arie M. C. A. Koster. Combinatorial optimization on graphs of bounded treewidth. Comput. J., 51(3):255 269, 2008. [Bodlaender, 1996] Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput., 25(6):1305 1317, 1996. [Chen, 2004] Hubie Chen. Quantified constraint satisfaction and bounded treewidth. In ECAI 04, pages 161 165. IOS Press, 2004. [Chesnevar et al., 2000] Carlos Iv an Chesnevar, Ana Gabriela Maguitman, and Ronald Prescott Loui. Logical models of argument. ACM Computing Surveys (CSUR), 32(4):337 383, 2000. [Creignou et al., 2011] Nadia Creignou, Johannes Schmidt, Michael Thomas, and Stefan Woltran. Complexity of logic-based argumentation in post s framework. Argument & Computation, 2(2-3):107 129, 2011. [Creignou et al., 2014] Nadia Creignou, Uwe Egly, and Johannes Schmidt. Complexity classifications for logicbased argumentation. ACM Trans. Comput. Log., 15(3):19:1 19:20, 2014. [Curticapean, 2019] Radu Curticapean. Counting Problems in Parameterized Complexity. In Christophe Paul and Michal Pilipczuk, editors, 13th International Symposium on Parameterized and Exact Computation (IPEC 2018), volume 115 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1 1:18, Dagstuhl, Germany, 2019. Schloss Dagstuhl Leibniz-Zentrum f ur Informatik. [Downey and Fellows, 1999] Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer Verlag, 1999. [Dung, 1995] Phan Minh Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2):321 357, 1995. [Durand et al., 2005] Arnaud Durand, Miki Hermann, and Phokion G. Kolaitis. Subtractive reductions and complete

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

problems for counting complexity classes. Theor. Comput. Sci., 340(3):496 513, 2005. [Dvor ak and Woltran, 2020] Wolfgang Dvor ak and Stefan Woltran. Complexity of abstract argumentation under a claim-centric view. Artificial Intelligence, 285:1 22, 2020. [Dvoˇr ak et al., 2023] Wolfgang Dvoˇr ak, Alexander Greßler, Anna Rapberger, and Stefan Woltran. The complexity landscape of claim-augmented argumentation frameworks. Artificial Intelligence, 317:103873, 2023. [Fazzinga et al., 2015] Bettina Fazzinga, Sergio Flesca, and Francesco Parisi. On the complexity of probabilistic abstract argumentation frameworks. ACM Trans. Comput. Log., 16(3):22:1 22:39, 2015. [Fichte et al., 2020] Johannes Klaus Fichte, Markus Hecher, and Andreas Pfandler. Lower Bounds for QBFs of Bounded Treewidth. In LICS, pages 410 424. ACM, 2020. [Fichte et al., 2021] Johannes Klaus Fichte, Markus Hecher, Yasir Mahmood, and Arne Meier. Decomposition-guided reductions for argumentation and treewidth. In IJCAI 21, pages 1880 1886. IJCAI Organization, 2021. [Fichte et al., 2023] Johannes K Fichte, Markus Hecher, Yasir Mahmood, and Arne Meier. Quantitative reasoning and structural complexity for claim-centric argumentation. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, pages 3212 3220, 2023. [Flum and Grohe, 2004] J org Flum and Martin Grohe. The parameterized complexity of counting problems. SIAM J. Comput., 33(4):892 922, 2004. [Flum and Grohe, 2006] J org Flum and Martin Grohe. Parameterized Complexity Theory. Springer Verlag, 2006. [Haak et al., 2023] Anselm Haak, Arne Meier, Om Prakash, and B. V. Raghavendra Rao. Parameterised counting in logspace. Algorithmica, 85(10):2923 2961, 2023. [Hunter and Thimm, 2017] Anthony Hunter and Matthias Thimm. Probabilistic reasoning with abstract argumentation frameworks. J. Artif. Intell. Res., 59:565 611, 2017. [Hunter, 2012] Anthony Hunter. Some foundations for probabilistic abstract argumentation. Comma, 2012:117 128, 2012. [Hunter, 2013] Anthony Hunter. A probabilistic approach to modelling uncertain logical arguments. International Journal of Approximate Reasoning, 54(1):47 81, 2013. [Impagliazzo et al., 2001] Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512 530, 2001. [Mahmood et al., 2023] Yasir Mahmood, Arne Meier, and Johannes Schmidt. Parameterized complexity of logicbased argumentation in schaefer s framework. ACM Transactions on Computational Logic, 24(3):1 25, 2023. [Mc Cartin, 2006] Catherine Mc Cartin. Parameterized counting problems. Annals of Pure and Applied Logic, 138(13):147 182, 2006.

[Parsons et al., 2003] Simon Parsons, Michael Wooldridge, and Leila Amgoud. Properties and complexity of some formal inter-agent dialogues. Journal of Logic and Computation, 13(3):347 376, 2003. [Prakken and Vreeswijk, 2002] Henry Prakken and Gerard Vreeswijk. Logics for Defeasible Argumentation, pages 219 318. Springer Verlag, 2002. [Pu et al., 2015] Fuan Pu, Jian Luo, Yulai Zhang, and Guiming Luo. Attacker and defender counting approach for abstract argumentation. In David C. Noelle, Rick Dale, Anne S. Warlaumont, Jeff Yoshimi, Teenie Matlock, Carolyn D. Jennings, and Paul P. Maglio, editors, Proceedings of the 37th Annual Meeting of the Cognitive Science Society, Cog Sci 2015, Pasadena, California, USA, July 22-25, 2015. cognitivesciencesociety.org, 2015. [Rago et al., 2018] Antonio Rago, Oana Cocarascu, and Francesca Toni. Argumentation-based recommendations: Fantastic explanations and how to find them. 2018. [Riveret et al., 2007] Regis Riveret, Antonino Rotolo, Giovanni Sartor, Roth Bram, and Henry Prakken. Success chances in argument games: a probabilistic approach to legal disputes. Available at SSRN 1100672, 2007. [Sipser, 1997] Michael Sipser. Introduction to the theory of computation. PWS Publishing Company, 1997. [Syed et al., 2019] Zafar Habeeb Syed, Michael R oder, and Axel-Cyrille Ngonga Ngomo. Unsupervised discovery of corroborative paths for fact validation. In Chiara Ghidini, Olaf Hartig, Maria Maleshkova, Vojtˇech Sv atek, Isabel Cruz, Aidan Hogan, Jie Song, Maxime Lefranc ois, and Fabien Gandon, editors, The Semantic Web ISWC 2019, pages 630 646, Cham, 2019. Springer International Publishing. [Tseitin, 1983] G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning: 2: Classical Papers on Computational Logic 1967 1970, pages 466 483. Springer Berlin Heidelberg, 1983. [Wu and Caminada, 2010] Yining Wu and Martin Caminada. A labelling based justification status of arguments. Studies in Logic, 3:12 29, 01 2010.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)