U. Hustadt, B. Konev, and R. A. Schmidt (2005): ``Deciding Monodic Fragments by Temporal Resolution.'' In R. Nieuwenhuis, editor, Procceedings of the 20th International Conference on Automated Deduction CADE-20 (Tallinn, Estonia, July 22-27, 2005), pp. 204-218. LNAI 3632, Springer.
Abstract, BibTeX, PDF (© Springer), Abstract + PDF (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. [an error occurred while processing this directive]