GroLog Seminar

SPEAKER: Revantha Ramanayake (University of Groningen)

DATE: Friday 28 November 2025

TIME: 16:00-17:00

PLACE: Bernoulliborg, room 5161.0267

TITLE: Analytic Restriction for Tense Logic

ABSTRACT: The foundational result in proof theory is cut-elimination, introduced by Gentzen in the 1930s. This is the algorithm that eliminates instances of the cut-rule from a formal proof.  For many non-classical logics, cut-elimination fails in the proof formalism of the sequent calculus. Since the 1960s, the response was to introduce more expressive (and complicated) formalisms to regain cut-elimination. A recent alternative [1,2] aims to retain the advantages of the sequent calculus, by transforming---when elimination is not possible---the cut-formulas into simpler ones. As with cut-elimination, the final goal is to limit the proof search space to support proof-theoretic and meta-logical investigation. In this talk, I present an algorithm [3] transforming a sequent calculus proof into an analytic one. In an analytic proof, every rule instance is analytic i.e., every formula in every premise is a subformula of some formula in its conclusion. It is called {analytic restriction} to convey that it is not only the instances of the cut-rule that are made analytic, but also rule instances that introduce modalities. The algorithm is technically interesting and intended as a stepping stone along the path to a general (cut-)restriction algorithm. 

Joint work with Agata Ciabattoni (TU Wien) and Timo Lang (UCL).

[1] A. Ciabattoni, T. Lang, RR: Bounded-analytic Sequent Calculi and Embeddings for Hypersequent Logics. J. Symb. Log. 86(2): 635-668 (2021)

[2] A. Ciabattoni, T. Lang, RR: Cut-Restriction: From Cuts to Analytic Cuts. LICS 2023: 1-13

[3] A. Ciabattoni, T. Lang, RR: Analytic Proofs for Tense Logic. TABLEAUX 2025: 220-237