IJCAR 2001 Tutorial

Clausal Temporal Resolution

Tuesday 19th June 9:00-12:30


Temporal logic is a variety of non-classical logic that was originally developed in order to represent tense in natural language. Recently, it has achieved a significant role in the formal specification and verification of concurrent and distributed systems, providing a simple mechanism for concisely specifying a number of useful concepts, such as safety, liveness and fairness of computational entities. The increasing importance of temporal verification, in a variety of critical situations, has led to development of a range of proof methods for temporal logics. In this tutorial, we introduce, analyse and develop a clausal approach to resolution in temporal logics.


This tutorial will provide an introduction to a key development within temporal proof. As such it will be primarily of value to those working in Computer Science or Artificial Intelligence, who wish to gain an understanding of this approach to temporal proof, but will also be of interest to philosophers and linguists with an interest in how the concept of temporal reasoning is treated in Artificial Intelligence and Computer Science. The tutorial will be supported by explanatory notes.


The tutorial begins by introducing the basic concepts of temporal logics, particularly propositional discrete linear temporal logics. We show how arbitrary specifications in such a logic can be transformed into a simple and intuitive normal form, and then describe the novel resolution rules that can be applied to formulae in this form. We then progressively introduce more complex extensions of the basic approach, tackling clausal resolution within more complex temporal logics, and refinements of clausal temporal resolution itself. The tutorial incorporates a variety of examples, exhibiting the workings of the clausal temporal resolution approach.

Target Audience

We expect attendees to be researchers interested in the foundational aspects of temporal reasoning and temporal verification. The tutorial assumes general knowledge of proof methods (such as tableaux and resolution) and a basic understanding of classical logic (syntax, semantics, proof theory).


  Clare Dixon
  Department of Computer Science, 
  The University of Liverpool
  Liverpool, L69 7ZF
  United Kingdom
  email C.Dixon@csc.liv.ac.uk
  tel   (+44 1 51) 794 3674 
  fax   (+44 1 51) 794 3715
  Michael Fisher
  Department of Computer Science, 
  The University of Liverpool
  Liverpool, L69 7ZF
  United Kingdom
  email M.Fisher@csc.liv.ac.uk
  tel   (+44 1 51) 794 6701 
  fax   (+44 1 51) 794 3715


9:00 - 9:45 Introduction to temporal logics/Separated Normal Form (SNF)

9:45-10:30 Temporal Resolution Method

10:30-11:00 Coffee Break

11:00-11:45 Extending with a Modal Dimension: Temporal Logic of Knowledge

11:45-12:30 Extensions and Restrictions (will include some of the following)


Brief Resume of the Presenters:

Clare Dixon and Michael Fisher have both published and presented widely on the theory, implementation and application of temporal proof and are internationally recognised and respected for their work in this field.

Clare Dixon is an well known for developing practical proof techniques, not only for temporal logics, but also for logics combining temporal and modal dimensions. She has been responsible for key advances in these areas, particularly the development of effective loop search algorithms in temporal resolution and the extension of clausal resolution to temporal logics of knowledge. She also has a high profile in the international TIME workshops, the only annual forum specifically for research into temporal reasoning, co-chairing the 1999 workshop.

Michael Fisher has many years experience working on the specification, verification and implementation of concurrent and distributed systems, in particular utilising temporal logics both as a specification notation and as a programming language. He has been responsible for key advances in temporal logics, such as the introduction of the clausal temporal resolution approach, and the development of a variety of expressive executable temporal logics. In addition to being involved in the TIME workshops, he has also been involved in the International Conference on Temporal Logic.