The course overviews non-classical logics relevant for computer scientists, in particular

• Modal logics, extended to formalisms for reasoning about programs - PDL, mu-calculus. Modal systems also form the core of logics of agency and logics for reasoning about knowledge. Moreover they can be seen as a computationally well-behaved fragment of first-order logic over relational structures.

• Intuitionistic logic, which can be seen as a fragment of certain modal logics (S4) or as the logic of type theory and program extraction.

• Linear logic, which is established as the core system for resource-aware reasoning 

• The logic of bunched implications and separation logic: more recent formalisms to reason about heap verification and programs involving shared mutable data structures.

• Fuzzy and multi-valued logics for reasoning with vague information.