A Resolution-Based Calculus for Temporal Logics

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.

December

1995

Jörg H. Siekmann