MPI-I-92-213

The following is a draft version of the first six chapters of a book which is attempting to supply a comprehensive coverage of the mathematical and computational aspects of temporal logic. The first chapter introduces temporal logic and gives a fairly detailed preview of the issues which will be covered in the rest of the whole book. These include expressive power, fixed point temporal languages and applications in computing. Chapter 2 develops the basic idea of a language built from connectives whose semantics is appropriate to some class of underlying "`models"' of time: for example linear or branching time. Chapter 3 introduces Hilbert style axiomatizations of such logics and contains some simple completeness proofs. The incomplete chapter 4 considers the generally incomplete predicate temporal languages and gives examples of some of the variety of choices of language here. In Chapter 5 we debate the merits of using classical first order logic to talk about temporal structures from the "`outside"' instead of using temporal languages "`inside"' the structure. We also consider the possibility of using temporal logic itself as a metalanguage. Finally, in Chapter 6 we present a general theory of axiomatization of temporal logics. This examines and uses the irreflexivity rule of Gabbay to provide very general techniques.

Note:

Since the publication of the book (Gabbay, D. M.; Hodkinson, I.; Reynolds, M. : "Temporal logic: mathematical foundations and computational aspects", Oxford : Clarendon 1994), this work is no longer available as report.