Complexity of logic-based argumentation in Post's framework

Creignou, Nadia; Schmidt, Johannes; Thomas, Michael; Woltran, Stefan

doi:10.1080/19462166.2011.629736

Complexity of logic-based argumentation in Post's framework^†

Article type: Research Article

Authors: Creignou, Nadia^a | Schmidt, Johannes^{a; *} | Thomas, Michael^{b; ‡} | Woltran, Stefan^c

Affiliations: [a] LIF, UMR CNRS 6166, Aix-Marseille Université, 163 Avenue de Luminy, 13288, Marseille Cedex 9, France | [b] TWT GmbH, Bernhäuser Straße 40–42, 73765, Neuhausen a.d.F., Germany | [c] Institut für Informationssysteme E184/2, Technische Universität Wien, Favoritenstr. 9–11, 1040, Wien, Austria

Correspondence: [*] Corresponding author. E-mail: [email protected]

Note: [†] An earlier version appeared in the Proc. of 12th European Conference on Logics in Artificial Intelligence, JELIA’2010, Helsinki, Finland.

Note: [‡] Work performed while employed at the Institut für Theoretische Informatik, Gottfried Wilhelm Leibniz Universität, Appelstr. 4, 30167 Hannover, Germany.

Keywords: logic based argumentation, complexity, Post's lattice, counting, enumeration

DOI: 10.1080/19462166.2011.629736

Journal: Argument & Computation, vol. 2, no. 2-3, pp. 107-129, 2011

Received 19 May 2011

Accepted 23 September 2011

Published: 1 September 2011

Get PDF

Abstract

Many proposals for logic-based formalisations of argumentation consider an argument as a pair (Φ,α), where the support Φ is understood as a minimal consistent subset of a given knowledge base which has to entail the claim α. In case the arguments are given in the full language of classical propositional logic reasoning in such frameworks becomes a computationally costly task. For instance, the problem of deciding whether there exists a support for a given claim has been shown to be Σ2p-complete. In order to better understand the sources of complexity (and to identify tractable fragments), we focus on arguments given over formulæ in which the allowed connectives are taken from certain sets of Boolean functions. We provide a complexity classification for four different decision problems (existence of a support, checking the validity of an argument, relevance and dispensability) with respect to all possible sets of Boolean functions. Moreover, we make use of a general schema to enumerate all arguments to show that certain restricted fragments permit polynomial delay. Finally, we give a classification also in terms of counting complexity.

1.Introduction

Argumentation is nowadays a main research topic within the area of Artificial Intelligence (Bench-Capon and Dunne 2007; Besnard and Hunter 2008; Rahwan and Simari 2009) aiming to formally analyse the pros and cons of statements within a certain scenario in order to understand implicit conflicts and to support decision-making. The overall process of formal argumentation can be considered as a sequence of the following steps; see, for instance, the work by Caminada and Amgoud (2007) or Gorogiannis and Hunter (2011): Given a knowledge base Δ, in the first step arguments are formed, and then conflicts between the arguments are identified. Next, one abstracts from the concrete contents of the arguments and uses certain semantics to find acceptable subsets of arguments by analysing solely the graph obtained from the arguments and conflicts; this particular step was first proposed by Dung (1995) who invented the concept of abstract argumentation frameworks. Finally, by inspecting selected arguments certain conclusions can be made. Towards practicably efficient realisations, a good understanding of the computational complexity of all these single steps is thus of high importance.

We focus here on the first step of this process, i.e. forming valid and plausible arguments from a given set of formulæ. This step is also sometimes referred to as logic-based argumentation (Chesñevar, Maguitman, and Loui 2000; Prakken and Vreeswijk 2002; Besnard and Hunter 2008; Amgoud and Besnard 2010) in order to separate it from the abstraction as used in Dung's frameworks. One goal in logic-based argumentation is thus to find a concrete formal representation of an argument and then to define – on top of this concept – notions such as counterarguments, rebuttals or undercuts (see Besnard and Hunter 2001). Many proposals consider an argument as a pair (Φ,α), where the support Φ is a consistent set (or a minimal consistent set) of formulæ from a given knowledge base that entails the claim α which is a formula (Cayrol 1995; Besnard and Hunter 2001; Amgoud and Cayrol 2002; García and Simari 2004; Dung, Kowalski, and Toni 2006). Different logical formalisms provide different definitions for consistency and entailment and hence give different options for defining the notion of an argument. One natural candidate for formalising arguments is the full language of classical propositional logic. However, it is computationally challenging to generate arguments from a knowledge base Δ, using classical logic; in fact, the problem of deciding whether there exists a support Φ⊆Δ for a given claim α has been shown to be Σ2p-complete by Parsons, Wooldridge, and Amgoud (2003).

Computing the support for an argument underlies many reasoning problems in logic-based argumentation, for instance, the computation of argument trees as proposed by Besnard and Hunter (2001). Since the basic task of finding a support is already computationally involved, it is indispensable to understand its sources of complexity and to identify fragments for which that problem becomes tractable. In this paper, we contribute to this line of research by restricting the formulæ involved (i.e. formulæ in the knowledge base and thus in the support, as well as the formula used as the claim). In fact, we restrict formulæ to use only connectives from a given set B of Boolean functions and study the decision problems of existence, validity, relevance, and respectively, dispensability, which are defined as follows:

• Arg (Argumentation): given Δ, α, does there exist a support Φ⊆Δ for α?
• Arg-Check (Argument Checking): given a pair (Φ,α), is it an argument?
• Arg-Rel (Argument Relevance): given Δ, α, ϕ, is there an argument (Φ,α) such that φ∈Φ⊆Δ?
• Arg-Disp (Argument Dispensability): given Δ, α, ϕ, is there an argument (Φ,α) such that φ∉Φ⊆Δ?

We understand here as arguments pairs (Φ,α) with minimal support, i.e. (Φ,α) is an argument if Φ is consistent, entails α, and no Φ′⊊Φ entails α. Moreover, we consider the problems of enumerating and counting arguments:

• #Arg (Argument Counting): given Δ, α, how many arguments (Φ,α) with Φ⊆Δ exist?
• Enum-Arg (Argument Enumeration): given Δ, α, output all arguments (Φ,α) such that Φ⊆Δ.

It can be seen that the minimality condition is only important for the decision problems Arg-Check and Arg-Rel (for instance, in case of Arg-Disp, there exists a support Φ without ϕ for α exactly if there exists a minimal such support; we will make this more precise in Section 2.3) as well as for #Arg and Enum-Arg. For the Enum-Arg problem, we will provide a general scheme to compute all arguments making use of decision procedures for Arg-Check, Arg-Rel and Arg-Disp. This also indicates the practical relevance of the decision problems we study, since enumerating all arguments is the central task in the overall process discussed above. However, also counting the number of arguments is of importance. Consider two different formulæ α, β, it might be of interest to know whether more arguments of form (Φ,α) than arguments of form (Ψ,β) exist for a given knowledge base. Usually, such counting problems are considered without explicitly making use of enumeration procedures. Note that the latter might have to output an exponential number of solutions (thus requiring exponential time), although the number of solutions may be efficiently computable. In fact, counting complexity recently gained interest in AI as is witnessed by work from Hermann and Pichler (2010) or Durand and Hermann (2008). However, except recent work by Barnoi, Dunne, and Giacomin (2010), who consider counting complexity for abstract argumentation, we are not aware of such investigations in the area of argumentation.

A major tool when analysing the complexity of problems parameterised by a given set B of Boolean connectives is Post's lattice: a lattice showing the inclusion relations between all existing sets of Boolean functions that are closed under superposition (that is, roughly speaking, closed under arbitrary composition, see Section 2.2 for a formal definition). Several complexity classifications have already been obtained in this so-called Post's framework, such as the classical satisfiability problem (Lewis 1979), equivalence and implication problems (Reith 2003; Beyersdorff, Meier, Thomas, and Vollmer 2009a), satisfiability and model checking in modal and temporal logics (Bauland, Hemaspaandra, Schnoor, and Schnoor 2006; Bauland, Schneider, Schnoor, Schnoor, and Vollmer 2008), default logic (Beyersdorff, Meier, Thomas, and Vollmer 2009b), circumscription (Thomas 2009) and abduction (Creignou, Schmidt, and Thomas 2010).

The main contribution of this paper is a systematic complexity classification for the six aforementioned problems in terms of all possible sets of Boolean connectives.

• Concerning the four decision problems, we show that, depending on the chosen set of connectives, the problems range from inside P up to the second level of the polynomial hierarchy, and we identify those fragments complete for NP, coNP, and also for DP, the class of differences of problems in NP. We also show that unless the polynomial hierarchy collapses there exist particular sets of Boolean connectives such that: (i) deciding the existence of an argument is easier than verifying a given one; (ii) deciding the dispensability of a formula for some argument is easier than deciding its relevance.
• We provide a general schema for enumerating all arguments. For the fragments which have their decision problems in P, we also obtain positive results in terms of enumeration by showing that either each solution is computed with at most polynomial delay (for the fragments where the number of arguments might be exponential) or that all solutions can be computed in polynomial time (which obviously is only possible for fragments where the number of arguments is bounded polynomially in the size of the knowledge base and the claim). Finally, we complement our picture by considering the problem of counting the number of arguments in terms of all possible sets of Boolean connectives.

The paper is structured as follows. Section 2 contains the necessary background on complexity theory (Section 2.1) and on Post's lattice (Section 2.2). Moreover, we define the studied framework of argumentation and relevant problems in Section 2.3. We then turn to our main results which are given in Sections 3 and 4. More specifically, the complexity of the decision problems is classified in Sections 3.2–3.4, enumeration is studied in Section 4.1 and counting complexity is dealt with in Section 4.2. We summarise our results and discuss their relation to similar work (as e.g. in the area of abduction) in a dedicated Section 5. Finally, Section 6 concludes with a brief recapitulation of the achieved results as well as future research directions.

2.Background

We assume familiarity with propositional logic. The set of all propositional formulæ is denoted by ℒ. A model for a formula ϕ is a truth assignment to the set of its variables that satisfies ϕ. Further, we denote by φ[α/β] the formula obtained from ϕ by replacing all occurrences of α with β.

For a given formula ϕ, we denote by Vars(φ) the set of variables occurring in ϕ. We extend this definition on sets of formulæ Γ as Vars(Γ)=⋃φ∈ΓVars(φ). We identify finite Γ with the conjunction of all the formulæ in Γ, ⋀φ∈Γφ. Naturally, Γ[α/β] then stands for ⋀φ∈Γφ[α/β]. We say that two formulæ ϕ and ψ are equivalent (written φ≡ψ) if every assignment σ:Vars(φ)∪Vars(ψ)→{0,1} on the combined variable sets satisfies ϕ if and only if it satisfies ψ. For any formula φ∈L, we write Γ⊧φ if Γ entails ϕ, i.e. if ϕ is satisfied in every model of Γ.

A literal l is a variable x or its negation ¬ x. A positive literal is a variable x, a negative literal is the negation of a variable ¬ x. Given a set of variables V, Lits(V) denotes the set of all literals formed upon the variables in V, i.e. Lits(V):=V∪{¬x∣x∈V}. A clause is a disjunction of literals and a term is a conjunction of literals.

2.1Complexity theory

We require standard notions of the complexity theory. For the decision problems, the arising complexity degrees encompass the classes Logspace, P, NP, coNP, DP and Σ2p. The class DP is defined as the set of languages recognisable by the difference of two languages in NP, i.e. DP:={L1∖L2∣L1,L2∈NP}={L1∩L2∣L1∈NP,L2∈NP}. The class Σ2p is the set of languages recognisable by non-deterministic polynomial-time Turing machines with an NP oracle. For our hardness results, we employ logspace many-one reductions, defined as follows: a language A is logspace many-one reducible to some language B (written A⩽mlogB) if there exists a logspace-computable function f such that x∈A if and only if f(x)∈B. Thus, for 𝒞 being any of the complexity class NP, coNP, DP or Σ2p, we call 𝒞-hard a problem G if any instance of a generic problem in 𝒞 can be reduced to an instance of G by means of a logspace many-one reduction. If in addition G belongs to the class 𝒞, then it is called 𝒞-complete. A complete problem for DP is Critical-Sat, the problem to decide whether a given formula in 3CNF is unsatisfiable, but removing any of its clauses makes it satisfiable (Papadimitriou and Wolfe 1988). A prototypical Σ2p-complete problem is deciding the truth of an expression ∃X∀Yβ where β is a propositional formula over the set of variables X∪Y. This quantified formula is valid if and only if there exists a truth assignment to the variables of X such that for all truth assignments to the variables of Y the formula β is true. In this paper, we use a more restricted version, that we denote by Qsat2,∃, in which the formula β is 3-DNF, and which is still Σ2p-complete.

When analysing an enumeration algorithm, polynomial time complexity is not a suitable yardstick of efficiency since the output size is usually exponential in the size of the input. We consider an enumeration algorithm to be efficient, when it runs in polynomial delay, i.e. if the delay until the first solution is output, thereafter the delay between any two consecutive solutions, and the delay between the last solution and termination is bounded by a polynomial p(n) in the input size n. This notion of efficiency for enumeration has first been introduced by Johnson, Papadimitriou, and Yannakakis (1988). We denote the corresponding complexity class by DelayP.

A counting problem is represented using a witness function w, which for every input x returns a finite set of witnesses. This witness function gives rise to the following counting problem: given an instance x, find the cardinality |w(x)| of the witness set w(x). The class #P; is the class of counting problems naturally associated with decision problems in NP. According to Hemaspaandra and Vollmer (1995), if 𝒞 is a complexity class of decision problems, we define #·C to be the class of all counting problems whose witness function is such that the size of every witness y of x is polynomially bounded in the size of x, and checking whether y∈w(x) is in 𝒞. Thus, we have #P=#·P and #P⊆#·NP. Completeness of counting problems is usually proved by means of Turing reductions. A stronger notion is the parsimonious reduction (Papadimitriou 1994), where the exact number of solutions is conserved by the reduction function. When there is a parsimonious reduction from a counting problem #A to a counting problem #B we write #A⩽!#B.

For more background information on complexity theory, the reader is referred to Papadimitriou (1994).

2.2Post's lattice

A Boolean function is an n-ary function f:{0,1}n→{0,1}. A clone is a set of Boolean functions that is closed under superposition, i.e. it contains all projections (that is, the functions f(a1,…,an)=ak for all 1≤k≤n and n∈N) and is closed under arbitrary composition (that is, application of one function to the results of other functions). Let B be a finite set of Boolean functions. We denote by [B] the smallest clone containing B and call B a base for [B]. Post (1941) identified, the set of all clones of Boolean functions. He gave a finite base for each of the clones and showed that they form a lattice under the usual ⊆-relation, hence the name Post's lattice (Figure 1). To define the clones, we introduce the following notions, where f is an n-ary Boolean function:

• f is c-reproducing if f(c,…,c)=c, c∈{0,1}. The binary and (∧) and the binary or (∨) are 0- and 1-reproducing, the binary exclusive or (⊕) is 0-reproducing, but not 1-reproducing, whereas the unary negation (¬ ) is neither 1- nor 0-reproducing.
• f is monotonic if a1⩽b1,…,an⩽bn implies f(a1,…,an)⩽f(b1,…,bn). Boolean functions built up on composition of only ∧, ∨, 0, 1 are monotonic, like for instance g(x,y,z)≡x∧(1∧(y∨z)).
• f is c-separating of degree k if for all A⊆f−1(c) of size |A|=k there exists an i∈{1,…,n} such that (a1,…,an)∈A implies a_i=c, c∈{0,1}. The (m+1)-ary function hm(x1,…,xm+1)≡⋁i=1m+1⋀j=1,j≠im+1xj being true if and only if ‘at least m variables are true’ is 1-separating of degree m. For instance h2(x,y,z)≡(x∧y)∨(x∧z)∨(y∧z) is 1-separating of degree 2.
• f is c-separating if f is c-separating of degree | f⁻¹(c)|. The implication g(x,y)≡¬x∨y is 0-separating.
• f is self-dual if f≡dual(f), where dual(f)(x1,…,xn):=¬f(¬x1,…,¬xn). The function g(x,y,z)≡(x∧¬y)∨(x∧¬z)∨(¬y∧¬z) is self-dual.
• f is affine if f≡x1⊕⋯⊕xn⊕c with c∈{0,1}. The function g(x,y,z)≡x⊕y⊕z⊕1 is affine and self-dual.

A list of all clones with definitions and finite bases is given in Table 1. In the naming of the clones, the semantic of single indexes is as follows. Index 2 indicates that the clone contains no constants at all. Index 0 (resp. 1) indicates that the clone contains only the constant 0 (resp. 1), but not 1 (resp. 0). Clones with no index contain both constants 0 and 1. The only exceptions to this convention are the clones D and D1 which do not contain any constants at all. The index * stands for all valid indexes. Clones of particular importance in this paper, since among other things they mark points in Post's lattice where the complexity of argumentation changes, are:

• the clone of all Boolean functions BF=[∧,¬]=[∧,∨,¬,0,1]
• the monotonic clones M∗, e.g. M2=[∧,∨], M=[∧,∨,0,1]
• the affine clones L∗, e.g. L2=[x⊕y⊕z], L=[x⊕y,0,1]
• the disjunctive clones V∗, e.g. V2=[∨], V=[∨,0,1]
• the conjunctive clones E∗, e.g. E2=[∧], E=[∧,0,1]
• the c-reproducing clones R∗, R1 1-repr., R0 0-repr., R2 1- and 0-repr.
• the implication clone S0=[→]
• the negated-implication clone S1=[x∧¬y]
• the dual clones D∗, D self-dual, D1=D∩R2, D2=D∩M
• the clones S00=S0∩R2∩M=[x∨(y∧z)], S10=S1∩R2∩M=[x∧(y∨z)] and S12=S1∩R2=[x∧(y∨¬z)]

We will often add some function f∉C to a clone C and consider the clone C′=[C∪{f}] generated out of C and f. With Post's lattice, one can quite easily determine this C′: it is the lowest clone above C that contains f. The following identities will be frequently used.

• [S10∪{1}]=M1
• [D2∪{1}]=S012
• [S1∪{1}]=[D∪{1}]=BF

Figure 1.

Post's lattice showing the complexity of the decision problems studied herein.

Table 1.

The list of all Boolean clones with definitions and bases, where hn:=⋁i=1n+1⋀j=1,j≠in+1xj and dual(f)(a₁, …, a_n)=¬ f(¬ a₁ …, ¬ a_n).

Name	Definition	Base
BF	All Boolean functions	{x∧y,¬x}
R0	{f∣fis 0-reproducing}	{x∧y,x⊕y}
R1	{f∣fis 1-reproducing}	{x∨y,x⊕y⊕1}
R2	R0∩R1	{∨,x∧(y⊕z⊕1)}
M	{f∣fis monotonic}	{x∨y,x∧y,0,1}
M1	M∩R1	{x∨y,x∧y,1}
M0	M∩R0	{x∨y,x∧y,0}
M2	M∩R2	{x∨y,x∧y}
S0n	{f∣fis 0-separatingofdegreen}	{x→y,dual(hn)}
S0	{f∣fis 0-separating}	{x→y}
S1n	{f∣fis 1-separatingofdegreen}	{x∧¬y,hn}
S1	{f∣fis 1-separating}	{x∧¬y}
S02n	S0n∩R2	{x∨(y∧¬z),dual(hn)}
S02	S0∩R2	{x∨(y∧¬z)}
S01n	S0n∩M	{dual(hn),1}
S01	S0∩M	{x∨(y∧z),1}
S00n	S0n∩R2∩M	{x∨(y∧z),dual(hn)}
S00	S0∩R2∩M	{x∨(y∧z)}
S12n	S1n∩R2	{x∧(y∨¬z),hn}
S12	S1∩R2	{x∧(y∨¬z)}
S11n	S1n∩M	{hn,0}
S11	S1∩M	{x∧(y∨z),0}
S10n	S1n∩R2∩M	{x∧(y∨z),hn}
S10	S1∩R2∩M	{x∧(y∨z)}
D	{f∣fis self-dual}	{(x∧¬y)∨(x∧¬z)∨(¬y∧¬z)}
D1	D∩R2	{(x∧y)∨(x∧¬z)∨(y∧¬z)}
D2	D∩M	{(x∧y)∨(x∧z)∨(y∧z)}
L	{f∣fis affine}	{x⊕y,1}
L0	L∩R0	{x⊕y}
L1	L∩R1	{x⊕y⊕1}
L2	L∩R2	{x⊕y⊕z}
L3	L∩D	{x⊕y⊕z⊕1}
V	{f∣f is a disjunction of variables or constants</texlscub>	{x∨y,0,1}
V0	V∩R0	{x∨y,0}
V1	V∩R1	{x∨y,1}
V2	V∩R2	{x∨y}
E	{f∣f is a conjunction of variables or constants</texlscub>	{x∧y,0,1}
E0	E∩R0	{x∧y,0}
E1	E∩R1	{x∧y,1}
E2	E∩R2	{x∧y}
N	{f∣f depends on at most one variable</texlscub>	{¬x,0,1}
N2	N∩R2	{¬x}
I	{f∣fis a projection or a constant}	{id,0,1}
I0	I∩R0	{id,0}
I1	I∩R1	{id,1}
I2	I∩R2	{id}

For an example on how these identities will be useful, see Section 3.1, in particular at the end.

A propositional formula using only functions from B as connectives is called a B-formula. The set of all B-formulæ is denoted by L(B).

Let f be an n-ary Boolean function. A B-formula ϕ is called B-representation of f if f≡φ. Such a B-representation exists for every f∈[B]. Yet, it may happen that the B-representation of some function uses some input variable more than once, see Example 2.1.

Example 2.1

Example 2.1Exponential blow up

Let h(x,y)≡¬(x∧y). An {h}-representation of the binary and, and(x,y)≡x∧y, is h(h(x,y),h(x,y)). Observe that an {h}-representation of the n-ary and, andn(x1,…,xn)≡x1∧⋯∧xn, based on the recursive application of the {h}-representation h(h(x,y),h(x,y)) of the binary and to the formula

(⋯(((x1∧x2)∧x3)∧x4)∧⋯)∧xn

leads to an explosion of the formula size. This is because the parentheses-depth is linear and the variables x, y appear twice in the {h}-representation h(h(x,y),h(x,y)) of the binary and. We can avoid this exponential blow up by placing the parentheses in a way such that we get a formula of logarithmic parentheses-depth, i.e.

(⋯((x1∧x2)∧(x3∧x4))∧⋯)∧(⋯∧((xn−3∧xn−2)∧(xn−1∧xn))⋯),

2.3Logic-based argumentation

Throughout the paper, Δ is assumed to be a given finite set of formulæ (the knowledge base) representing a large depositary of information, from which arguments can be constructed for arbitrary claims.

Following Besnard and Hunter (2001), an argument is a pair (Φ,α), where Φ is a set of formulæ and α is a formula such that

(1) Φ is consistent,
(2) Φ⊧α,
(3) Φ is minimal with this last property, i.e. no proper subset of Φ entails α.

We say that (Φ,α) is an argument for α. If Φ⊆Δ, then it is said to be an argument in Δ. We call α the consequent and Φ the support of the argument. Note that these three conditions are equivalent to the following:

(C1) Φ is satisfiable,
(C2) Φ∧¬α is unsatisfiable (i.e. Φ⊧α), and
(C3) for all φ∈Φ, (Φ∖{φ})∪{¬α} is satisfiable (i.e. Φ is minimal).

Let B be a finite set of Boolean functions. Then the argument existence problem for B-formulæ is defined as

Problem: Arg(B).
Instance: A=(Δ,α), where Δ⊆L(B) and α∈L(B).
Question: Does there exist Φ such that (Φ,α) is an argument in Δ?

Besides the decision problem for the existence of an argument, we are interested in the decision problems for B-formulæ for validity, relevance and dispensability. They are defined as follows and deal with formulæ in L(B) only.

Problem: Arg-Check(B).
Instance: A=(Φ,α), where Φ⊆L(B) and α∈L(B).
Question: Is (Φ,α) an argument?

Problem: Arg-Rel(B).
Instance: A=(Δ,α,φ), where Δ⊆L(B) and α,φ∈L(B).
Question: Does there exist an argument (Φ,α) in Δ such that φ∈Φ?

Problem: Arg-Disp(B).
Instance: A=(Δ,α,φ), where Δ⊆L(B) and α,φ∈L(B).
Question: Does there exist an argument (Φ,α) in Δ such that φ∉Φ?

Observe that the minimality of the support is only relevant to the problems Arg-Check and Arg-Rel. For Arg and Arg-Disp, the existence of a consistent subset Φ of the knowledge base Δ that entails the claim α (and does not contain some formula ϕ) implies a consistent Φ′⊆Φ such that Φ′⊧α and Φ′∖{ψ}⊭α for all ψ∈Φ′. To decide the existence of an argument, it therefore suffices to find any consistent subset of Δ that entails α. For Arg-Rel, on the other hand, we have to decide whether there exists an argument for α that contains the formula ϕ. The existence of some consistent set Φ⊆Δ with φ∈Φ and Φ⊧α does not help here, because ϕ might be excluded from the minimal subset Φ′⊆Φ yielding an argument for α. Consequently, unlike in other non-monotonic reasoning formalisms, the complexity of deciding relevance and dispensability of a formula for some argument may differ. Indeed, we will show that there exist sets B such that Arg-Rel(B) is harder to decide than Arg-Disp(B) unless the polynomial hierarchy collapses. Similarly, for Arg-Check, we have to verify that the set Φ in the given pair (Φ,α) is indeed minimal with respect to consistency and entailment of α. While this is supposedly easier to decide than Arg, we will see that owing to the verification of minimality there exist sets B such that Arg-Check(B) is harder to decide than Arg(B) unless the polynomial hierarchy collapses.

Other interesting tasks are to enumerate all solutions or to count them.

Problem: Enum-Arg(B).
Instance: A=(Δ,α), where Δ⊆L(B) and α∈L(B).
Output: Generate all arguments (Φ,α) in Δ without repetition.

Problem: #Arg(B).
Instance: A=(Δ,α), where Δ⊆L(B) and α∈L(B).
Output: Number of arguments (Φ,α) in Δ.

Obviously, for both Enum-Arg(B) and #Arg(B), minimality of the support plays a crucial role, as well.

3.Decision problems

3.1Tools and methods

Observe that if B₁ and B₂ are two sets of Boolean functions such that B1⊆[B2], then every function of B₁ can be expressed by a B₂-formula, namely by its B₂-representation. This way there is a canonical reduction between Arg (B1,M) and Arg (B2,M) if B1⊆[B2]: replace all B₁-connectives by their B₂-representation. This reduction is not necessarily polynomial: Since the B₂-representation of some function may use some input variable more than once, the formula size may grow exponentially, see Example 2.1. (The existence or not of a polynomial-size B₂-representation for any B₁-formula is a topic of independent interest, which has been addressed several times in the literature, see e.g. Spira 1971; Karchmer and Wigderson 1988). Nevertheless, we will use the idea of this canonical reduction very frequently, dealing only with cases where exponential blow up can be avoided by special structures of the B₁-formulæ, similar to Example 2.1.

When we show hardness-results for Arg(B) for some B such that C⊆[B] (C a clone), we generally show hardness first only for Arg(C) and show then in a second step that the proof can indeed be extended to show hardness also for Arg(B), using the above-mentioned canonical reduction.

The following lemmas show that we can often suppose that our considered B contains the constant 1. This will reduce the number of cases to study.

Lemma 3.1

Let Arg-P denote any of the problems Arg, Arg-Check or Arg-Rel. Let B be a finite set of Boolean functions such that ∧∈[B], i.e. E2⊆[B]. Then Arg-P(B∪{1})⩽mlog Arg-P(B).

Proof

Let ℐ be the given instance. We map ℐ to the instance ℐ′ obtained by replacing each formula ψ occurring in ℐ by ψ[1/t]∧t, where t is said to be a fresh variable. ▪

In addition on this, one can also eliminate the constant 1 for the problems Arg(B) and Arg-Rel(B) when D2⊆[B].

Lemma 3.2

Let B be a finite set of Boolean functions such that D2⊆[B]. Then Arg (B∪{1})⩽mlog Arg(B) and Arg-Rel (B∪{1})⩽mlog Arg-Rel(B).

Proof

Let g(x,y,z):=(x∧y)∨(x∧z)∨(y∧z). The function g is a base of D2 and evaluates to true if and only if at least two of the variables are set to true. Given an instance (Δ,α) of Arg (B∪{1}), we define an instance (Δ′,α′) of Arg(B) by Δ′:={ψ[1/t]∣ψ∈Δ}∪{t} and α′=g(α[1/t],t,q),where t and q are fresh variables. We claim that there is an argument for α in Δ if and only if there is an argument for α′ in Δ′.

Let Φ be an argument for α in Δ. Consider Φ′:={ψ[1/t]∣ψ∈Φ}∪{t}. Observe that Φ′≡Φ. Thus Φ′ is satisfiable and Φ′⊧α, hence Φ′⊧α[1/t]∧t, as t does not occur in α. Therefore, we obtain Φ′⊧g(α[1/t],t,q). Moreover, either Φ′ or Φ′∖{t} is minimal with this property. Indeed, suppose that there exists a ψ′∈Φ′ with ψ′=ψ[1/t] for some ψ∈Φ such that Φ′∖{ψ′}⊧g(α[1/t],t,q). Then Φ′∖{ψ′}⊧α[1/t]∧t as q does not occur in Φ′, and hence Φ∖{ψ}⊧α, contradictory to the minimality of Φ.

Conversely, with similar arguments, it is easy to see that if Φ′ is an argument for α′ in Δ′, then Φ:={ψ[t/1]∣ψ∈Φ′,ψ≠t} is an argument for α in Δ: as q does not occur in Φ′, Φ′⊧α′ implies that Φ′⊧α[1/t]∧t.

This proves a correctness of the reduction from Arg (B∪{1}) to Arg(B). The analogous result for Arg-Rel follows from the same arguments as above, mapping the additional component ϕ to φ′:=φ[1/t]. ▪

Remark 1

Observe that this reduction does not work for Arg-Check: one would have to decide whether to map Φ to Φ′ or to Φ′∖{t} to ensure minimality, which requires the ability to decide whether Φ′∖{t}⊧t in Logspace. Further observe that an analogous statement of Lemma 3.1 for the constant 0 cannot be obtained in the obvious way. Replacing every formula ψ by ψ[0/f]∨f for a fresh variable f fails since such a reduction does not preserve consistency.

Let us show in an example how one can use these lemmas. Suppose, we want to show hardness results for Arg-Rel(B) in the case where S00⊆[B] or D2⊆[B] or S10⊆[B] (see Theorem 3.9). Since in the latter two cases either D2⊆[B] or E2⊆[B], according to Lemmas 3.1 and 3.2 we have Arg-Rel (B∪{1})⩽mlog Arg-Rel(B). Therefore, it is sufficient to prove hardness for Arg-Rel (B∪{1}). Observe that if D2⊆[B] then S012=[D2∪{1}]⊆[[B]∪{1}]=[B∪{1}] and if S10⊆[B] then M1=[S10∪{1}]⊆[B∪{1}]. Since S00⊆S012 and S00⊆M1, we have in both cases S00⊆[B∪{1}]. So, finally in order to prove that Arg-Rel(B) is hard in the case where S00⊆[B] or D2⊆[B] or S10⊆[B], it is sufficient to prove that the hardness holds for B such that S00⊆[B].

We will henceforth give less details when applying Lemmas 3.1 and 3.2.

3.2The complexity of verification

We commence our study of the introduced argumentation problems with the argument verification problem. This problem is in DP. Indeed, it is readily observed, as there are languages A, B with A∈NP and B∈coNP such that Arg-Check = A∩B, with

A={(Δ,Φ,α)∣Φis satisfiable,∀φ∈Φ:Φ∖{φ}⊭α};B={(Δ,Φ,α)∣Φ⊧α}.

The next two results will cover all cases where we have a matching lower bound, i.e. we provide those clones for which DP-hardness holds.

Proposition 3.3

Let S00⊆[B]. Then Arg-Check(B) is DP-complete.

Proof

To prove DP-hardness, we establish a reduction from Critical-Sat. Let ψ=⋀j=1mCj be an instance of Critical-Sat, and Vars(ψ)={x1,…,xn}. Let u,x1′,…,xn′ be fresh, pairwise distinct variables. Note that if ψ∈ Critical-Sat then each variable of ψ appears both as positive and as negative literal. Let further Cj′:=Cj[¬xi/xi′∣1⩽i⩽n] for 1≤j≤m and ψ′=⋀j=1mCj′. We map ψ to (Φ,α), where we define

Φ={Cj′|1⩽j⩽m}andα=⋁i=1nu∨(xi∧xi′).

Since x∨ y and x∨(y∧z) are functions of S00, α and all C′_j’s are S00-formulæ. These are by definition 1-reproducing. Therefore, Φ and α are satisfiable. For 1≤k≤m, let Φ_k, ψ_k, ψ_k′ denote the respective set of clauses where we deleted the kth clause. Note that always Φ≡ψ′ and Φk≡ψk′.

Suppose now that ψ ∈ Critical-Sat, i.e. ψ is unsatisfiable and ψ_k is satisfiable for all k∈{1,…,m}. We show that Φ entails α. Since ψ≡ψ′∧⋀i=1n(xi⊕xi′) is unsatisfiable, and ψ′≡Φ is monotonic, all models of Φ have to set both x_i and x′_i to 1 for at least one i∈{1,…,n}. Since α[u/0]≡⋀i=1n(xi∧xi′), we therefore have Φ⊧α[u/0]. Obviously also Φ⊧α[u/1], thus we have Φ⊧α.

It remains to prove that Φ is minimal. Since for each k∈{1,…,m} ψk≡ψk′∧⋀i=1n(xi⊕xi′) is satisfiable, no ψk′≡Φk entails α[u/0]≡⋀i=1n(xi∧xi′). A fortiori no Φ_k entails α.

Conversely suppose that (Φ,α)∈ Arg-Check. Then, in particular, Φ entails α[u/0]. Thus, we have ψ′⊧⋀i=1n(xi∧xi′), which implies that ψ is unsatisfiable. By the minimality of Φ we know that no Φ_k entails α. Since Φk⊧α[u/1], we conclude that Φk⊭α[u/0], which implies that ψk′∧⋀i=1n(¬xi∨¬xi′) is satisfiable. As ψ_k′ is monotonic, we also obtain that ψk′∧⋀i=1n(xi⊕xi′) and hence ψ_k itself is satisfiable.

We finally transform (Φ,α) into a B-instance for all B such that S00⊆[B] by replacing every connective by its B-representation. This transformation works in logarithmic space for Φ since it consists in clauses of size 3. It also does for α if we first represent it as an ∨-tree of depth logarithmic in n. ▪

Proposition 3.4

Let B be a finite set of Boolean functions such that D2⊆[B]. Then Arg-Check(B) is DP-complete.

Proof

We give a reduction from Critical-Sat similar to Proposition 3.3. For k∈N, we define g_k as the (k+1)-ary function verifying

(a) gk(z1,…,zk,0)≡⋀i=1kzi and
(b) gk(z1,…,zk,1)≡⋀i=1kzi.

Note that for every k∈N, g_k is monotonic and self-dual, and thus contained in D2. By abuse of notation, given a clause C=(l1∨l2∨l3) and a variable x, g₃(C, x) stands for g3(l1,l2,l3,x). Let ψ=⋀j=1mCj be an instance of Critical-Sat with Cj=(lj1∨lj2∨lj3) and Vars(ψ)={x1,…,xn}. Let further u,v,x1′,…,xn′ be fresh, pairwise distinct variables and Cj′:=Cj[¬xi/xi′∣1⩽i⩽n] for 1≤j≤m.

We map ψ to (Φ,α), where we define

Φ={g3(Cj′,u)∣1⩽j⩽m},andα=gn((g2(xi,xi′,v))1⩽i⩽n,u).

Obviously α and the formulæ in Φ are D2-formulæ and thus satisfiable. Let ψ′:=⋀j=1mCj′ and for 1≤k≤m, let Φ_k, ψ_k, ψ_k′ denote the respective set of formulæ (clauses) where we deleted the kth formula (clause).

Note that if ψ∈ Critical-Sat then each variable of ψ appears both as positive and as negative literal. Without loss of generality we may further assume that each literal has at least two occurrences in two different clauses. These two properties will assure that we have for all k∈{1,…,m}

Vars(ψ′)=Vars(ψk)={xi,xi′|1⩽i⩽n}.(1)Vars(Φ)=Vars(Φk)={xi,xi′|1⩽i⩽n}∪{u}.(2)

Suppose now that ψ∈ Critical-Sat, i.e. ψ is unsatisfiable and ψ_k is satisfiable for all k∈{1,…,m}. We show that Φ entails α for all possible values of u, v, where we consider in detail only the case where v=0. The case v=1 is analogous.

(i) (u,v)=(1,0): Φ[u/1]≡ψ′ and α[u/1,v/0]≡⋁i=1n(xi∧xi′). Since ψ≡ψ′∧⋀i=1n(xi⊕xi′) is unsatisfiable and ψ′ is monotonic, all models of ψ′ have to set both x_i and x_i′ to 1 for at least one i∈{1,…,n}. Therefore, Φ[u/1]⊧α[u/1,v/0].
(ii) (u, v)=(0, 0): Φ[u/0]≡⋀i=1n(xi∧xi′) and α[u/0,v/0]≡⋀i=1n(xi∧xi′). Obviously Φ[u/0]⊧α[u/0,v/0].

It remains to prove that Φ is minimal. Since ψ∈ Critical-Sat, ψk≡ψk′∧⋀i=1n(xi⊕xi′) is satisfiable and hence Φk[u/1]≡ψk′ does not entail α[u/1,v/0]≡⋁i=1n(xi∧xi′), i.e. Φk⊭α.

Conversely suppose that (Φ,α)∈ Arg-Check. Then, in particular, Φ[u/1] entails α[u/1,v/0]. Thus, we have ψ′⊧⋁i=1n(xi∧xi′), which implies that ψ is unsatisfiable. By the minimality of Φ, we obtain that no Φ_k entails α. One easily verifies that in the cases (u,v)∈{(0,0),(0,1),(1,1)} Φ_k still entails α (use Equation (2) for (u, v)=(0, 0)). Thus, we have that Φk[u/1]⊭α[u/1,v/0], which implies that ψk′∧⋀i=1n(¬xi∨¬xi′) is satisfiable. As ψ_k′ is monotonic, we obtain that ψk′∧⋀i=1n(xi⊕xi′) and hence ψ_k itself is satisfiable, too.

Finally, we transform (Φ,α) into a B-instance for all B such that D2⊆[B] in replacing all occurrences of g_k by its B-representation. This transformation works in logarithmic space, because we may assume the function g_n to be a g₂-tree of depth logarithmic in n. ▪

The full picture for Arg-Check(B) is given in the forthcoming theorem, where we also provide the results for the ‘easier’ clones.

Theorem 3.5

Let B be a finite set of Boolean functions. Then the argument validity problem for propositional B-formulæ, Arg – Check (B), is

(1) DP-complete if S00⊆[B] or S10⊆[B] or D2⊆[B],
(2) in P if L2⊆[B]⊆L,
(3) in Logspace if [B]⊆V or [B]⊆E or [B]⊆N.

Proof

For DP-completeness, according to Propositions 3.3 and 3.4, it remains only to deal with the case S10⊆[B]. Since D2⊆M1=[S10∪{1}]⊆[B∪{1}], we obtain that Arg-Check (B∪{1}) is DP-hard by Proposition 3.4. As ∧∈[B], we may apply Lemma 3.1 and obtain the DP-hardness of Arg-Check(B).

In the case L2⊆[B]⊆L, the sets Φ, Φ∪{¬α}, and (Φ∖{φ})∪{¬α} for all φ∈Φ can be easily transformed into systems of linear equations. Thus, checking the three conditions as mentioned in Section 2.3 comes down to solving a polynomial number of systems of linear equations. This can be done in polynomial time, using Gaussian elimination. For [B]⊆V, for [B]⊆E, and for [B]⊆N this check can be done in logarithmic space, as in this case the satisfiability of sets of B-formulæ can be determined in logarithmic space (Schnoor 2005). ▪

3.3The complexity of existence and dispensability

We next consider the problems Arg(B) and Arg-Disp(B). For the membership part of the forthcoming results, we can make use of the results from the previous subsection.

Theorem 3.6

Let B be a finite set of Boolean functions. Then the argument existence problem for propositional B -formulæ, Arg(B), is

(1) Σ2p -complete if D⊆[B] or S1⊆[B],
(2) coNP-complete if X⊆[B]⊆Y with X∈{S00,S10,D2} and Y∈{M,R1},
(3) in NP if [B]∈{L,L0,L3},
(4) in P if [B]∈{L1,L2}, and
(5) in Logspace if [B]⊆V or [B]⊆E or [B]⊆N.

The same classification holds for Arg-Disp(B).

Proof

The general argumentation problem has been shown to be Σ2p-complete by Parsons et al. (2003) via a reduction from Qsat2,∃. An instance of this problem is a quantified formula ∃X∀Yβ, and one may assume that the formula β is in 3DNF, i.e. β=⋁j=1ptj with exactly three literals by term. The authors map such an instance ∃X∀Yβ to (Δ,α), where Δ:={x↔0,x↔1|x∈X}, and α:=β. We use this reduction to obtain Σ2p-completeness for Arg(B) if [B]=BF. We insert parentheses in β and obtain a formula of logarithmic parentheses-depth only. We can now substitute all occurring connectives with their B-representations and obtain this way in logarithmic space an instance of Arg(B) which is equivalent to the original (Δ,α).

As ∧∈S1 and [S1∪{1}]=BF, we obtain Σ2p-completeness for the case S1⊆[B] according to Lemma 3.1. For the case D⊆[B], we obtain Σ2p-completeness by Lemma 3.2, since D2⊆D and [D∪{1}]=BF.

For X⊆[B]⊆Y with X∈{S00,S10,D2} and Y∈{M,R1}, membership in NP follows from the facts that satisfiability is in Logspace (Lewis 1979), while entailment is in coNP (Beyersdorff et al. 2009a). To prove the coNP-hardness of Arg(B), we give a reduction from the implication problem for B-formulæ, which is coNP-hard if [B] contains one of the clones S00, S10, D2. Let (ψ,α) be a pair of B-formulæ. We map this instance to ({ψ},α) if ψ is satisfiable (which is easy to decide) and to a trivial positive instance otherwise.

For [B]∈{L,L0,L3}, membership in NP follows from the fact that in this case Arg-Check is in P. Owing to the trivial satisfiability of B-formulæ for [B]∈{L1,L2}, we can improve the upper bound for Arg(B) with [B]∈{L1,L2} to membership in P.

In all other cases, Logspace-membership follows from the fact that both problems, satisfiability and entailment, are contained in Logspace (see Beyersdorff et al. 2009a) for B-formulæ.

Finally, observe that we have Arg-Disp (B)≡mlog Arg(B). To prove that Arg (B)⩽mlog Arg-Disp(B), map A=(Δ,α) to D:=(Δ∪{t},α,t). For the converse direction, map D=(Δ,α,φ) to A:=(Δ∖{φ},α). ▪

3.4The complexity of relevance

The remaining decision problem to analyse is Arg-Rel(B) which turns out to be the most difficult in terms of complexity.

Proposition 3.7

Let B be a finite set of Boolean functions such that S00⊆[B]. Then Arg-Rel(B) is Σ2p -complete.

Proof

To see that Arg-Rel(B) is contained in Σ2p, observe that, given an instance (Δ,α,φ), we can guess a set Φ⊆Δ such that φ∈Φ and verify conditions (C1)–(C3) in polynomial time using an NP-oracle.

To prove Σ2p-hardness, we provide a reduction from the problem Qsat2,∃. An instance of this problem is a quantified formula ∃X∀Yβ, where β=⋁j=1ptj with exactly three literals by term. Let X={x1,…,xn} and Y={y1,…,ym}. Let u, v, x1′,…,xn′,y1′,…,ym′ be fresh variables. We transform ∃X∀Yβ to (Δ,α,φ), where

Δ:={xi,xi′∣1⩽i⩽n}∪v∧⋀i=1m(yi∨yi′)∪{u},α:=β′∧v∧⋁i=1n(xi∧xi′)∨u,φ:=u,

and where β′=⋁j=1ptj′ and tj′:=tj[¬x1/x1′,…,¬xn/xn′,¬y1/y1′,…,¬ym/ym′] for all 1≤j≤p.

We show that ∃X∀Yβ is valid if and only if (Δ,α,φ)∈ Arg-Rel ({∧,∨}). If ∃X∀Yβ is valid, then there exists an assignment σ:X→{0,1} such that σ⊧β. Consequently, for Φ:={xi∣σ(xi)=1}∪{xi′∣σ(xi)=0}∪{u,v∧⋀i=1m(yi∨yi′)}, we obtain Φ⊧α. As Φ is consistent, it thus remains to show that u is relevant, i.e. that Φ∖{u}⊭α. This follows from the fact that Φ∖{u} is satisfied by any assignment σ′ extending σ with σ′(u):=0 and σ′(xi′):=1−σ(xi), while such a σ′ does not entail ⋁i=1n(xi∧xi′)∨u and hence σ′⊭α.

For the converse direction, let Φ be a support for α such that u∈Φ. Since Φ⊧α we conclude that v∧⋀i=1m(yi∨yi′)∈Φ and hence Φ=X∪{v∧⋀i=1m(yi∨yi′)}∪{u}, for some X⊆{xi,xi′∣1⩽i⩽n}. From Φ⊧α also follows that Φ⊧β′. From the minimality of Φ, we conclude that in particular Φ∖{u}⊭α. And therefore Φ⊭⋁i=1n(xi∧xi′). That is Φ∧⋀i=1n(¬xi∨¬xi′) is satisfiable and since Φ is monotonic, consequently also Φ∧⋀i=1n(xi⊕xi′) is satisfiable. Summed up, we know that γ:=X∧⋀i=1n(xi⊕xi′)∧⋀i=1m(yi∨yi′) is satisfiable and γ⊧β′. Hence, a fortiori, γ′:=X∧⋀i=1n(xi⊕xi′)∧⋀i=1m(yi⊕yi′) is satisfiable and γ′⊧β′. Define now σX(xi)=1 if xi∈X, σX(xi)=0 otherwise. Obviously any extension of σ_X to Y satisfies β and therefore ∃X∀Yβ is valid.

It remains to transform (Δ,α,φ) into an Arg-Rel(B)-instance for all B such that S00⊆[B]. As both ∧ and ∨ are associative, we can insert parentheses into (Δ,α,φ), such that we can represent each formula as binary {∧,∨}-tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean function in S00 defined by h(f,x,y)≡f∨(x∧y). We further transform our instance into (Δ′,α′∨f,φ′), where Δ′,α′,φ′ are obtained by replacing each occurrence of x ∧ y by h( f, x, y). One easily verifies that (Δ′,α′∨f,φ′) is in Arg-Rel ({∨,h}) if and only if (Δ,α,φ)∈ Arg-Rel ({∧,∨}). We finally replace ∨ and h by their B-representation. ▪

Proposition 3.8

Let B be a finite set of Boolean functions such that [B]⊆V or [B]⊆E or [B]⊆N. Then Arg-Rel(B) is in Logspace.

Proof

We assume the representation of V-, E-, or N-formulæ as respectively positive clauses, positive terms, or literals. Let us first consider Arg-Rel(B) for [B]⊆E. It is easy to observe that a set of positive terms Δ entails a positive term α if and only if Vars(α)⊆Vars(Δ). We claim that Algorithm 1 decides Arg-Rel(B).

Algorithm 1 can be implemented using only a logarithmic amount of space if we do not construct Δ_x entirely, but rather check the condition in line 3 directly: Δx⊧α holds if and only if Vars(α)⊆Vars(φ)∪Vars({τ∈Δ|x∉Vars(τ)}).

To prove correctness, notice that Algorithm 1 accepts only if there exists a Δx⊆Δ such that Δx⊧α and Δx∖{φ}⊭α. Thus Δ_x contains a support Φ such that φ∈Φ. Conversely, let Φ be a support such that φ∈Φ. Since Φ⊧α and Φ∖{φ}⊭α, there is at least one xi∈(Vars(φ)∩Vars(α))∖Vars(Φ). For this x_i, the algorithm constructs Δxi:={φ}∪{τ∈Δ∣xi∉Vars(τ)}. Obviously Φ⊆Δxi and therefore Δxi⊧α which causes the algorithm to accept.

Next, consider Arg-Rel(B) for [B]⊆V. Observe that a set of positive clauses C entails a positive clause α if and only if there is a clause c∈C such that Vars(c)⊆Vars(α). Thus if there is a support Φ with φ∈Φ then it is the singleton {φ}. Given (Δ,α,φ) as an instance of Arg-Rel (V), it hence suffices to check whether Vars(φ)⊆Vars(α), which can be done in Logspace.

Finally Arg-Rel(B) for [B]⊆N is in Logspace, since each B-formula can be transformed into a single literal. ▪

We obtain the following complexity classification for Arg-Rel.

Theorem 3.9

Let B be a finite set of Boolean functions. Then the argument relevance problem for propositional B -formulæ, Arg-Rel(B), is

(1) Σ2p -complete if S00⊆[B] or D2⊆[B] or S10⊆[B],
(2) in NP if L2⊆[B]⊆L,
(3) in Logspace if [B]⊆V or [B]⊆E or [B]⊆N.

Proof

Applying Lemma 3.1 and Lemma 3.2 as shown in Section 3.1, for (1) it suffices to show hardness for B such that S00⊆[B]. This has been done in Proposition 3.7. Item (2) follows from the fact that for [B]⊆L, Arg-Check(B) is in P (Proposition 3.5) and (3) has been shown in Proposition 3.8. ▪

4.Enumeration and counting problems

4.1Enumeration

A general procedure to enumerate all supports in Δ for a given claim α is given in Algorithm 2. The initial call has to be done by Enum (Δ,α,∅). The idea is to build supports recursively, picking up at each step a formula ϕ from Δ and deciding whether ϕ will be present in the currently constructed support or not. The decision procedures for Arg-Rel and Arg-Disp are used in order to avoid backtracking.

The correctness of the procedure is based on the deduction theorem, which says that {φ}∪Φ⊧α if and only if Φ⊧(φ→α). Observe that, in general, when initially called on B-formulæ, this procedure deals in its recursive calls with some formulæ which are not B-formulæ anymore (because of the formula φ→α). There is an exception to the sets B such that S0⊆[B], since in this case →∈[B] and thus φ→α can be represented as a B-formula.

Note that the only cases in which we can hope to obtain polynomial delay enumeration algorithms are those for which the decision problem Arg(B) is tractable, i.e. the cases [B]⊆V or [B]⊆N or [B]⊆E or [B]⊆L1. Indeed the presented procedure can be slightly modified in these cases, except for the case [B]⊆L1, in order to either avoid recursive calls or manage recursive calls on B-formulæ only. As a consequence and since in these cases the three decision problems Arg-Check(B), Arg-Rel(B) and Arg-Disp(B) are in P, the procedure will generate efficiently all possible arguments. This is made precise in the following proposition.

Proposition 4.1

Let B be a finite set of Boolean functions. If [B]⊆V or [B]⊆N then Enum-Arg(B) is in FP. If [B]⊆E then Enum-Arg(B) is in DelayP.

Proof

If [B]⊆V or [B]⊆N then we have seen (in the proof of Proposition 3.8) that every support for α consists of a single formula. For this reason, no recursive call in the procedure is necessary. It is enough to check whether every single formula from Δ is a support for α. Since Arg-Check(B) is in P in this case (see Theorem 3.5), we are done.

If [B]⊆E then every B-formula is a positive term. Recall that if Φ is a set of positive terms, and ϕ is a positive term, then we have Φ⊧α if and only if Vars(α)⊆Vars(Φ). As a consequence, in the case of positive terms {φ}∪Φ⊧α if and only if Φ⊧α∖φ, where α∖φ denotes the term obtained from α by removing those variables that occur in ϕ. Therefore, in the general enumeration procedure described above, we can make the recursive call on α∖φ instead of α→φ. In this way, starting from B-formulæ, all recursive calls will be made on B-formulæ as well. Since Arg-Check(B), Arg-Rel(B) and Arg-Disp(B) are all in P for any B such that [B]⊆E (see Theorems 3.9 and 3.6), it is then clear that the procedure runs with polynomial delay and uses only polynomial space. ▪

4.2Counting

The argument counting problem #Arg(B) belongs to #·NP. This follows from the facts that checking an argument is in DP⊆PNP=Δ2p (see Section 3.2) and from the equality #·Δ2p=#·NP (see Hemaspaandra and Vollmer 1995).

Proposition 4.2

Let B be a finite set of Boolean functions such that either D⊆[B] or S1⊆[B]. Then #Arg(B) is #·NP -complete.

Proof

We show #·NP-hardness by giving a parsimonious reduction from the following #·NP-hard problem: Count the number of satisfying assignments of ψ(x1,…,xn)=∀y1⋯∀ymφ(x1,…,xn,y1,…,ym), where ϕ is a DNF-formula (Durand, Hermann, and Kolaitis 2005).

Let t,r1,…rn be fresh variables. We map ψ to (Δ,α) which we define as follows:

Δ={xi,¬xi,xi⟶ri,¬xi⟶ri|1⩽i⩽n}∪{φ⟶t}α=t∧⋀i=1nri.

By minimality, every support Φ⊆Δ for α contains for every i either x_i or ¬ x_i, but not both. One easily verifies that by m↦{xi|m(xi)=1}∪{¬xi|m(xi)=0} we define a bijection between the models of ψ and the supports for α in Δ.

Since D2⊆D and E2⊆S1, we can use Lemmas 3.1 and 3.2. Observe that the reductions used in the proofs of these lemmas are parsimonious. Therefore we have #Arg (B∪{1})⩽! #Arg(B). Thus, it is sufficient to prove that hardness holds for #Arg (B∪{1}). Since BF=[D∪{1}]⊆[B∪{1}] and BF=[S1∪{1}]⊆[B∪{1}], it suffices finally to prove that hardness of #Arg(B) holds for any B such that BF=[B]. Suppose that φ=⋁i∈Iti and let Γ′ be the set of formulæ obtained from Γ by replacing φ→t≡¬(⋁i∈Iti)∨t≡(⋀i∈I¬ti)∨t by the set of clauses {¬ti∨t|i∈I}. Then Γ′ is a set of disjunctions of literals, whose size is polynomially bounded by |Γ|. Hence, by the associativity of ∨, Γ′ can be transformed in logarithmic space into an equivalent set of B-formulæ. This provides a parsimonious reduction from the above #·NP-complete problem to #Arg(B). ▪

Proposition 4.3

Let B be a finite set of Boolean functions such that X⊆[B]⊆Y with X∈{S00,S10,D2} and Y∈{M,R1}. Then #Arg (B) is in #·NP and #P;-hard.

Proof

Since the reductions in Lemmas 3.1 and 3.2 are parsimonious, analogously to Theorem 3.9, it suffices to show hardness for the case S00⊆[B].

We prove #P;-hardness by giving a parsimonious reduction from the following #P;-hard problem: count the number of models of a positive 2-CNF-formula. Let φ=⋀j=1pCj with Vars(φ)={x1,…,xn} be such a formula. Let x1′,…,xn′ be fresh variables. We map ϕ to (Δ,α) which we define as follows:

Δ={xi,xi′|1⩽i⩽n}α=φ∧⋀i=1n(xi∨xi′)

By minimality every support Φ⊆Δ for α contains for every i either x_i or x_i′, but not both. One easily verifies that by m↦{xi|m(xi)=1}∪{xi′|m(xi)=0}, we define a bijection between the models of ϕ and the supports for α in Δ.

It remains to show that α can be transformed in polynomial time into a B-formula for all B such that S00⊆[B]. As ∧ and ∨ are monotonic, we can insert parentheses such that α is represented as a binary (∧,∨)-tree of logarithmic depth. Let f be a fresh variable and let h be the Boolean functions in S00 defined by h(f,x,y)≡f∨(x∧y). We further transform α into α′ by replacing every occurrence of x∧ y by h( f, x, y). Since f does not occur in Δ it is clear that the arguments for α in Δ are the ones for α′. Since ∨,h∈S00⊆[B], we finally replace ∨ and h by their B-representation, thus concluding the proof. ▪

Proposition 4.4

Let B be a finite set of Boolean functions such that E2⊆[B]⊆E. Then #Arg(B) is #P;-complete.

Proof

Membership in #P; follows from the fact that Arg (B)∈P for every B such that [B]⊆E.

To prove #P;-hardness, we establish a parsimonious reduction from the same #P;-hard problem as in the previous proposition. So let φ=⋀j=1pCj with Vars(φ)={x1,…,xn} be a positive 2-CNF-formula. We introduce p new variables {c1,…,cp} that will represent the clauses. For every 1≤i≤n let occ(xi)={j|1⩽j⩽p,xioccursCj}. We map ϕ to (Δ,α) which we define as follows:

Δ=xi,xi∧⋀j∈occ(xi)cj|1⩽i⩽nα=⋀j=1pcj∧⋀i=1nxi

By minimality every support Φ⊆Δ for α contains for every i either x_i or xi∧⋀j∈occ(xi)cj, but not both. One easily verifies that by m↦{xi∧⋀j∈occ(xi)cj|m(xi)=1}∪{xi|m(xi)=0}, we define a bijection between the models of ϕ and the supports for α in Δ.

It remains to transform α and the formulæ in Δ into B-formulæ. We can insert parentheses in each term in order to represent it as a binary ∧-tree of logarithmic depth. Then it suffices to replace the ∧-connective by its B-representation which exists since ∧∈E2⊆[B]. ▪

Theorem 4.5

Let B be a finite set of Boolean functions. Then the argument counting problem for propositional B -formulæ, #Arg (B), is

(1) #·NP-complete if D⊆[B] or S1⊆[B],
(2) in #·NP and #P;-hard if X⊆[B]⊆Y with X∈{S00,S10,D2} and Y∈{M,R1},
(3) in #P; if L2⊆[B]⊆L,
(4) #P;-complete if E2⊆[B]⊆E, and
(5) in FP if [B]⊆V or [B]⊆N.

Proof

Items (1), (2) and (4) follow directly from the above three propositions. Item (3) follows from the fact that Arg (B)∈NP for B such that [B]⊆L (see Theorem 3.6). In the last case, all supports are singletons (see e.g. Theorem 3.8), thus there is at most a polynomial number of supports that can hence be parsed in polynomial time in order to determine the exact number of solutions. ▪

Let us conclude this section by pointing out that for the case where E2⊆[B]⊆E, i.e. when formulæ may depend on more than one variable and are representable as positive terms, the counting problem is intractable (#P;-hard, Proposition 4.4), whereas enumeration is tractable (∈DelayP, Proposition 4.1).

5.Discussion of results

Complexity classifications along the lines of Boolean clones have already been carried out for AI formalisms as circumscription (Thomas 2009) and abduction (Creignou et al. 2010). In particular, the latter work is closely related to the contents of this paper. To make this more precise, let us consider the positive abduction problem P-Abd(B). It takes as an instance a triple (Γ,H,m), where Γ⊆L(B), m∈L(B), H is a set of variables, and asks whether there exists an explanation E⊆ H such that Γ∧E is satisfiable and Γ∧E⊧m. Hence, the main differences to argumentation are as follows: (a) the knowledge base Γ is always entirely used (together with a selected subset of hypotheses) in the tests for consistency and entailment, while for argumentation these tests are performed on a chosen subset of the knowledge base Δ; (b) the parameterisation via B-formula affects only ‘fixed’ parts Γ and m in abduction (the hypotheses are by definition restricted); while in argumentation, the parameterisation is applied to the knowledge base Δ from which one has to select a subset. Nonetheless, the following relations between these two formalisms hold:

(1) if ∧∈[B], i.e. if E2⊆[B], then P-Abd(B)⩽mlog Arg(B)
(2) if →∈[B], i.e. if S0⊆[B], then Arg (B)⩽mlogP-Abd(B)

For (1), one can give the reduction (Γ,A,ψ)↦(Δ,α), where Δ:={⋀φ∈Γφ}∪A and α:=ψ∧⋀φ∈Γφ; likewise the mapping (Δ,α)↦(Γ,A,α), where A:={xφ∣φ∈Δ} and Γ:={xφ↔φ;|φ∈Δ} underlies (2).

It turns out that Arg and Arg-Disp have the same complexity classification as positive abduction. This is due to the fact that minimality of the argument plays no role in Arg and Arg-Disp. However, for Arg-Rel the situation is different but we expect similarly harder complexity for the relevance problem in abduction with respect to subset-minimal explanations (see Eiter and Gottlob 1995 for the definitions) which has not been analysed by Creignou et al. (2010). In other words, the results provided in the present paper can be used to obtain novel results for certain variants of abduction, which have not been classified yet.

Table 2 gives an overview of the results for the studied argumentation problems. The small numbers on the right side in the table cells refer to the corresponding theorem/proposition/remark.

Table 2.

The complexity of the argumentation problems.

	N∗,V∗	E_*	L1,L2	L,L0,L3	D2,S∗0⊆ [B]⊆M,R1	D,S1⊆ [B]⊆BF
Arg-Check	∈L, 3.5	∈L, 3.5	∈P, 3.5 ∈P, 3.5	DP-c, 3.3, 3.4	DP-c, 3.3, 3.4
Arg, Arg-Disp	∈L, 3.6	∈L, 3.6	∈P, 3.6	∈NP, 3.6	coNP-c, 3.6	Σ2p-c, 3.6
Arg-Rel	∈L, 3.8	∈L, 3.8	∈NP, 3.9	∈NP, 3.9	Σ2p-c, 3.7	Σ2p-c, 3.7
Enum-Arg	∈FP, 4.1	∈DelayP, 4.1	Unknown	Unknown	coNP-h, 3.6	Σ2p-h, 3.6
#Arg	∈FP, 4.5	#P;-c, 4.4	∈#P;, 4.5	∈#P;, 4.5	∈#·NP, #P;-h, 4.3	#·NP-c, 4.2

Note: The *-subscripts on clones denote all valid completions, L abbreviates Logspace, and ‘-c’ and ‘-h’ indicate, respectively, completeness and hardness.

Our results show, for instance, that when the knowledge base's formulæ are restricted to be represented as positive clauses or single literals (column V∗,N∗) then all considered decision problems as well as counting and enumeration are very easy. When allowing for positive terms (column E_*), the decision problems remain very easy, the enumeration problem becomes less trivial but still tractable (DelayP), whereas the counting problem becomes even intractable, namely #P;-complete.

Notably are the sets B of Boolean connectives where X⊆[B]⊆Y with X∈{S00,S10,D2} and Y∈{M,R1}. This case typically applies to monotonic formulæ in which no negation is involved. Such sets of B give coNP-completeness for Arg(B), while Arg-Rel(B) remains complete for Σ2p. It may come as a surprise that in these cases verifying an argument is potentially harder than deciding the existence of an argument (Arg-Check is DP-complete, Arg is only coNP-complete). This is due to the fact that when verifying an argument, the minimality condition of a support has to be checked, whereas this condition is of no importance to the argument existence problem.

The results obtained for the L-cases are partial. This corresponds to the case where individual formulæ are linear equations over the two-element field. The fact that Arg(B) with L2⊆[B]⊆L1 is in P relies on Gaussian elimination, knowing that in this case we only have to check whether Φ⊧α, that is whether the linear system Φ∧¬α is satisfiable. For the corresponding problems Arg-Rel(B), in which minimality plays a role, we only have an NP upper-bound, so far. In fact, the exact classification of the problems into tractable and intractable cases remains open for affine sets of Boolean connectives in the following cases: Arg(B) with [B]∈{L,L0,L3} and Arg-Rel(B) with L2⊆[B]⊆L.1 1

6.Conclusion and future work

To summarise, we took in this paper first steps to understanding the complexity of logic-based argumentation. We provided a classification of the complexity of four important decision tasks (Figure 1), as well as a classification of the complexity of enumeration and counting, for all possible restrictions on the set of allowed connectives.

The interpretation of our results is twofold: first, we have shown that the high complexity (i.e. Σ2p) only shows up for small parts of the lattice. In other words, only a few Boolean clones provide the inherent full complexity, while others allow for alternative, less involved, algorithms. Nonetheless, for the important problem of Arg-Rel, Σ2p covers the most interesting areas of the lattice. The bad news is that all tractable fragments are of little practical relevance. Recall that these fragments were literals, positive terms, positive clauses, and with each of the latter two restrictions we cannot even construct an inconsistent Δ. This also hints that for future work, it might be important to restrict the connectives in Δ, and respectively, α independently.

The complexity of the problems studied in this paper is also a computational core for evaluating more complex argumentation problems, for instance, the warranted formula problem (WFP) on argument trees, which has recently been shown to be PSPACE-complete by Hirsch and Gorogiannis (2011). We expect that fragments studied here also lower the complexity of WFP, but leave details for future work. Another problem which is amenable to the kind of complexity analysis we did in this paper is the identification of conflicts between two arguments (different notions for conflicts between arguments based on classical logic exist, see e.g. Gorogiannis and Hunter 2011) which is an intractable problem itself; however, since most conflicts are identified via the implication problem, we expect results similar to the one derived by Beyersdorff et al. (2009a). A complexity analysis in that direction has already been undertaken by Wooldridge, Dunne, and Parsons (2006). In that paper, the authors studied problems as, for instance, equivalence of arguments. Further future work also concerns studying the complexity of all the problems investigated here in the popular Schaefer's framework in which formulas are in generalised conjunctive normal form (see Creignou and Zanuttini (2006), Nordh and Zanuttini (2008) for complexity classifications of abduction in this framework, and Creignou and Vollmer (2008) for a survey of results obtained for various non-monotonic logics).

Notes

1 We note that the complexity of the corresponding fragments remained unclassified also for circumscription and positive abduction.

Acknowledgements

Supported by ANR ENUM 07-BLAN-0327-04, WWTF grant ICT 08-028, FWF grant P20704-N18, ÖAD grant Amadée 17/2011/EGIDE PHC Amadeus project 24908NM, and DFG grant VO 630/6-2.

References

1	Amgoud, L. and Besnard, P. A Formal Analysis of Logic-based Argumentation Systems. Proceedings of the 4th International Conference on Scalable Uncertainty Management (SUM’10, Toulouse, France). Edited by: Deshpande, A. and Hunter, A. pp. 42–55. Springer Verlag. Vol. 6379 of Lecture Notes in Computer Science
2	Amgoud, L. and Cayrol, C. (2002) . A Reasoning Model Based on the Production of Acceptable Arguments. Annals of Mathematics and Artificial Intelligence, 34: : 197–215.
3	Baroni, P., Dunne, P. and Giacomin, M. On Extension Counting Problems in Argumentation Frameworks. Proceedings of the 3rd International Conference on Computational Models of Argument (COMMA 2010, Desenzano del Garda, Italy). Edited by: Baroni, P., Cerutti, F., Giacomin, M. and Simari, G. pp. 63–74. IOS Press. Vol. 216 of Frontiers in Artificial Intelligence and Applications
4	Bauland, M., Hemaspaandra, E., Schnoor, H. and Schnoor, I. Generalized Modal Satisfiability. Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science (STACS 2006, Marseille, France). Edited by: Durand, B. and Thomas, W. pp. 500–511. Springer Verlag. Vol. 3884 of Lecture Notes in Computer Science
5	Bauland, M., Schneider, T., Schnoor, H., Schnoor, I. and Vollmer, H. (2008) . The Complexity of Generalized Satisfiability for Linear Temporal Logic. Logical Methods in Computer Science, : 5
6	Bench-Capon, T. and Dunne, P. (2007) . Argumentation in Artificial Intelligence. Artificial Intelligence, 171: : 619–641.
7	Besnard, P. and Hunter, A. (2001) . A Logic-based Theory of Deductive Arguments. Artificial Intelligence, 128: : 203–235.
8	Besnard, P. and Hunter, A. (2008) . Elements of Argumentation, MIT Press.
9	Beyersdorff, O., Meier, A., Thomas, M. and Vollmer, H. (2009) a. The Complexity of Propositional Implication. Information Processing Letters, 109: : 1071–1077.
10	Beyersdorff, O., Meier, A., Thomas, M. and Vollmer, H. The Complexity of Reasoning for Fragments of Default Logic. Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009, Swansea, UK). Edited by: Kullmann, O. pp. 51–64. Springer Verlag. Vol. 5584 of Lecture Notes in Computer Science
11	Caminada, M. and Amgoud, L. (2007) . On the Evaluation of Argumentation Formalisms. Artificial Intelligence, 171: : 286–310.
12	Cayrol, C. On the Relation between Argumentation and Non-monotonic Coherence-based Entailment. Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 1995, Montréal, Canada). pp. 1443–1448. Morgan Kaufmann.
13	Chesñevar, C., Maguitman, A. and Loui, R. (2000) . Logical Models of Argument. ACM Compututing Surveys, 32: : 337–383.
14	Creignou, N., Schmidt, J. and Thomas, M. Complexity of Propositional Abduction for Restricted Sets of Boolean Functions. Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning (KR 2010, Toronto, Canada). Edited by: Lin, F., Sattler, U. and Truszczynski, M. pp. 8–16. AAAI Press. (full review to appear in Journal of Logic and Computation 2011)
15	Creignou, N. and Vollmer, H. Boolean Constraint Satisfaction Problems: When Does Post's Lattice Help?. Complexity of Constraints – An Overview of Current Research Themes. Edited by: Creignou, N., Kolaitis, P. G. and Vollmer, H. pp. 3–37. Springer. Vol. 5250 of Lecture Notes in Computer Science
16	Creignou, N. and Zanuttini, B. (2006) . A Complete Classification of the Complexity of Propositional Abduction. SIAM Journal on Computing, 36: : 207–229.
17	Dung, P., Kowalski, R. and Toni, F. (2006) . Dialectical Proof Procedures for Assumption-based Admissible Argumentation. Artificial Intelligence, 170: : 114–159.
18	Dung, P. M. (1995) . On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artificial Intelligence, 77: : 321–358.
19	Durand, A., Hermann, M. and Kolaitis, P. G. (2005) . Subtractive Deductions and Complete Problems for Counting Complexity Classes. Theoretical Computer Science, 340: : 496–513.
20	Durand, A. and Hermann, M. (2008) . On the Counting Complexity of Propositional Circumscription. Information Processing Letters, 106: : 164–170.
21	Eiter, T. and Gottlob, G. (1995) . The Complexity of Logic-based Abduction. Journal of the ACM, 42: : 3–42.
22	García, A. and Simari, G. (2004) . Defeasible Logic Programming: An Argumentative Approach. Theory and Practice of Logic Programming, 4: : 95–138.
23	Gorogiannis, N. and Hunter, A. (2011) . Instantiating Abstract Argumentation with Classical Logic Arguments: Postulates and Properties. Artificial Intelligence, 175: : 1479–1497.
24	Hemaspaandra, L. and Vollmer, H. (1995) . The Satanic Notations: Counting Classes Beyond #P and Other Definitional Adventures. Complexity Theory Column 8, ACM-SIGACT News, 26: : 2–13.
25	Hermann, M. and Pichler, R. (2010) . Counting Complexity of Propositional Abduction. Journal of Computer and System Sciences, 76: : 634–649.
26	Hirsch, R. and Gorogiannis, N. (2010) . The Complexity of the Warranted Formula Problem in Propositional Argumentation. Journal of Logic and Computation, 20: : 481–499.
27	Johnson, D., Papadimitriou, C. and Yannakakis, M. (1988) . On Generating All Maximal Independent Sets. Information Processing Letters, 27: : 119–123.
28	Karchmer, M. and Wigderson, A. Monotone Circuits for Connectivity Require Super-logarithmic Depth. Proceedings of the 20th Annual ACM Symposium on Theory of Computing (STOC 1988, Chicago, Illinois, USA). Edited by: Simon, J. pp. 539–550. ACM.
29	Lewis, H. (1979) . Satisfiability Problems for Propositional Calculi. Mathematical Systems Theory, 13: : 45–53.
30	Nordh, G. and Zanuttini, B. (2008) . What Makes Propositional Abduction Tractable. Artificial Intelligence, 172: : 1245–1284.
31	Papadimitriou, C. (1994) . Computational Complexity, Addison-Wesley.
32	Papadimitriou, C. and Wolfe, D. (1988) . The Complexity of Facets Resolved. Journal of Computer and System Sciences, 37: : 2–13.
33	Parsons, S., Wooldridge, M. and Amgoud, L. (2003) . Properties and Complexity of Some Formal Inter-agent Dialogues. Journal of Logic and Computation, 13: : 347–376.
34	Post, E. (1941) . The Two-valued Iterative Systems of Mathematical Logic. Annals of Mathematics Studies, 5: : 1–122.
35	Prakken, H. and Vreeswijk, G. (2002) . “Logical Systems for Defeasible Argumentation”. In Handbook of Philosophical Logic, Edited by: Gabbay, D. Kluwer.
36	Rahwan, I. and Simari, G. (2009) . Argumentation in Artificial Intelligence, Edited by: Rahwan, I. and Simari, G. Springer Verlag.
37	Reith, S. On the Complexity of some Equivalence Problems for Propositional Calculi. Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science (MFCS 2003, Bratislava, Slovakia). Edited by: Rovan, B. and Vojtás, P. pp. 632–641. Springer Verlag. Vol. 2747 of Lecture Notes in Computer Science
38	Schnoor, H. (2005) . The Complexity of the Boolean Formula Value Problem, University of Hannover. Technical Report, Theoretical Computer Science
39	Spira, P.M. (1971), ‘On Time-hardware Complexity Tradeoffs for Boolean Functions’, Proceedings of the 4th Hawaii International Symposium on System Sciences, pp. 525–527
40	Thomas, M. The Complexity of Circumscriptive Inference in Post's Lattice. Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009, Potsdam, Germany). Edited by: Erdem, E., Lin, F. and Schaub, T. pp. 290–302. Springer Verlag. Vol. 5753 of Lecture Notes in Computer Science
41	Wooldridge, M., Dunne, P. and Parsons, S. On the Complexity of Linking Deductive and Abstract Argument Systems. Proceedings of the 21st National Conference on Artificial Intelligence (AAAI 2006, Boston, Massachusetts, USA). pp. 299–304. MIT Press.

Abstract

1.Introduction

2.Background

2.1Complexity theory

2.2Post's lattice

Figure 1.

Table 1.

Example 2.1

Example 2.1Exponential blow up

2.3Logic-based argumentation

3.Decision problems

3.1Tools and methods

Lemma 3.1

Proof

Lemma 3.2

Proof

Remark 1

3.2The complexity of verification

Proposition 3.3

Proof

Proposition 3.4

Proof

Theorem 3.5

Proof

3.3The complexity of existence and dispensability

Theorem 3.6

Proof

3.4The complexity of relevance

Proposition 3.7

Proof

Proposition 3.8

Proof

Theorem 3.9

Proof

4.Enumeration and counting problems

4.1Enumeration

Proposition 4.1

Proof

4.2Counting

Proposition 4.2

Proof

Proposition 4.3

Proof

Proposition 4.4

Proof

Theorem 4.5

Proof

5.Discussion of results

Table 2.

6.Conclusion and future work

Notes

Acknowledgements

References

Share this:

North America

Europe

Asia