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

Monodic Temporal Resolution

Degtyarev, Anatoli and Fisher, Michael and Konev, Boris (2003) Monodic Temporal Resolution. In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction.

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


First-order temporal logic is a coincise 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 have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Item Type:Conference or Workshop Item (Paper)
ID Code:878
Deposited By:Dr Anatoli Degtyarev
Deposited On:07 Nov 2007 16:09
Last Modified:07 Nov 2007 16:09

Repository Staff Only: item control page