A Resolution-Based Calculus For Temporal Logics

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 approach proposed in this work is based on a particular translation method into classical first-order predicate logic which utilizes certain interesting translational invariants.

Das ständig wachsende Interesse an Temporallogiken in zahlreichen Gebieten der Informatik verlangt nach Methoden, mit deren Hilfe effizient und schnell Schlussfolgerungen in diesen Logiken gezogen werden können. Üblicherweise geschieht dies durch die Entwicklung eines implementierten Kalküls, und tatsächlich wurden in den vergangenen Jahren bemerkenswerte Fortschritte in diese Richtung erzielt. Die bis heute bekannten Verfahren können grob in zwei Hauptkategorien eingeteilt werden: Entweder werden schon bekannte Techniken für andere Logiken (üblicherweise klassische Prädikatenlogik erster Stufe) erweitert, um mit der neuen Syntax zurechtzukommen, oder Übersetzungstechniken in die Prädikatenlogik werden definiert, welche es erlauben schon bekannte Kalküle wiederzuverwenden. Der Ansatz, der in dieser Arbeit vorgestellt wird, basiert auf einer bestimmten Übersetzungsmethode in die klassische Prädikatenlogik erster Stufe und einem darauf aufbauenden Kalkül, der gewisse interessante Übersetzungsvarianten ausnützt.