@INCOLLECTION{HK2004,
 AUTHOR        = {Hustadt, Ullrich and Konev, Boris},
 TITLE         = {{TRP++}: A temporal resolution prover},
 BOOKTITLE     = {Collegium Logicum},
 PUBLISHER     = {Kurt G{\"o}del Society},
 YEAR          = {2004},
 EDITOR        = {Baaz, Matthias and Makowsky, Johann and Voronkov, Andrei},
 PAGES         = {65-79},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf},
 ABSTRACT      = {Temporal logics are extensions of classical logic with
 operators that deal with time. They have been used in a wide variety
 of areas within Computer Science and Artificial Intelligence, for
 example robotics, databases, hardware verification and agent-based
 systems. 
 <p>
 In particular, propositional temporal logics have been
 applied to (i) the specification and verification of reactive
 (e.g. distributed or concurrent) systems; (ii) the synthesis of
 programs from temporal specifications;; (iii) the semantics of
 executable temporal logic; (iv) algorithmic verification via
 model-checking; and (v) knowledge representation and reasoning.
 </p>
 <p>
 In developing these techniques, temporal proof is often required, and
 we base our work on practical proof techniques for the clausal
 resolution method for propositional linear-time temporal logic
 PLTL. The method is based on an intuitive clausal form, called SNF,
 comprising three main clause types and a small number of resolution
 rules.
 </p>
 While the approach has been shown to be competitive using
 a prototype implementation of the method, we now aim at an even more
 efficient implementation. This implementation, called TRP++, is the
 focus of this paper.}
}