A Guided Tour of Sequent Formalisms for Modal Logics
Aus International Center for Computational Logic
A Guided Tour of Sequent Formalisms for Modal Logics
Vortrag von Tim Lyon
- Veranstaltungsort: APB 3027
- Beginn: 3. Dezember 2026 um 11:00
- Ende: 3. Dezember 2026 um 12:00
- Forschungsgruppe: 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.
