Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt





A Resolution-Based Calculus for Temporal Logics


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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

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

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.