Nonclassical Logics in Computer Science

The course offers an overview of 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.

Literature

  • Patrick Blackburn, Maarten de Rijke, Yde Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. 2002
  • Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press 1997
  • David Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, 2002.
  • Greg Restall. An Introduction to Substructural Logics, Routledge 2000
  • Nick Galatos, Peter Jipsen, Tomasz Kowalski, Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier 2007