LIRa Session: Bahareh Afshari

Speaker: Bahareh Afshari (ILLC)

Date and Time: Thursday, March 14th 2019, 16:30-18:00

Venue: ILLC Seminar Room F1.15, Science Park 107.

Title: An infinitary treatment of fixed point modal logic.

Abstract. Fixed point modal logic deals with the concepts of induction and recursion in a most fundamental way. The term refers to any logic built on the foundation of modal logic that features inductively and/or co-inductively defined operators. Examples range from simple temporal logics (e.g. Tense Logic and Linear Time Logic) to the highly expressive Modal Mu-Calculus and its extensions.

In this talk I will introduce the modal mu-calculus and present a complete proof system for it based on nested sequents. We will see how the proof system can be used to obtain a proof of the finite model property and, time permitting, I will also explain how the framework lends itself to a sound and complete axiomatisation for the extension of mu-calculus with backward modalities.

(Joint work with Gerhard Jäger and Graham Leigh)