@INPROCEEDINGS{Ludwig+Hustadt@FTP2009,
 AUTHOR        = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE         = {Redundancy Elimination in Monodic Temporal Reasoning},
 BOOKTITLE     = {Proceedings of the 7th International Workshop on First-Order
Theorem Proving (FTP 2009) [Oslo, Norway, 6-7 July 2009]},
 YEAR          = {2009},
 EDITOR        = {Peltier, N. and Sofronie-Stokkermans, V.},
 PAGES         = {},
 CADDRESS      = {Oslo, Norway},
 CYEAR         = {2009},
 CMONTH        = jul # {6-7},
 YEAR          = {2009},
 URL           = {Ludwig+Hustadt@FTP2009.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.}
}