Logic
COMPLEXITY IN MODAL LOGIC
Introductory course

MAARTEN MARX and PATRICK BLACKBURN

Department of Computing, Imperial College and

Computational Linguistics, University of the Saarland

Second week
m.marx@doc.ic.ac.uk and patrick@coli.uni-sb.de
Course description

This course introduces the fundamental ideas of computational complexity and shows how they work in modal logic. The course has
three main parts.

First, we introduce the fundamental computational notions needed to understand complexity: Turing machines, algorithms, the costs of algorithms in terms of (memory) space and time, complexity classes, reductions, and so on.

Second, we show that there is a very natural combinatorial perspective from which to think about computational issues, namely the perspective provided by tiling problems and tiling games. Moreover --- as we shall show --- this perspective provides a simple and intuitive bridge to modal logic, for a tiling is simply a Kripke structure. By examining several tiling problems we shall show just how close undecidability can be in modal logic, and demonstrate the difference in computational cost between local satisfiability ("A is true at a world in a model") and global satisfiability ("A is true at every world in a model") in the minimal modal logic K. Generally speaking, tiling-based complexity analyses are an excellent way of really getting to know your logic, and we intend to get this message across loud and clear.

In the third part of the course we present the three most important classes of algorithms used in modal logic: "guessing poly-size models" (NP), the tableaux-based K-world algorithm (PSPACE), and Pratt's "deleting bad worlds" method (EXPTIME).

The course is directed at students who know virtually nothing about complexity but understand the basic (semantical) ideas underlying modal logic (that is, Kripke semantics). Our immediate pedagogical goal is to remove the fear of computational complexity that many students have, and replace it with the idea that complexity is fun. Our long-term goal is to help ensure that computational complexity becomes part of the standard repertoire of methods understood by students of logic and formal semantics.

 

Prerequisites
None
Literature
For further information please check this homepage: http://turing.wins.uva.nl/~marx/esslli98/

 

 


HOME
PROGRAMME
CONTACT
REGISTRATION