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 First-Order Temporal Resolution

Degtyarev, Anatoli and Fisher, Michael (2001) Towards First-Order Temporal Resolution. In: KI 2001: Advances in Artificial Intelligence.

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

Abstract

In this paper we show how to extend clausal temporal resolution to the ground eventuality fragment of monodic first-order temporal logic, which has recently been introduced by Hodkinson, Wolter and Zakharyaschev. While a finite Hilbert-like axiomatization of complete monodic first order temporal logic was developed by Wolter and Zakharyaschev, we propose a temporal resolution-based proof system which reduces the satisfiability problem for ground eventuality monodic first-order temporal formulae to the satisfiability problem for formulae of classical first-order logic.

Item Type:Conference or Workshop Item (Paper)
Subjects:UNSPECIFIED
ID Code:888
Deposited By:Dr Anatoli Degtyarev
Deposited On:08 Nov 2007 08:33
Last Modified:08 Nov 2007 08:33

Repository Staff Only: item control page