At TABLEAUX 2025, the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods held in Reykjavik, Iceland, from 27-29 September 2025, VCLA co-chair Agata Ciabattoni was awarded the best paper award for the paper “Analytic Proofs for Tense Logic,” which she co-authored with Timo Lang and Revantha Ramanayake. After awards at IJCAI 2025 (best paper award) and JELIA 2025 (best student paper award), this is the third distinction for a paper co-authored by Agata Ciabattoni in only two months. 

TABLEAUX is the main international conference at which research on all aspects—theoretical foundations, implementation techniques, systems development and applications—of tableaux-based reasoning and related methods are presented.

The winning 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. We 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 ultimate 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. You can access the full paper here.

ABOUT THE AUTHORS

	Agata Ciabattoni is Professor and Head of the Research Unit Theory and Logic at TU Wien Informatics. She is co-chair of the Vienna Center for Logic and Algorithms (VCLA) and serves as a board member of the cluster of excellence Bilateral AI. She is the principal investigator of the FWF project Logical methods for Deontic Explanations (LoDEx). She is a recipient of the FWF START Prize 2011, the highest Austrian award for early-career researchers.
	Timo Lang obtained his PhD in computer science from TU Wien (supervisors Chris Fermüller and Agata Ciabattoni). He then joined the IRIS group at University College London, and now works at the Huwaei Ireland Research Center, which aims to prove the security of cloud services using automated reasoning techniques.
	Revantha Ramanayake is an Associate Professor in Proof Theory of Non-Classical Logics at the University of Groningen in the Netherlands. Before that, he was a post-doctoral researcher of A. Ciabattoni as well as a senior post-doctoral researcher within the Theory and Logic group of TU Wien.