COURSE
Kripke's World
Andreas Herzig
https://www.irit.fr/~Andreas.Herzig/CTableaux//ULogic10.html
and
http://www.uni-log.org/t3-kripkeworld.html
organized as part of
World Congress and School on Universal Logic III
April 18 - 21, 2010
Course material (updated since, see Lotrec page)
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 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).
Contents:
- 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. 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.
-
M. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel, Dordrecht, 1983.
-
M. D'Agostino (editor). Handbook of Tableau Methods. Kluwer Academic Publishers, 1999.
-
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