The Method of Refinement: Deriving Proof-Calculi from Semantics for Multi-Modal Logics

Talk by Tim Lyon

Location: Digital
Start: 11. June 2020 at 1:00 pm
End: 11. June 2020 at 2:30 pm
Event series: KBS Seminar
iCal

In this talk, we look at how to derive nested calculi from labelled calculi for multi-modal logics, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. Since labelled calculi are constructed by transforming the semantics of a logic into a proof system, the method of refinement shows how one can derive simplified calculi from the semantics of a logic. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. As a consequence of the extraction process, each nested calculus inherits fundamental proof-theoretic properties from its associated labelled calculus and is suitable for applications such as decidability and interpolation.

Tim is currently working at the informatics faculty of the TU Wien in Vienna as a PreDoc Researcher in the research unit "Theory and Logic".

This talk will be held digitally. If there is any interest in attending, please write an e-mail to thomas.feller@tu-dresden.de.