@INPROCEEDINGS{Hustadt+Konev+Schmidt@CADE2005,
 AUTHOR        = {Ullrich Hustadt and Boris Konev and Renate A. Schmidt},
 TITLE         = {Deciding Monodic Fragments by Temporal Resolution},
 BOOKTITLE     = {Proceedings of the 20th International Conference on
 Automated Deduction (CADE-20) [Tallin, Estonia, 22-27 July 2005]},
 YEAR          = {2005},
 EDITOR        = {Robert Nieuwenhuis},
 PAGES         = {204-218},
 PUBLISHER     = {Springer},
 PYEAR         = {2005},
 CADDRESS      = {Tallinn, Estonia},
 CYEAR         = {2005},
 CMONTH        = jul # {~22-27},
 SERIES        = {LNAI},
 VOLUME        = {3632},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/Hustadt+Konev+Schmidt@CADE2005.pdf},
 URL           = {http://dx.doi.org/10.1007/11532231_15},
 ABSTRACT      = {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.
 <p>
 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.
 </p>
 The latter is of immediate practical value, due to the
 availability of <a href="http://www.csc.liv.ac.uk/~konev/TeMP/">TeMP</a>, 
 an implementation of fine-grained temporal resolution.}
}