Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS.
|Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Friday, 16-Aug-2013 16:50:51 BST © 1998-2004 by Ullrich Hustadt.|