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

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

Konev, Boris and Degtyarev, Anatoli and Dixon, Clare and Fisher, Michael and Hustadt, Ullrich (2003) Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. In: 10th International Symposium on Temporal Representation and Reasoning.

[img]Postscript - Repository staff only - Requires a viewer, such as GSview
166Kb

Abstract

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. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

Item Type:Conference or Workshop Item (Paper)
Subjects:UNSPECIFIED
ID Code:880
Deposited By:Dr Anatoli Degtyarev
Deposited On:07 Nov 2007 16:03
Last Modified:07 Nov 2007 16:03

Repository Staff Only: item control page