Tense Logics, Structural Proof Theory, and Effective Translations

Tim Lyon

Tim Lyon (TU Vienna) will present "Tense Logics, Structural Proof Theory, and Effective Translations" at 11 on 23 November in Old Quad G10.

Abstract: In this talk I will present recent work on effective translations between labelled and display calculi for a certain class of tense logics. I will give a brief overview of the Kripke semantics and axiomatizations of these logics and will also detail the proof-theoretic properties of the associated labelled and display calculi. I show how to transform labelled and display sequents into graphs that expose their structural features and provide a simple algorithm that transforms one type of graph into the other--thus facilitating the translation between labelled and display. By harnessing these algorithms, it can be shown that for a large class of tense logics every display proof can be transformed into a corresponding labelled proof. The reverse translation--from labelled to display--proves more difficult and can only be carried out for a smaller class of tense logics. I explain the difficulties that arise when translating labelled proofs into display proofs, show the class of logics for which this translation can be carried out, and explain some consequences of these results as well as possible future work.