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

Handling Equality in Monodic Temporal Resolution

Konev, Boris and Degtyarev, Anatoli and Fisher, Michael (2003) Handling Equality in Monodic Temporal Resolution. In: LPAR, Logic for Programming, Artificial Intelligence, and Reasoning,.

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


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 including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated with the clausal resolution method, and state correctness and completeness results.

Item Type:Conference or Workshop Item (Paper)
ID Code:879
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