Item

Abstract

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.