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.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Ullrich Hustadt, Boris Konev, Renate A. Schmidt
• Keywords: Automated Reasoning, CADE 2005, First-order Temporal Logic, Immediate Practical Value, Temporal Resolution