|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Towards First-Order Temporal Resolution
Degtyarev, Anatoli and Fisher, Michael (2001) Towards First-Order Temporal Resolution. In: KI 2001: Advances in Artificial Intelligence.
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.
Repository Staff Only: item control page