### 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

#### Abstract

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

- R. Goré. Automated reasoning in modal, tense and temporal logics. Slides. [pdf]
- P. Wolper. Temporal logic can be more expressive.
*Inform. and Comput.*, v. 56, n. 1-2, pp. 72-99, 1983. [doi link] - P. Abate, R. Goré, F. Widmann. One-pass tableaux for
Computation Tree Logic. In N. Dershowitz, A. Voronkov, eds.,
*Proc. of 14th Int. Conf. on Logics for Programming, Artificial Intelligence and Reasoning, LPAR 2007 (Yerevan, Oct. 2007)*, v. 4790 of*Lect. Notes in Artif. Intell.*, pp. 32-46. Springer, 2007. [doi link] - R. Goré, L. A. Nguyen. EXPTIME tableaux for ALC using sound global
caching. In D. Calvanese et al., eds.,
*Proc. of 2007 Int. Wksh. on Description Logics, DL 2007 (Brixen-Bressanone, June 2007)*, v. 250 of*CEUR Wksh. Proc.*, 8 pp. RWTH Aachen, 2007. [article at RWTH Aachen] (Long version in*J. of Autom. Reasoning*, to appear.) - R. Goré, F. Widmann. Sound global state caching for ALC with
inverse roles. In M. Giese, A. Waaler, eds.,
*Proc. of 18th Int. Conf. on Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 (Oslo, July 2009)*, v. 5607 of*Lect. Notes in Artif. Intell.*, pp. 205-219. Springer, 2009. [doi link] - R. Goré. Global caching, inverse roles and fixpoint
logics. In B. C. Grau et al., eds.,
*Proc. of 22nd Int. Wksh. on Description Logics, DL 2009 (Oxford, July 2009)*, v. 477 of*CEUR Wksh. Proc.*, 11 pp. RWTH Aachen, 2009. [article at RWTH Aachen]

Last changed **
March 7, 2011 14:25 EET**
by
local organizers, ewscs11(at)cs.ioc.ee

EWSCS'11 page:
//cs.ioc.ee/ewscs/2011/