Modal Logic

Dr. Jakob Piribauer
SWS: (2/2/0), in English

Description

Modalities are expressions that quantify the truth of a statement, e.g., 'possibly' and 'necessarily'. Modal logics are simple, yet expressive, formalisms that incorporate such modalities. The incorporated modalities offer a  wide variety of possible readings such as temporal readings ('at some point in the future …'), epistemic readings ('the agent knows that …'), or readings talking about the dynamics of programs ('there is an execution of program P after which …'). Therefore, modal logics are applicable to various application domains and play an important role in computer science, philosophy, mathematics, and linguistics among others.

This course provides an introduction to the main concepts of modal logic with a focus on its role in computer science. It covers:

• syntax and semantics of modal logics,
• Kripke structures and Kripke frames,
• bisimulations,
• translations to first-order logic,
• frame definability,
• soundness and completeness results,
• complexity and decidability results,
• propositional dynamic logic.

Literature

The course follows the book "Modal logic (Fourth printing with corrections)", Patrick Blackburn, Maarten de Rijke, Yde Venema; Cambridge University Press, 2010.

This book is available online via the SLUB.

Registration

Enrolling via OPAL is required until October 16th 2023.

Dates

Lectures will take place on Tuesdays, while exercise classes will take place on Wednesdays. Occasionally, there might be deviations from this assignment to the time slots, which will be announced in advance.

Prerequisites

For the course, basic knowledge on first-order logic and complexity theory as well as elementary mathematical knowledge and skills are presumed.

Exam and Creditability

Bachelor Informatik

• INF-B-510: Vertiefung in der Informatik (25 minute oral exam)

• INF-B-520: Spezialisierung in der Informatik (25 minute oral exam)

Master Informatik

• INF-BAS6: Theoretische Informatik (exam according to module description)

• INF-VERT6: Vertiefung Theoretische Informatik (exam according to module description)

Diplom Informatik

• INF-BAS6: Theoretische Informatik (exam according to module description)

• INF-VERT6: Vertiefung Theoretische Informatik (exam according to module description)

Master Computational Logic

• MCL-TCSL: Theoretical Computer Science and Logic (exam according to module description)

Master Computational Modeling and Simulation

• CMS-LM-BAS: Foundations of Logical Modeling (25 minute oral exam)

Contact