The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Many of the logics that are used in computer science today are variations of modal logics as they offer a good compromise between expressive power on the one hand, and good algorithmic properties on the other hand. Extensions of basic modal logic are obtained by allowing for ontological reasoning (description logics) and by adding the ability to specify ongoing, possibly infinite behaviour (fixpoint logics). Other variations of basic modal logic are designed to fit specific semantic domains such as modal logics for Markov chains, game frames or neighbourhood structures.
In my talk I am going to present coalgebraic modal logic as a general framework in which the above mentioned variations of basic modal logic can be studied in a uniform way. In particular, I am going to describe tableau calculi that yield generic decidability proofs for the coalgebraic mu-calculus and coalgebraic description logics. As corollaries we obtain previously unknown Exptime-decidability results for these logics.