16th Estonian Winter School in Computer Science (EWSCS)
XVI Eesti Arvutiteaduse Talvekool

Palmse, Estonia, February 27 -March 4, 2011

Rajeev Goré

School of Computer Science
(Research School of Information Sciences and Engineering)
Australian National University
Canberra, Australia

Automated reasoning in modal, tense and temporal logics


Lecture 1: Introduction to Modal and Tense Logics

We begin with a very introductory lecture on the syntax and Kripke semantics of classical normal modal logics. We consider five basic normal modal logics: K, KT, K4 and S4, and S5. We define the semantic notions of logical consequence, validity and satisfiability in these logics. We consider the natural extensions of these logics to tense logics Kt, KtT, Kt4, KtS4 and KtS5. We explain their correspondence to fragments of classical first-order logic.

Assumption: we assume some basic familiarity with classical first-order logic.

Lecture 2: Automated Reasoning for Modal/Tense Logics

We study the latest incarnation of analytic tableaux as a method for automated reasoning in modal logic. We introduce the notion of negation normal form to minimise our tableaux rules. We highlight the differences between tree-tableaux and graph-tableaux in terms of worst-case computational complexity. We study the complications introduced by converse roles and their recent solution.

Assumption: some prior knowledge of tableau for classical propositional logic would be an advantage.

Lecture 3: Introduction to Temporal Logics

We extend our introduction to cover temporal logics from computer science, specifically Linear Temporal Logic and Computational Tree Logic. We explain the notion of least and greatest fixpoints. We explain the differences in the expressive power of these logics.

Lecture 4: Automated Reasoning for Temporal Logics

We explain the basic multi-pass tableaux methods for LTL and CTL. We consider a detailed application of LTL for business process synthesis.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed March 7, 2011 14:25 EET by local organizers, ewscs11(at)cs.ioc.ee
EWSCS'11 page: //cs.ioc.ee/ewscs/2011/