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