We’re excited to announce that Agata Ciabattoni, Timo Lang, and Revantha Ramanayake have won the Best Paper Award at TABLEAUX 2025 for their paper “Analytic Proofs for Tense Logic”!

The paper focuses on the sequent calculus for Kt, a modal logic that serves as a minimal framework for temporal reasoning. In this system, the cut rule is known to be non-eliminable. In the paper, the authors present the first algorithm that restricts the application of the cut rule to analytic cases—that is, only to subformulas of the end formulas. This yields the first constructive procedure showing that proofs in Kt can be transformed into analytic proofs, complementing earlier results that established this fact only from a semantic perspective. As with cut-elimination, the aim of this transformation is twofold: to reduce the proof search space, thereby supporting automated reasoning, and to provide new tools for meta-logical analysis of Kt and related logics.

TABLEAUX 2025, the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, was held at the end of September in Reykjavik, Iceland. It is the leading international conference for presenting research on all aspects of tableaux-based reasoning and related methods—including theoretical foundations, implementation techniques, system development, and applications.

Congratulations to Agata, Timo, and Revantha on this outstanding achievement — especially to Agata, for receiving her third Best Paper Award this year!

Abstract

The first algorithm to transform a proof in Nishimura’s sequent calculus GKt for tense logic Kt into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm analytic restriction to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas—not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.

About the authors

Agata Ciabattoni is Professor and Head of the Research Unit Theory and Logic at TU Wien Informatics. She serves as a board member of the cluster of excellence Bilateral AI, and as co-chair of the Vienna Center for Logic and Algorithms (VCLA). She is the principal investigator of the WWTF-funded projects Training and Guiding AI Agents with Ethical Rules (TAIGER) and Acquiring and explaining norms for AI systems (AXAIS), as well as the project Logical methods for Deontic Explanations (LoDEx), funded by the Austrian Science Fund FWF. She is also a recipient of the FWF START Prize 2011, the highest Austrian award for early-career researchers.

Timo Lang is a mathematician and computer scientist. His academic work focuses on the semantics and proof theory of non-classical logics. In industry, he uses formal methods to improve the reliability of software. In December 2024, he joined a new team at Huawei Ireland Research Center that aims to prove the security of cloud services using automated reasoning techniques. Prior to that, he was a postdoctoral researcher at University College London. He received his PhD in computer science from TU Wien Informatics, where he was supervised by Agata Ciabattoni and Chris Fermüller.

Revantha Ramanayake is an Associate Professor in Proof Theory of Non-Classical Logics at the University of Groningen. He was a post-doctoral researcher at the Wolfgang Pauli Institute (WPI). Prior to that, he was a post-doctoral researcher in the Research Unit Theory and Logic, headed by Agata Ciabattoni at TU Wien Informatics. Before that, he was a post-doctoral researcher at the École Polytechnique (LIX). He completed his PhD at The Australian National University, Canberra, in 2011.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.