Generic methods in the construction of cut free sequent systems
Bjoern Lellmann (Imperial College London)
LOGIC AND COMPUTATION SEMINARDATE: 2013-02-04
TIME: 14:00:00 - 15:00:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
The emergence of ever new modal logics, particularly in Computer Science, encourages the development of generic methods for investigating properties of these logics such as decidability or complexity. On the other hand, for specific logics these questions are often attacked proof-theoretically using cut free sequent or tableaux systems. This suggests the development of generic methods and tools for the construction and investigation of such sequent systems.
The basis for this talk is a general format for sequent rules for not necessarily normal propositional modal logics based on classical or intuitionistic logic. The format covers most standard modal logics including K and S4 together with their constructive counterparts as well as non-normal logics such conditional logics. I will present some generic results concerning cut elimination and complexity of such systems and the connections between the rules and axioms in a Hilbert-style system.
Based on joint work with Dirk Pattinson
BIO:
After graduating from the University of Freiburg I am now a PhD student at Imperial College London.
