{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:08:45Z","timestamp":1761620925384,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,1]]},"abstract":"<jats:p>\n            Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the\n            <jats:italic>monodic<\/jats:italic>\n            fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for this monodic fragment.In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for monodic formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL can be established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.\n          <\/jats:p>","DOI":"10.1145\/1119439.1119443","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T16:09:20Z","timestamp":1147104560000},"page":"108-150","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Monodic temporal resolution"],"prefix":"10.1145","volume":"7","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[{"name":"King's College London, London, UK"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, UK"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, UK"}]}],"member":"320","published-online":{"date-parts":[[2006,1]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Artale A. and Franconi E. 2004. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence M. Fisher D. M. Gabbay and L. Vila Eds. Elsevier Amsterdam The Netherlands.]]  Artale A. and Franconi E. 2004. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence M. Fisher D. M. Gabbay and L. Vila Eds. Elsevier Amsterdam The Netherlands.]]"},{"volume":"2424","volume-title":"Proceedings of JELIA'02","author":"Artale A.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","first-page":"19","article-title":"Resolution theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, Amsterdam, The Netherlands","volume":"2","author":"Bachmair L.","year":"2001","journal-title":"Chapter"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Springer Berlin Germany.]]  B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 1997. The Classical Decision Problem. Springer Berlin Germany.]]","DOI":"10.1007\/978-3-642-59207-2"},{"volume":"2174","volume-title":"KI 2001, Proceedings. Lecture Notes in Computer Science","author":"Degtyarev A.","key":"e_1_2_1_5_1"},{"volume":"2381","volume-title":"Proceedings. Lecture Notes in Computer Science","author":"Degtyarev A.","key":"e_1_2_1_6_1"},{"volume":"2850","volume-title":"Proceedings of 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Lecture Notes in Computer Science","author":"Degtyarev A.","key":"e_1_2_1_7_1"},{"volume":"2741","volume-title":"Proc. CADE-19","author":"Degtyarev A.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021352309671"},{"volume-title":"Proceedings of the CADE-13","series-title":"Lecture Notes in Artificial Intelligence","author":"Dixon C.","key":"e_1_2_1_10_1"},{"volume-title":"Amsterdam, The Netherlands","year":"1850","author":"Ferm\u00fcller C.","key":"e_1_2_1_11_1"},{"volume-title":"Proceedings of IJCAI'91","year":"1991","author":"Fisher M.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752618"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.4.429"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371311"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/544862.544943"},{"volume-title":"Proceedings of 3rd International Workshop on Automated Verification of Critical Systems (AVoCS 2003; Southampton, U.K.). 177--186","author":"Fisher M.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings on Colloquium on Temporal Logic and Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science","volume":"398","author":"Gabbay D.","year":"1987"},{"volume-title":"Proceedings of the 16th International FLAIRS Conference. AAAI Press","author":"Gabelaia D.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","unstructured":"Gallier H. 1986. Logic for Computer Science. Harper and Row New York NY.]]  Gallier H. 1986. Logic for Computer Science. Harper and Row New York NY.]]"},{"volume-title":"Proceedings of the 14th IEEE Symposium on Logic in Computer Science. 295--305","author":"Ganzinger H.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021356410579"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume":"2741","volume-title":"Proceedings of CADE-19","author":"Hustadt U.","key":"e_1_2_1_25_1"},{"volume":"3097","volume-title":"Lecture Notes in Artificial Intelligence","author":"Hustadt U.","key":"e_1_2_1_26_1"},{"volume":"1632","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","author":"Hustadt U.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646730.703674"},{"volume-title":"Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press","author":"Kesten Y.","key":"e_1_2_1_29_1"},{"volume-title":"Proceedings TIME-ICTL'03","author":"Konev B.","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.005"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:STUD.0000027468.28935.6d"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Berlin Germany.]]   Manna Z. and Pnueli A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Berlin Germany.]]","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_34_1","unstructured":"Maslov S. 1968. The inverse method for establishing deducibility for logical calculi. Trudy Math. Inst. Steklov XCVIII 22--25. (English translation AMS 1971.)]]  Maslov S. 1968. The inverse method for establishing deducibility for logical calculi. Trudy Math. Inst. Steklov XCVIII 22--25. (English translation AMS 1971.)]]"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.1992.10510779"},{"key":"e_1_2_1_36_1","first-page":"335","article-title":"Computing small clause normal forms. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, Amsterdam, The Netherlands","volume":"6","author":"Nonnengart A.","year":"2001","journal-title":"Chapter"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of IJCAR","volume":"2083","author":"Riazanov A.","year":"2001"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90045-X"},{"volume-title":"Automation of Reasoning (Classical Papers on Computational Logic)","year":"1968","author":"Tseitin G.","key":"e_1_2_1_41_1"},{"key":"e_1_2_1_42_1","unstructured":"Wolper P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation. Stanford University Stanford CA.]]   Wolper P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation. Stanford University Stanford CA.]]"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695115"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Wolter F. and Zakharyaschev M. 2002a. Axiomatizing the monodic fragment of first-order temporal logic. Ann. Pure Appl. logic 118 133--145.]]  Wolter F. and Zakharyaschev M. 2002a. Axiomatizing the monodic fragment of first-order temporal logic. Ann. Pure Appl. logic 118 133--145.]]","DOI":"10.1016\/S0168-0072(01)00124-5"},{"key":"e_1_2_1_45_1","unstructured":"Wolter F. and Zakharyaschev M. 2002b. Qualitative spatio-temporal representation and reasoning: A computational perspective. In Exploring Artificial Intelligence in the New Millenium. Morgan Kaufmann San Francisco CA 175--216.]]   Wolter F. and Zakharyaschev M. 2002b. Qualitative spatio-temporal representation and reasoning: A computational perspective. In Exploring Artificial Intelligence in the New Millenium. Morgan Kaufmann San Francisco CA 175--216.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119443","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1119439.1119443","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:18Z","timestamp":1750262898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119443"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.1145\/1119439.1119443"],"URL":"https:\/\/doi.org\/10.1145\/1119439.1119443","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,1]]},"assertion":[{"value":"2006-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}