@ARTICLE{Konev+Degtyarev+Dixon+Fisher+Hustadt@InfComputat2005,
 AUTHOR        = {Boris Konev and Anatoli Degtyarev and Clare Dixon and Michael Fisher and Ullrich Hustadt},
 TITLE         = {Mechanising first-order temporal resolution},
 JOURNAL       = {Information and Computation},
 YEAR          = {2005},
 VOLUME        = {199},
 NUMBER        = {1-2},
 PAGES         = {55-86},
 URL           = {http://dx.doi.org/10.1016/j.ic.2004.10.005},
 ABSTRACT = {First-order temporal logic is a concise and powerful
 notation, with many potential applications in both Computer Science
 and Artificial Intelligence. While the full logic is highly complex,
 recent work on monodic first-order temporal logics has identified
 important enumerable and even decidable fragments. Although a
 complete and correct resolution-style calculus has already been
 suggested for this specific fragment, this calculus involves
 constructions too complex to be of practical value. In this paper, we
 develop a machine-oriented clausal resolution method which features
 radically simplified proof search. We first define a normal form for
 monodic formulae and then introduce a novel resolution calculus that
 can be applied to formulae in this normal form. By careful encoding,
 parts of the calculus can be implemented using classical first-order
 resolution and can, thus, be efficiently implemented. We prove
 correctness and completeness results for the calculus and illustrate
 it on a comprehensive example. An implementation of the method is
 briefly discussed.}
}