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


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)
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