Tech Reports

ULCS-03-012

Exploring the Monodic Fragment of First-Order Temporal Logic using Clausal Temporal Resolution

Anatoli Degtyarev, Michael Fisher and Boris Konev

Abstract

Until recently, first-order temporal logic has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of first-order temporal logic. Following this result, the clausal temporal resolution technique, originally developed for propositional temporal logics, has been extended to such monodic fragments. While this is useful as a practical proof technique for certain monodic classes, in this paper we show that the use of clausal temporal resolution provides us with increased understanding of the monodic fragment. In particular, several features of monodic first-order temporal logic are established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, an extension of finite axiomatisability beyond the monodic fragment.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.