|
Published Articles >> Table of Contents >> Abstract
10th International Symposium on Temporal Representation and Reasoning and Fourth International Conference on Temporal Logic
p. 72
Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case
Boris Konev, University of Liverpool
Anatoli Degtyarev, King’s College London
Clare Dixon, University of Liverpool
Michael Fisher, University of Liverpool
Ullrich Hustadt, University of Liverpool
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt,
"Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case,"
time-ictl,
p. 72,
10th International Symposium on Temporal Representation and Reasoning and Fourth International Conference on Temporal Logic,
2003
|
|
