Deciding Monodic Fragments by Temporal Resolution

Hustadt, U., Konev, B., and Schmidt, R. A. (2005) In Nieuwenhuis, R. (eds), Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Lecture Notes in Artificial Intelligence, Vol. 3632, Springer, 204-218. BiBTeX, PDF, Full text via Springer (Copyright © Springer).

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 fine-grained 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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 07 Jun 06
Copyright © 2005 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk