@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.}
}