Help Privacy Policy Disclaimer
  Advanced SearchBrowse





A Resolution-Based Calculus for Temporal Logics


Nonnengart,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Nonnengart, A. (1995). A Resolution-Based Calculus for Temporal Logics. PhD Thesis, Universität des Saarlandes, Saarbrücken.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AC2B-5
The increasing interest in applying temporal logics in various areas of computer science requires the development of efficient means that allow to reason within such logics. Usually this is realized by an implementable calculus and indeed remarkable progress has been made in the last two decades. The approaches developed so far can be roughly divided into two main categories: Either known techniques are extended to cope with the temporal logic syntax, or translation techniques into predicate logic are defined which allow to exploit already existing calculi. The former approach has the advantage that derivations remain within the temporal logic syntax, whereas the latter approach benefits from many years (in fact decades) of experience gained in classical logic theorem proving. The approach proposed in this work is based on a particular translation method into classical first-order predicate logic which utilizes certain interesting translational invariants. The reader is assumed to have detailed knowledge of automated theorem proving and formal logic, in particular classical first-order predicate logic. Although the introduction of modal and temporal logics is fairly self-contained at least some knowledge of these logic areas would be quite helpful.