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

Mechanising first-order temporal resolution

Konev, Boris and Degtyarev, Anatoli and Dixon, Clare and Fisher, Michael and Hustadt, Ullrich (2005) Mechanising first-order temporal resolution. Information and Computtation, 199 (1-2). pp. 55-86. ISSN 0747-7171

[img]PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL:


First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Item Type:Article
ID Code:845
Deposited By:Dr Anatoli Degtyarev
Deposited On:07 Nov 2007 16:07
Last Modified:07 Nov 2007 16:07

Repository Staff Only: item control page