Chapter 9 Theorem-proving for discrete temporal logic

M. Reynolds, C. Dixon

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

Abstract

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
Pages279-313
Number of pages35
Volume1
DOIs
Publication statusPublished - 2005

Keywords

  • Temporal Logic
  • Model Checking
  • Stit

Fingerprint

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

Cite this