@inproceedings{Konev+Degtyarev+Dixon+Fisher+Hustadt@TIME2003,
 author    = {Boris Konev and
              Anatoli Degtyarev and
              Clare Dixon and
              Michael Fisher and
              Ullrich Hustadt},
 title     = {Towards the Implementation of First-Order Temporal Resolution:
              the Expanding Domain Case},
 year      = {2003},
 pages     = {72-82},
 url       = {http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882},
 booktitle = {Proceedings of the 10th International Symposium on Temporal Representation
              and Reasoning / 4th International Conference on Temporal
              Logic (TIME-ICTL 2003), [Cairns, Queensland, Australia, 8-10 July 2003]},
 publisher = {IEEE Computer Society},
 year      = {2003},
 isbn      = {0-7695-1912-1},
 bibsource = {DBLP, http://dblp.uni-trier.de},
 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 has identified 
 important enumerable and even decidable fragments. In this paper, 
 we develop a clausal resolution method for the monodic fragment 
 of first-order temporal logic over expanding domains. We first 
 define a normal form for monodic formulae and then introduce novel 
 resolution calculi that can be applied to formulae in this normal form. 
 We state correctness and completeness results for the method. 
 We illustrate the method on a comprehensive example. The method is 
 based on classical first-order resolution and can, thus, be 
 efficiently implemented.}
}

{"_id":"LhCuRDysnZew4sGpM","bibbaseid":"konev-degtyarev-dixon-fisher-hustadt-towardstheimplementationoffirstordertemporalresolutiontheexpandingdomaincase-2003","author_short":["Konev, B.","Degtyarev, A.","Dixon, C.","Fisher, M.","Hustadt, U."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Boris"],"propositions":[],"lastnames":["Konev"],"suffixes":[]},{"firstnames":["Anatoli"],"propositions":[],"lastnames":["Degtyarev"],"suffixes":[]},{"firstnames":["Clare"],"propositions":[],"lastnames":["Dixon"],"suffixes":[]},{"firstnames":["Michael"],"propositions":[],"lastnames":["Fisher"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]}],"title":"Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case","year":"2003","pages":"72-82","url":"http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882","booktitle":"Proceedings of the 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), [Cairns, Queensland, Australia, 8-10 July 2003]","publisher":"IEEE Computer Society","isbn":"0-7695-1912-1","bibsource":"DBLP, http://dblp.uni-trier.de","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 has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.","bibtex":"@inproceedings{Konev+Degtyarev+Dixon+Fisher+Hustadt@TIME2003,\n author = {Boris Konev and\n Anatoli Degtyarev and\n Clare Dixon and\n Michael Fisher and\n Ullrich Hustadt},\n title = {Towards the Implementation of First-Order Temporal Resolution:\n the Expanding Domain Case},\n year = {2003},\n pages = {72-82},\n url = {http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882},\n booktitle = {Proceedings of the 10th International Symposium on Temporal Representation\n and Reasoning / 4th International Conference on Temporal\n Logic (TIME-ICTL 2003), [Cairns, Queensland, Australia, 8-10 July 2003]},\n publisher = {IEEE Computer Society},\n year = {2003},\n isbn = {0-7695-1912-1},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n abstract = {First-order temporal logic is a concise and powerful notation, \n with many potential applications in both Computer Science and \n Artificial Intelligence. While the full logic is highly complex, \n recent work on monodic first-order temporal logics has identified \n important enumerable and even decidable fragments. In this paper, \n we develop a clausal resolution method for the monodic fragment \n of first-order temporal logic over expanding domains. We first \n define a normal form for monodic formulae and then introduce novel \n resolution calculi that can be applied to formulae in this normal form. \n We state correctness and completeness results for the method. \n We illustrate the method on a comprehensive example. The method is \n based on classical first-order resolution and can, thus, be \n efficiently implemented.}\n}\n\n","author_short":["Konev, B.","Degtyarev, A.","Dixon, C.","Fisher, M.","Hustadt, U."],"key":"Konev+Degtyarev+Dixon+Fisher+Hustadt@TIME2003","id":"Konev+Degtyarev+Dixon+Fisher+Hustadt@TIME2003","bibbaseid":"konev-degtyarev-dixon-fisher-hustadt-towardstheimplementationoffirstordertemporalresolutiontheexpandingdomaincase-2003","role":"author","urls":{"Paper":"http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214882"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["towards","implementation","first","order","temporal","resolution","expanding","domain","case","konev","degtyarev","dixon","fisher","hustadt"],"title":"Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case","year":2003}