|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Mechanising first-order temporal resolution
Konev, Boris and Degtyarev, Anatoli and Dixon, Clare and Fisher, Michael and Hustadt, Ullrich (2005) Mechanising first-order temporal resolution. Information and Computtation, 199 (1-2). pp. 55-86. ISSN 0747-7171
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. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.
Repository Staff Only: item control page