@INPROCEEDINGS{Ludwig+Hustadt@TIME2009,
 AUTHOR        = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE         = {Resolution-Based Model Construction for {PLTL}},
 BOOKTITLE     = {Proceedings of the 16th International Symposium on
 Temporal Representation and Reasoning (TIME-2009)
 [Brixen-Bressanone, Italy, 23-25 July 2009]},
 YEAR          = {2009},
 EDITOR        = {Lutz, Carsten and Raskin, Jean-Francois},
 PAGES         = {73-80},
 PUBLISHER     = {IEEE Computer Society},
 CADDRESS      = {Brixen-Bressanone, Italy},
 CYEAR         = {2009},
 CMONTH        = jul # {23--25},
 YEAR          = {2009},
 URL           = {Ludwig+Hustadt@TIME2009.pdf},
 ABSTRACT = {The elimination of redundant clauses is an essential part
 of resolution-based theorem proving in order to reduce the size of
 the search space. In this paper we focus on ordered fine-grained
 resolution with selection, a sound and complete resolution-based
 calculus for monodic first-order temporal logic. The inference rules
 of the calculus are based on standard resolution between different
 types of temporal clauses on one hand and inference rules with
 semi-decidable applicability conditions that handle eventualities on
 the other hand. We define a subsumption relation on temporal clauses
 and show how the calculus can be extended with reduction rules that
 eliminate redundant clauses. We also illustrate how the subsumption
 relation can be used to simplify the loop search process for
 eventualities.}
}