{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:01:37Z","timestamp":1742947297794,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030897154"},{"type":"electronic","value":"9783030897161"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-89716-1_2","type":"book-chapter","created":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T09:08:02Z","timestamp":1635152882000},"page":"19-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Theorem Proving Using Clausal Resolution: From Past to Present"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4610-9533","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"65","author":"M Abadi","year":"1989","unstructured":"Abadi, M.: The power of temporal proofs. Theor. Comput. Sci. 65(1), 35\u201383 (1989)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 19\u201399. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"2_CR3","unstructured":"Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.): Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. North-Holland (2007)"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1080\/095281399146625","volume":"11","author":"A Bolotov","year":"1999","unstructured":"Bolotov, A., Fisher, M.: A clausal resolution method for CTL branching-time temporal logic. J. Exp. Theor. Artif. Intell. 11(1), 77\u201393 (1999)","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: Spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514\u2013520. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_38"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A Degtyarev","year":"2006","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Trans. Comput. Log. 7(1), 108\u2013150 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/3-540-61511-3_121","volume-title":"Automated Deduction \u2014 Cade-13","author":"C Dixon","year":"1996","unstructured":"Dixon, C.: Search strategies for resolution in temporal logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 673\u2013687. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_121"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1018942108420","volume":"22","author":"C Dixon","year":"1998","unstructured":"Dixon, C.: Temporal resolution using a breadth-first search algorithm. Ann. Math. Artif. Intell. 22, 87\u2013115 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Dixon, C.: Using Otter for temporal resolution. In: Advances in Temporal Logic. Applied Logic Series, vol. 16, pp. 149\u2013166. Kluwer (2000). Proceedings the Second International Conference on Temporal Logic (ICTL). ISBN 0-7923-6149-0","DOI":"10.1007\/978-94-015-9586-5_8"},{"issue":"3","key":"2_CR10","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"2_CR11","unstructured":"Fisher, M.: A resolution method for temporal logic. In: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI), Sydney, Australia, pp. 99\u2013104. Morgan Kaufman, August 1991"},{"issue":"4","key":"2_CR12","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M Fisher","year":"1997","unstructured":"Fisher, M.: A normal form for temporal logic and its application in theorem-proving and execution. J. Log. Comput. 7(4), 429\u2013456 (1997)","journal-title":"J. Log. Comput."},{"key":"2_CR13","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472","volume-title":"An Introduction to Practical Formal Methods Using Temporal Logic","author":"M Fisher","year":"2011","unstructured":"Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1), 12\u201356 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: Combi, C., Leucker, M., Wolter, F. (eds.) Eighteenth International Symposium on Temporal Representation and Reasoning, TIME 2011, L\u00fcbeck, Germany, 12\u201314 September 2011, pp. 49\u201356. IEEE (2011)","DOI":"10.1109\/TIME.2011.16"},{"issue":"1\u20133","key":"2_CR16","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I Hodkinson","year":"2000","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order temporal logics. Ann. Pure Appl. Log. 106(1\u20133), 85\u2013134 (2000)","journal-title":"Ann. Pure Appl. Log."},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-25984-8_23","volume-title":"Automated Reasoning","author":"U Hustadt","year":"2004","unstructured":"Hustadt, U., Konev, B., Riazanov, A., Voronkov, A.: TeMP: a temporal monodic prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 326\u2013330. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25984-8_23"},{"key":"2_CR18","unstructured":"Hustadt, U., Konev, B.: TRP++: a temporal resolution prover. In: 3rd International Workshop on the Implementation of Logics (2002)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 274\u2013278. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_21"},{"key":"2_CR20","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Fensel, D., Giunchiglia, F., McGuinness, D., Williams, M.-A. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR 2002), pp. 533\u2013544. Morgan Kaufmann (2002)"},{"issue":"1\u20132","key":"2_CR21","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.ic.2004.10.005","volume":"199","author":"B Konev","year":"2005","unstructured":"Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Mechanising first-order temporal resolution. Inf. Comput. 199(1\u20132), 55\u201386 (2005)","journal-title":"Inf. Comput."},{"issue":"2\u20133","key":"2_CR22","first-page":"68","volume":"23","author":"M Ludwig","year":"2010","unstructured":"Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal prover. AI Commun. 23(2\u20133), 68\u201396 (2010)","journal-title":"AI Commun."},{"key":"2_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems - Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"issue":"3\u20134","key":"2_CR24","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.jalgor.2007.04.001","volume":"62","author":"C Nalon","year":"2007","unstructured":"Nalon, C., Dixon, C.: Clausal resolution for normal modal logics. J. Algorithms 62(3\u20134), 117\u2013134 (2007)","journal-title":"J. Algorithms"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Nalon, C., Dixon, C., Hustadt, U.: Modal resolution: proofs, layers, and refinements. ACM Trans. Comput. Log. 20(4), 23:1\u201323:38 (2019)","DOI":"10.1145\/3331448"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-319-40229-1_28","volume-title":"Automated Reasoning","author":"C Nalon","year":"2016","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: K$$_{\\rm S}$$P: A resolution-based prover for multimodal K. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 406\u2013415. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_28"},{"issue":"3","key":"2_CR27","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s10817-018-09503-x","volume":"64","author":"C Nalon","year":"2020","unstructured":"Nalon, C., Hustadt, U., Dixon, C.: K$$_{\\rm n}$$: architecture, refinements, strategies and experiments. J. Autom. Reason. 64(3), 461\u2013484 (2020)","journal-title":"J. Autom. Reason."},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-030-79876-5_5","volume-title":"Automated Deduction \u2013 CADE 28","author":"F Papacchini","year":"2021","unstructured":"Papacchini, F., Nalon, C., Hustadt, U., Dixon, C.: Efficient local reductions to basic modal logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 76\u201392. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_5"},{"issue":"2,3","key":"2_CR29","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15(2,3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-02959-2_20","volume-title":"Automated Deduction \u2013 CADE-22","author":"L Zhang","year":"2009","unstructured":"Zhang, L., Hustadt, U., Dixon, C.: A refined resolution calculus for CTL. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 245\u2013260. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_20"},{"issue":"2\u20133","key":"2_CR31","first-page":"111","volume":"23","author":"L Zhang","year":"2009","unstructured":"Zhang, L., Hustadt, U., Dixon, C.: CTL-RP: a computational tree logic resolution prover. AI Commun. 23(2\u20133), 111\u2013136 (2009)","journal-title":"AI Commun."},{"issue":"1","key":"2_CR32","doi-asserted-by":"publisher","first-page":"1529","DOI":"10.1145\/2529993","volume":"15","author":"L Zhang","year":"2014","unstructured":"Zhang, L., Hustadt, U., Dixon, C.: A resolution calculus for the branching-time temporal logic CTL. ACM Trans. Comput. Log. 15(1), 1529\u20133785 (2014)","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-89716-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T09:09:10Z","timestamp":1635152950000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-89716-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030897154","9783030897161"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-89716-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Liverpool","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp2021.csc.liv.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}