|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
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.
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.
Repository Staff Only: item control page