Tech Reports

ULCS-03-001

Monodic Temporal Resolution

Anatoly Degtyarev, Michael Fisher and Boris Konev


Abstract

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 have identified important enumable 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 results, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

[Full Paper]