M. Ludwig and U. Hustadt (2009a): ``Redundancy Elimination in Monodic Temporal Reasoning.'' In N. Peltier and V. Sofronie-Stokkermans, editors, Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP 2009) [Oslo, Norway, July 6-7, 2009].
Abstract, BibTeX, PDF.

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.


Logic and Computation Group at the Department of Computer Science, University of Liverpool
Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Thursday, 08-Aug-2013 18:19:00 BST © 1998-2004 by Ullrich Hustadt.