Kripke's World

Kripke's World

This tutorial is one of the events of the 3rd World Congress and School on Universal Logic 2010.


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 tutorial 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 users that are not computer scientists. The tutorial 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).

(To download: "Right-click" then choose the command "Save link as..." or "Save target as...")