Guiding Clausal Temporal Resolution

Abstract

The effective mechanisation of temporal logic is vital to the application of temporal reasoning in many fields, for example the verification of reactive systems, the implementation of temporal query languages, and temporal logic programming. Consequently, a variety of proof methods have been developed, implemented and applied. While clausal temporal resolution has been successfully employed for a range of problems, a number of improvements are still required. One particular drawback for certain applications is the restriction that temporal resolution operations must occur only after all relevant non-temporal resolution steps have been carried out. It is this restriction that we consider in this paper, where we introduce, justify and apply a new temporal resolution rule. This rule, which may be seen as a generalisation of the existing temporal resolution rule, can be applied at any time during the refutation, thus providing the possibility for much greater interleaving between temporal and non-temporal operations. In addition, the use of this temporal resolution rule can provide information that is useful in guiding any subsequent search.