Dialectical Classical Argumentation (Dialectical Cl-Arg) has been shown to satisfy rationality postulates under resource bounds.In particular, the consistency and non-contamination postulates are satisfied despite dropping the assumption of logical omniscience and the consistency and subset minimality checks on arguments' premises that are deployed by standard approaches to Cl-Arg.This paper studies Dialectical Cl-Arg's formalisation of Preferred Subtheories (PS) nonmonotonic reasoning under resource bounds.The contribution of this paper is twofold.First, we establish soundness and completeness for Dialectical Cl-Arg's credulous consequence relation under the preferred semantics and credulous PS consequences.This result paves the way for the use of argument game proof theories and dialogues that establish membership of arguments in admissible (and so preferred) extensions, and hence the credulous PS consequences of a belief base.Second, we refine the non-standard characteristic function for Dialectical Cl-Arg, and use this refined function to show soundness for Dialectical Cl-Arg consequences under the grounded semantics and resource-bounded sceptical PS consequence.We provide a counterexample that shows that completeness does not hold.However, we also show that the grounded consequences defined by Dialectical Cl-Arg strictly subsume the grounded consequences defined by standard Cl-Arg formalisations of PS, so that we recover sceptical PS consequences that one would intuitively expect to hold.

Dialectical Classical Logic Argumentation (D-Cl-Arg) formalises maxi-consistent non-monotonic reasoning under the practical assumption that agents have bounded resources for classical inference, and that agents do not typically check arguments’ premises for subset minimality and consistency. However, D-Cl-Arg still satisfies all rationality postulates. Moreover D-Cl-Arg accommodates uses of argument characteristic of dialectical practice. This paper extends D-Cl-Arg to accommodate further dialectical uses of argument; in particular unrestricted rebuts on the deductively derived conclusions of arguments, and Occam Razor defeats that dialectically demonstrate that an argument makes use of redundant premises. We show that all rationality postulates are still satisfied, while relaxing constraints on preference relations that were previously required to prove rationality.

Abstract FDE, LP and $\mathbf {K_{3}}$ are closely related to each other and admit of an intuitive informational interpretation. However, all these logics are co-NP complete, and so idealized models of how an agent can think. We address this issue by shifting to signed formulae, where the signs express imprecise values associated with two bipartitions of the corresponding set of standard values. We present proof systems whose operational rules are all linear and have only two structural branching rules that express a generalized Principle of Bivalence. Each of these systems leads to defining an infinite hierarchy of tractable approximations to the respective logic, in terms of the maximum number of allowed nested applications of the two branching rules. Further, each resulting hierarchy admits of an intuitive 5-valued non-deterministic semantics.

ASPIC+ is an established general framework for argumentation and non-monotonic reasoning. However, ASPIC+ does not satisfy the non-contamination rationality postulates, and moreover, tacitly assumes unbounded resources when demonstrating satisfaction of the consistency postulates. In this paper we present a new version of ASPIC+ – Dialectial ASPIC+ – that is fully rational under resource bounds.

The argumentation turn in logic paves the way for importing problems and ideas from general philosophy of science into logical formalisms. The main problems are: when faced with an inconsistency, how do we choose the hypotheses/beliefs that are the most plausible candidates for revision? Do we really need to react to each single inconsistency or should we focus on predictive success and temporarily ignore “minor” inconsistencies? How do we distinguish ad hoc adjustments from heuristically fruitful revisions? These questions call for a sophisticated notion of “epistemic entrenchment”. The basic idea has played an important role both in the area of belief revision (Gärdenfors and Makinson) and, under different denominations, in that of general philosophy of science (Quine, Kuhn, Lakatos), with little or no interaction between them. The main aim of this talk is to bring the philosophical debate on this notion to the attention of the formal argumentation community and suggest how this interaction could lead to substantial advances in the field.

Classical logic argumentation (Cl-Arg) under the stable semantics yields argumentative characterisations of non-monotonic inference in Preferred Subtheories. This paper studies these characterisations under both the standard approach to Cl-Arg, and a recent dialectical approach that is provably rational under resource bounds. Two key contributions are made. Firstly, the preferred extensions are shown to coincide with the stable extensions. This means that algorithms and proof theories for the admissible semantics can now be used to decide credulous inference in Preferred Subtheories. Secondly, we show that as compared with the standard approach, the grounded semantics applied to the dialectical approach more closely approximates sceptical inference in Preferred Subtheories.

Classical logic based argumentation (ClAr) characterises single agent non-monotonic reasoning and enables distributed non-monotonic reasoning amongst agents in dialogues. However, features of ClAr that have been shown sufficient to ensure satisfaction of rationality postulates, preclude their use by resource bounded agents reasoning individually, or dialectically in real-world dialogue. This paper provides a new formalisation of ClAr that is both suitable for such uses and satisfies the rationality postulates. We illustrate by providing a rational dialectical characterisation of Brewka's non-monotonic Preferred Subtheories defined under the assumption of restricted inferential capabilities.

While the existence of a fundamental relationship between logic and information seems unquestionable, its precise nature has so far proved to be rather elusive and somewhat puzzling. The received view on this issue is epitomized by the traditional tenet that logical inference is ‘tautological’ (literally, repetitive and trivially true), namely that a valid inference is one in which the information carried by the conclusion is (in a sense variously specified) contained in the information carried by the (conjunction of the) premises. At the mid of the 20th century, Bar-Hillel and Carnap's controversial theory of ‘semantic information’ provided what is, to date, the strongest theoretical justification for this tenet. However, as remarked by a number of authors who have made the history of logic, including Frege, Dummett and Hintikka, the received view clashes with the intuitive idea that deductive arguments are useful just because, by their means, we obtain information that we did not possess before. Moreover, it also clashes with two 20th-century milestones of the theory of computation: the undecidability of first-order logic and the NP-hardness of propositional logic. How can logic be informationally trivial and, yet, computationally hard? Can we obtain an informational characterization of logical consequence that is more in tune with our intuition and with the negative results on the computational complexity of logical reasoning?

The method of analytic tableaux is a direct descendant of Gentzen's cut-free sequent calculus and is regarded as a paradigm of the notion of analytic deduction in classical logic. However, cut-free systems are anomalous from the proof-theoretical, the semantical and the computational point of view. Firstly, they cannot represent the use of auxiliary lemmas in proofs. Secondly, they cannot express the bivalence of classical logic. Thirdly, they are extremely inefficient, as is emphasized by the ‘computational scandal’ that such systems cannot potynomially simulate the truth-tables. None of these anomalies occurs if the cut rule is allowed. This raises the problem of formulating a proof system which incorporates a cut rule and yet can provide a suitable model of classical analytic deduction. For this purpose we present an alternative refutation system for classical logic, that we call KE. This system, though being ‘close’ to Smullyan's tableau method, is not cut-free but includes a classical cut rule which is not eliminable. Analytic deductions are then obtained by restricting the cut rule to analytic applications, namely applications that do not violate the subformula principle. It turns out that this analytic restriction of the KE system shares all the interesting properties of Smullyan's tableau method and of cut-free systems—it obeys the subformula principle and admits systematic refutation procedures—but uniformly and essentially improves on them from the complexity viewpoint. In particular, we show that the analytic KE system linearly simulates the tableau method, but the tableau method cannot p-simulate the analytic KE system. Finally, we show that every proof system that can simulate the cut rule in a constant number of steps is strictly more powerful than cut-free systems, from the complexity viewpoint, even in the domain of analytic deduction. Hence, the speed-up of the analytic KE system does not depend on the form of the operational rules but only on the analytic cut rule.