Tense Logics, Structural Proof Theory, and Effective Translations
Tim Lyon

November 23, 2018, 6:00am - 8:00am
Logic Group, The University of Melbourne

Old Quad
Parkville 3010


National Taiwan University

Topic areas


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.

Supporting material

Add supporting material (slides, programs, etc.)




Who is attending?

No one has said they will attend yet.

Will you attend this event?

Let us know so we can notify you of any change of plan.