Sciweavers

Share
CADE
2005
Springer

Deciding Monodic Fragments by Temporal Resolution

12 years 10 months ago
Deciding Monodic Fragments by Temporal Resolution
In this paper we study the decidability of various fragments of monodic first-order temporal logic by temporal resolution. We focus on two resolution calculi, namely, monodic temporal resolution and finegrained temporal resolution. For the first, we state a very general decidability result, which is independent of the particular decision procedure used to decide the first-order part of the logic. For the second, we introduce refinements using orderings and selection functions. This allows us to transfer existing results on decidability by resolution for first-order fragments to monodic first-order temporal logic and obtain new decision procedures. The latter is of immediate practical value, due to the availability of TeMP, an implementation of fine-grained temporal resolution.
Ullrich Hustadt, Boris Konev, Renate A. Schmidt
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Ullrich Hustadt, Boris Konev, Renate A. Schmidt
Comments (0)
books