A Guided Tour of Sequent Formalisms for Modal Logics
From International Center for Computational Logic
A Guided Tour of Sequent Formalisms for Modal Logics
Talk by Tim Lyon
- Location: APB 3027
- Start: 3. December 2026 at 11:00 am
- End: 3. December 2026 at 12:00 pm
- Research group: Computational Logic
- Event series: Research Seminar Logic and AI
- iCal
This tutorial explores the landscape of sequent-based proof formalisms for modal logics, using Gödel-Löb provability logic (GL) as a running example. We survey four major paradigms--labeled sequents, nested (or tree) sequents, linear nested sequents, and Gentzen sequents--and discuss the various trade-offs of choosing one formalism over another, including sequent size, proof size, and suitability for counter-model extraction. The central theme of the tutorial is understanding how these formalisms relate by means of proof transformations, explaining how one can systematically "transition" between them: from graphs, to trees, to lines, and to points (i.e., standard Gentzen sequents). Along the way, we highlight what is lost or gained in each transition, such as invertibility of rules or proof compactness. We also touch on how the choice of formalism affects proof-search algorithms.
