Kripke's World: an introduction to modal logics via tableau systems

Olivier Gasquet, Andreas Herzig, Bilal Said, and François Schwarzentruber

https://www.irit.fr/~Andreas.Herzig/CTableaux

Presented at ESSLLI 2010, August 9-13, 2010 (foundational course, lecturer: Andreas Herzig)

Slides

Course Description

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 bases of classical propositional logic).

Lectures

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).

References

M. D’Agostino (editor). Handbook of Tableau Methods. Kluwer Academic Publishers, 1999.
M. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel, Dordrecht, 1983.
M. Fitting. Basic modal logic. In D. Gabbay et al., editors, Handbook of Logic in Artificial Intelligence and Logic Programming: Logical Foundations, vol. 1. Oxford University Press, 1993.
Marcos A. Castilho, Luis Fariñas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3/4):281-297, 1997.
Olivier Gasquet, Andreas Herzig, and Mohamad Sahade. Terminating modal tableaux with simple completeness proof. In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Advances in Modal Logic, volume 6, pages 167-186. King's College Publications, 2006.

https://www.irit.fr/~Andreas.Herzig