KR’2021 Tutorial on Proof-Theoretic Approaches to Logical Argumentation
Ofer Arieli\(^1\) and Christian Straßer\(^2\)

Table of Contents

1- School of Computer Science, The Academic College of Tel-Aviv, Israel (

2- Institute of Philosophy II, Ruhr University Bochum, Germany (



Friday, 5 Nov 2021, 9:00–14:00 CET (8:00–13:00 UTC).
(free) registration for KR’21 is mandatory. Please register here by 15 October 2021.


Logical argumentation [7, 8] is a logic-based branch of formal argumentation theory [11, 12]. The basic entities in this context are deductive arguments, which are pairs of a finite set of formulas (\(\Gamma\), the support set) and a formula (\(\psi\), the conclusion), expressed in an arbitrary (usually propositional) language, such that the latter follows, according to some underlying logic, from the former. This gives rise to the association of arguments with Gentzen’s notion of sequents, where an argument is expressed by a sequent of the form \(\Gamma \Rightarrow \psi\). Accordingly, logical argumentation boils down to the exposition of formalized methods for reasoning with these syntactical objects, in the context of sequent-based argumentation frameworks.

Sequent-based argumentation frameworks [1] provide a generic method of drawing conclusions from a given set of sequent-based arguments, that allows for different logics, languages, and attack relations among the arguments. For this, standard Gentzen-style rules that allow to infer new arguments (sequents) from existing ones are augmented with new rules that allow to exclude some derived arguments due to the presence of other derived and opposing arguments. This gives rise to the notion of dynamic proofs (or dynamic derivations), which are intended for explicating the non-monotonic flavor of reasoning processes in an argumentation framework [2].

In this tutorial we introduce sequent-based frameworks and the dynamic derivations induced by them as a proof-theoretical approach for representing and reasoning with conflicting arguments. Particular attention is payed to the study of the basic properties and the general theory of sequent-based argumentation, its relations to other forms of non-monotonic reasoning, and various computational aspects of dynamic derivations.

The tutorial is largely based on the review paper in [4].

The Presenters

Ofer Arieli

o.jpg Ofer Arieli is a Professor of Computer Science at the School of Computer Science, the Academic College of Tel-Aviv. He received his B.Sc. in Mathematics and Computer Science from the Hebrew University in Jerusalem, and M.Sc. and Ph.D. in Computer Science from Tel-Aviv University. Afterwards (2000–2001) he was a postdoc researcher at the Department of Computer Science, the University of Leuven, Belgium.

His main research interests are related to the applications of non-classical logics in Artificial Intelligence and to reasoning with incomplete and inconsistent information. He has a number of publications on AI & KR-related journals and conferences, such as the AI Journal, IJCAI, KR, AAAI, ECAI, and co-authored of a book on the theory of paraconsistent logics (Theory of Effective Propositional Paraconsistent Logics, College Publications, 2018).

Affiliation. School of Computer Science, Tel-Aviv Academic College, Israel

Christian Straßer

c.png Christian Straßer is a Professor of Logic in Philosophy and Artificial Intelligence at the Institute for Philosophy II, Ruhr-University Bochum. He received his Master (equivalent) degrees in Philosophy and in Computer Science at University Passau and a Ph.D. in Philosophy from Ghent University (2011). In 2014 he was awarded a Sofja Kovalevskaja Award from the Alexander von Humboldt-Foundation.

Christian investigates logical aspects of defeasible reasoning. His research concerns theoretic foundations of non-monotonic logics and formal argumentation, as well as applications, including formal models of normative reasoning and agent-based models in the social epistemology. He frequently contributes to AI and KR related journals and conferences and authored a book on Adaptive Logics and Defeasible Reasoning (Springer, 2014).

Affiliation. Institute for Philosophy II, Ruhr-University Bochum, Germany


The tutorial is planned for half a day. It consists of two sessions, about two hours each, with a break of half an hour between the sessions (also, we might need a ~10-minutes mini-break in the middle of each session). So, altogether the tutorial is expected to last about 4.5 hours, including breaks.

The first session is a general survey on argumentation in AI/KR in general, sequent-based argumentation in particular, and some general properties in terms of rationality postulates. The second session covers slightly more advances topics, including dynamic proof theory and its applications, and a comparative study to related formalisms in argumentation and other forms of and non-monotonic reasoning.

The general plan of the course is therefore as follows:

First session (~120 minutes)
Introduction to argumentation (motivation, abstract & logical argumentation, Dung-style semantics) [5, 7, 8]
The base theory of sequent-based argumentation, including conceptual investigations (such as minimality and consistency of support) [1]
Rationality postulates and relations to reasoning with maximal consistency [3, 10, 14, 15]
Break (30 minutes)
Second session (~120 minutes)
Dynamic proof theory and its applications (including some illustrations) [2, 6]
Comparison to related formalisms in argumentation (e.g., ASPIC, ABA) and non-monotonic reasoning (e.g., Adaptive Logics) [9, 13]


  1. Ofer Arieli and Christian Straßer. Sequent-based logical argumentation. Argument & Computation 6(1), pages 73–99, 2015.
  2. Ofer Arieli and Christian Straßer. Logical argumentation by dynamic proof systems. Theoretical Computer Science 781, pages 63–91, 2019.
  3. Ofer Arieli, AnneMarie Borg, Christian Straßer. Reasoning with maximal consistency by argumentative approaches. Journal of Logic and Computation 28(7), pages 1523–1563, 2018.
  4. Ofer Arieli, AnneMarie Borg, Jesse Heyninck and Christian Straßer. Logic-Based Approaches to Formal Argumentation. The IfCoLog Journal of Logics and their Applications 8(6), pages 1793-1898, 2021. (Also: Chapter 12 of the Handbbok of Formal Argumentation, Vol.2, D.Gabbay, M.Giacomin, G.R..Simari, M.Thimm, editors, 2021)
  5. Pietro Baroni, Martin Caminada, & Massimiliano Giacomin. Abstract argumentation frameworks and their semantics. In: Handbook of Formal Argumentation, Vol. 1, P.Baroni, D.Gabbay, M.Giacomin, L.van der Torre, editors, pages 157–234, 2018
  6. Diderik Batens. A universal logic approach to adaptive logics. Logica Universalis, 1, 221–242, 2007
  7. Philippe Besnard, Alejandro Garcia, Anthony Hunter, Sanjay Modgil, Henry Prakken, Guillermo Simari, Francesca Toni. Special Issue of Argument & Computation on Tutorials on Structured Argumentation, Argument & Computation, 5(1), 2014
  8. Philippe Besnard and Anthony Hunter. A review of argumentation based on deductive arguments. In: Handbook of Formal Argumentation, Vol. 1, P.Baroni, D.Gabbay, M.Giacomin, L.van der Torre, editors, Chapter 9, pages 436-484, 2018.
  9. AnneMarie Borg. Assumptive sequent-based argumentation. IfCoLog Journal of Logics and their Applications 7(3), pages 227–294, 2020.
  10. Martin Caminada, & Leila Amgoud. On the evaluation of argumentation formalisms. Artificial Intelligence, 171, 286–310, 2007
  11. 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), pages 321–357, 1995.
  12. Frans H. van Eemeren, & Bart Verheij. Argumentation theory in formal and computational perspective. In: Handbook of Formal Argumentation, Vol. 1, P.Baroni, D.Gabbay, M.Giacomin, L.van der Torre, editors, Chapter 1, pages 3-74, 2018
  13. Sarit Kraus, Daniel Lehman, & Menachem Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artificial Intelligence, 44, 167–207, 1990
  14. David Makinson. Bridges between classical and nonmonotonic logic. Logic Journal of IGPL, 11(1), 69–96, 2003
  15. Nicholas Rescher and Ruth Manor. On inference from inconsistent premises. Theory and Decision, 1(2), 179–217, 1970