Chapter 9 Theorem-proving for discrete temporal logic

M. Reynolds, C. Dixon

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


This chapter considers theorem proving for discrete temporal logics. We are interested in deciding or at least enumerating the formulas of the logic which are valid, that is, are true in all circumstances. Most of the techniques for temporal theorem-proving have been extensions for methods developed for classical logics but completely novel techniques have also been developed. Initially we concentrate on discrete linear-time temporal logics, describing axiomatic, tableau, automata and resolution based approaches. The application of these approaches to other temporal logics is discussed.
Original languageEnglish
Title of host publicationFoundations of Artificial Intelligence
Number of pages35
Publication statusPublished - 2005


  • Temporal Logic
  • Model Checking
  • Stit


Dive into the research topics of 'Chapter 9 Theorem-proving for discrete temporal logic'. Together they form a unique fingerprint.

Cite this