Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

Monodic temporal resolution

Degtyarev, Anatoli and Fisher, Michael and Konev, Boris (2006) Monodic temporal resolution. ACM Transactions on Computational Logic, 7 (1). pp. 108-150.

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


Until recently, First-Order Temporal Logic (FOTL) has been only partially 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 previously available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for this monodic fragment.In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for monodic formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL can be 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, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

Item Type:Article
ID Code:837
Deposited By:Dr Anatoli Degtyarev
Deposited On:04 Nov 2007 13:15
Last Modified:04 Nov 2007 13:15

Repository Staff Only: item control page