Kees van Berkel, Andrea Sabatini and Christian Straßer have a new paper on “Making Argument Calculi Proof-Theoretically Robust: Cut-Elimination, Analyticity, and Interpolation” forthcoming in AI^3. Here’s the abstract:
Formal argumentation has proven to be a unifying framework for characterizing nonmonotonic logics in terms of arguments and counter-arguments expressing the defeasibility of such reasoning. Such arguments are often derived by employing proof-theoretic means. Sequent-style argument calculi have been shown particularly useful due to their rule-based characterization and modularity. A recent contribution in this direction are argument calculi, which have shown to characterize a large class of default and input/output logics. Despite their advantage, such calculi rely heavily on a rule called Cut. In order to fully harness the potential of such calculi and show they are mathematically robust, one needs to at least show the admissibility of Cut. Such a result opens the door to establishing various proof-theoretic results such as the subformula property, Craig interpolation, and syntax-driven proof-search for automated reasoning tasks. In this paper, we prove a stronger result, namely, that these calculi satisfy Cut-elimination, and consequently have the subformula property and interpolation.