{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:51Z","timestamp":1760202651518,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/D060451"],"award-info":[{"award-number":["EP\/D060451"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003213","name":"Beijing Municipal Education Commission","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003213","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61303018"],"award-info":[{"award-number":["61303018"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Technology Foundation for Selected Overseas Chinese Scholars, Bureau of Human Resources and Social Security of Beijing"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete, and terminating, and consider the complexity of the calculus.<\/jats:p>","DOI":"10.1145\/2529993","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A resolution calculus for the branching-time temporal logic CTL"],"prefix":"10.1145","volume":"15","author":[{"given":"Lan","family":"Zhang","sequence":"first","affiliation":[{"name":"Capital University of Economics and Business, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[{"name":"University of Liverpool, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"University of Liverpool, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03)","volume":"2796","author":"Abate P.","unstructured":"P. Abate and R. Gor\u00e9 . 2003. The Tableaux Work Bench . In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03) . Lecture Notes in Computer Science , vol. 2796 , Springer-Verlag, Berlin, 230--236. P. Abate and R. Gor\u00e9. 2003. The Tableaux Work Bench. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03). Lecture Notes in Computer Science, vol. 2796, Springer-Verlag, Berlin, 230--236."},{"key":"e_1_2_2_2_1","volume-title":"Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07)","volume":"4790","author":"Abate P.","unstructured":"P. Abate , R. Gor\u00e9 , and F. Widmann . 2007. One-pass Tableaux for computation tree logic . In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07) . Lecture Notes in Computer Science , vol. 4790 , Springer-Verlag, Berlin, 32--46. P. Abate, R. Gor\u00e9, and F. Widmann. 2007. One-pass Tableaux for computation tree logic. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07). Lecture Notes in Computer Science, vol. 4790, Springer-Verlag, Berlin, 32--46."},{"volume-title":"Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME'04)","author":"Afanasiev L.","unstructured":"L. Afanasiev , M. Franceschet , M. Marx , and M. De Rijke . 2004. CTL model checking for processing simple XPath queries . In Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME'04) . 117--124. L. Afanasiev, M. Franceschet, M. Marx, and M. De Rijke. 2004. CTL model checking for processing simple XPath queries. In Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME'04). 117--124.","key":"e_1_2_2_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_4_1","DOI":"10.1007\/978-3-540-39989-6_11"},{"doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. 2001. Resolution theorem proving. In Handbook of Automated Reasoning. vol. 1 Elsevier 19--99.  L. Bachmair and H. Ganzinger. 2001. Resolution theorem proving. In Handbook of Automated Reasoning. vol. 1 Elsevier 19--99.","key":"e_1_2_2_5_1","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"volume-title":"Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments. 17--29","author":"Basso A.","unstructured":"A. Basso and A. Bolotov . 2007. Towards GCM re-configuration extending specification by norms . In Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments. 17--29 . A. Basso and A. Bolotov. 2007. Towards GCM re-configuration extending specification by norms. In Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments. 17--29.","key":"e_1_2_2_6_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_7_1","DOI":"10.1145\/567532.567551"},{"volume-title":"Proceedings of the 7th International Workshop on Temporal Representation and Reasoning (TIME'00)","author":"Bolotov A.","unstructured":"A. Bolotov and C. Dixon . 2000. Resolution for branching time temporal logics: Applying the temporal resolution rule . In Proceedings of the 7th International Workshop on Temporal Representation and Reasoning (TIME'00) . 163--172. A. Bolotov and C. Dixon. 2000. Resolution for branching time temporal logics: Applying the temporal resolution rule. In Proceedings of the 7th International Workshop on Temporal Representation and Reasoning (TIME'00). 163--172.","key":"e_1_2_2_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_10_1","DOI":"10.1080\/095281399146625"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02)","volume":"2404","author":"Cimatti A.","unstructured":"A. Cimatti , E. M. Clarke , E. Giunchiglia , F. Giunchiglia , M. Pistore , M. Roveri , R. Sebastiani , and A. Tacchella . 2002. NuSMV 2: An OpenSource tool for symbolic model checking . In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02) . Lecture Notes in Computer Science , vol. 2404 , Springer-Verlag, Berlin, 359--364. A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV 2: An OpenSource tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02). Lecture Notes in Computer Science, vol. 2404, Springer-Verlag, Berlin, 359--364."},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science","volume":"131","author":"Clarke E. M.","unstructured":"E. M. Clarke and E. A. Emerson . 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic . In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science , vol. 131 , Springer-Verlag, Berlin, 52--71. E. M. Clarke and E. A. Emerson. 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science, vol. 131, Springer-Verlag, Berlin, 52--71."},{"doi-asserted-by":"publisher","key":"e_1_2_2_13_1","DOI":"10.1145\/5397.5399"},{"unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 2000. Model Checking. MIT Press.  E. M. Clarke O. Grumberg and D. A. Peled. 2000. Model Checking. MIT Press.","key":"e_1_2_2_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_15_1","DOI":"10.1023\/A:1018942108420"},{"doi-asserted-by":"publisher","key":"e_1_2_2_16_1","DOI":"10.1016\/S0004-3702(02)00196-0"},{"key":"e_1_2_2_17_1","first-page":"996","article-title":"Temporal and modal logic. In Handbook of Theoretical Computer Science, Elsevier","volume":"16","author":"Emerson E. A.","year":"1990","unstructured":"E. A. Emerson . 1990 . Temporal and modal logic. In Handbook of Theoretical Computer Science, Elsevier , Chapter 16 , 996 -- 1072 . E. A. Emerson. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, Elsevier, Chapter 16, 996--1072.","journal-title":"Chapter"},{"doi-asserted-by":"publisher","key":"e_1_2_2_18_1","DOI":"10.1145\/800070.802190"},{"doi-asserted-by":"publisher","key":"e_1_2_2_19_1","DOI":"10.1016\/0022-0000(85)90001-7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_20_1","DOI":"10.1145\/4904.4999"},{"doi-asserted-by":"publisher","key":"e_1_2_2_21_1","DOI":"10.1109\/SFCS.1988.21949"},{"doi-asserted-by":"publisher","key":"e_1_2_2_23_1","DOI":"10.1145\/371282.371311"},{"doi-asserted-by":"publisher","key":"e_1_2_2_24_1","DOI":"10.1007\/978-3-540-74621-8_13"},{"doi-asserted-by":"publisher","key":"e_1_2_2_25_1","DOI":"10.1016\/j.entcs.2010.04.008"},{"doi-asserted-by":"publisher","key":"e_1_2_2_26_1","DOI":"10.1109\/TIME.2011.16"},{"doi-asserted-by":"publisher","key":"e_1_2_2_27_1","DOI":"10.5555\/975331"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer.   Z. Manna and A. Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer.","key":"e_1_2_2_28_1","DOI":"10.1007\/978-1-4612-0931-7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_29_1","DOI":"10.1007\/978-3-540-31980-1_15"},{"doi-asserted-by":"publisher","key":"e_1_2_2_30_1","DOI":"10.1007\/978-3-540-87803-2_25"},{"doi-asserted-by":"publisher","key":"e_1_2_2_31_1","DOI":"10.1109\/TIME.2010.7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_32_1","DOI":"10.1016\/0022-0000(80)90061-6"},{"doi-asserted-by":"publisher","key":"e_1_2_2_33_1","DOI":"10.1007\/s00165-011-0193-4"},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98)","volume":"1397","author":"Robinson J. A.","year":"1965","unstructured":"J. A. Robinson . 1965 . Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227--234. S. Schwendimann. 1998. A new one-pass tableau calculus for PLTL . In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) . Lecture Notes in Computer Science , vol. 1397 , Springer-Verlag, Berlin, 277--291. J. A. Robinson. 1965. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227--234. S. Schwendimann. 1998. A new one-pass tableau calculus for PLTL. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98). Lecture Notes in Computer Science, vol. 1397, Springer-Verlag, Berlin, 277--291."},{"doi-asserted-by":"publisher","key":"e_1_2_2_35_1","DOI":"10.1145\/22145.22173"},{"doi-asserted-by":"publisher","key":"e_1_2_2_36_1","DOI":"10.1016\/0022-0000(86)90026-7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_37_1","DOI":"10.1007\/978-3-540-73595-3_38"},{"doi-asserted-by":"publisher","key":"e_1_2_2_39_1","DOI":"10.1007\/978-3-642-02959-2_20"},{"key":"e_1_2_2_40_1","first-page":"2","article-title":"CTL-RP: A computational tree logic resolution prover","volume":"23","author":"Zhang L.","year":"2009","unstructured":"L. Zhang , U. Hustadt , and C. Dixon . 2009 b. CTL-RP: A computational tree logic resolution prover . AI Commun. 23 , 2 -- 3 , 111--136. L. Zhang, U. Hustadt, and C. Dixon. 2009b. CTL-RP: A computational tree logic resolution prover. AI Commun. 23, 2--3, 111--136.","journal-title":"AI Commun."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2529993","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2529993","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:09:52Z","timestamp":1750234192000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2529993"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2529993"],"URL":"https:\/\/doi.org\/10.1145\/2529993","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}