Kripke's World

Kripke's World

This tutorial is one of the events of the The European Summer School in Logic, Language and Information - ESSLLI 2010.

Slides and course material


Possible worlds models have been introduced by Saul Kripke in the early sixties. Basically they are graphs with labelled nodes and edges. Such models provide semantics for various modal logics such as temporal logics, logics of knowledge and belief, logics of programs, logics of action, logics of obligation, as well as for description logics. They also provide semantics for other nonclassical logics such as intuitionistic logics and conditional logics. Such logics have been studied intensively in philosophical and mathematical logic and in computer science, and have been applied in various domains such as theoretical computer science, artificial intelligence, and more recently as a basis of the semantic web.

Semantic tableaux are the predominant reasoning tool for all these logics: given a formula (or a set of formulas) they allow to check whether it has a model or not. A tableau calculus uses a set of rules in order to build trees, and more generally graphs. If a tableau graph is contradiction free then it can be transformed into a model for the given formula.

The aim of the course is to provide a step-by-step introduction to modal logics, both in terms of Kripke models and in terms of semantic tableaux. The different logics will be illustrated by means of examples. We will use the generic tableaux theorem prover Lotrec (, which is a piece of software that allows to build models, check whether a given formula is true in a model, and check whether a given formula is valid in a given logic. Lotrec also allows to implement tableau systems for new logics by means of a simple interactive graph-based language accessible to readers that are not computer scientists.

The course requires basic mathematical and logic background (the basic definitions of graph theory, and the bases of classical propositional logic).


  • graphs, Kripke frames and Kripke models; model checking;
  • the basic modal logic K and its tableaux; soundness, completeness and decidability;
  • description logics;
  • the basic modal logics (KD, KT, S4, S5, …);
  • modal logics with transitive closure (PDL, logic of common knowledge).