Ciabattoni, Agata; Lang, Timo; Ramanayake, Revantha; (2023) Cut-restriction: from cuts to analytic cuts. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE: Boston, MA, USA.

Preview

Text Lang_2304.13657-4.pdf Download (288kB) | Preview

Abstract

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, subsumes Gentzen’s cut-elimination, and establishes new analytic cut properties.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item