Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

Publications Master Template :: Thesis :: Nonnengart, Andreas

Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit

Author(s)*:Nonnengart, Andreas
BibTeX citekey*:Nonnengart-Dissertation

Title, School
Title*:A Resolution-Based Calculus for Temporal Logics
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation

Note, Abstract, Copyright
LaTeX 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.

Referees, Status, Dates
1. Referee:Hans Jürgen Ohlbach
2. Referee:Dov M. Gabbay
Supervisor:Hans Jürgen Ohlbach
Date Kolloquium:21 December 1995
Chair Kolloquium:Jörg H. Siekmann

MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:experts only
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:
AUTHOR = {Nonnengart, Andreas},
TITLE = {A Resolution-Based Calculus for Temporal Logics},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {1995},
TYPE = {Doctoral dissertation}
MONTH = {December},

Entry last modified by Andreas Nonnengart, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Uwe Brahm
03/26/1996 04:26:59 PM

Andreas Nonnengart
Christine Kiesel
Uwe Brahm/MPII/DE

Edit Dates
12/03/97 13:15:52
02/12/96 09:27:10
03/26/96 04:32:44 PM