{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:14:39Z","timestamp":1763968479559,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"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":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523731","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"395-409","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["CycleQ: an efficient basis for cyclic equational reasoning"],"prefix":"10.1145","author":[{"given":"Eddie","family":"Jones","sequence":"first","affiliation":[{"name":"University of Bristol, UK"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Steven","family":"Ramsay","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_18"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0435-9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013087"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274490"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_8"},{"volume-title":"Sequent calculus proof systems for inductive definitions. Ph. D. Dissertation","author":"Brotherston James","key":"e_1_3_2_1_7_1","unstructured":"James Brotherston . 2006. Sequent calculus proof systems for inductive definitions. Ph. D. Dissertation . University of Edinburgh. College of Science and Engineering. School of Informatics. . James Brotherston. 2006. Sequent calculus proof systems for inductive definitions. Ph. D. Dissertation. University of Edinburgh. College of Science and Engineering. School of Informatics.."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328453"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51081-8_100"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012826"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_123"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13977-2_3"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:1)2020"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.29"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.29007\/hzq3"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the Seminaire d\u2019Informatique Theorique","author":"Dershowitz Nachum","year":"1982","unstructured":"Nachum Dershowitz . 1982 . Applications of the Knuth-Bendix Completion Procedure . In Proceedings of the Seminaire d\u2019Informatique Theorique . Paris. 95\u2013111. Nachum Dershowitz. 1982. Applications of the Knuth-Bendix Completion Procedure. In Proceedings of the Seminaire d\u2019Informatique Theorique. Paris. 95\u2013111."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16761-7_60"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73579"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-1675-3_3"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-23250-4_9"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17172-7_6"},{"key":"#cr-split#-e_1_3_2_1_28_1.1","unstructured":"Eddie Jones C Ong H Luke and Steven Ramsay. 2021. CycleQ: An Efficient Basis for Cyclic Equational Reasoning. https:\/\/doi.org\/10.48550\/arXiv.2111.12553 10.48550\/arXiv.2111.12553"},{"key":"#cr-split#-e_1_3_2_1_28_1.2","doi-asserted-by":"crossref","unstructured":"Eddie Jones C Ong H Luke and Steven Ramsay. 2021. CycleQ: An Efficient Basis for Cyclic Equational Reasoning. https:\/\/doi.org\/10.48550\/arXiv.2111.12553","DOI":"10.1145\/3519939.3523731"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90062-X"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16780-3_83"},{"key":"e_1_3_2_1_32_1","unstructured":"Matt Kaufmann and J Strother Moore. 2021. ACL2 User\u2019s Manual.  Matt Kaufmann and J Strother Moore. 2021. ACL2 User\u2019s Manual."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434282"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"volume-title":"Generalisation as a critic to the induction strategy. Master\u2019s thesis. Department of Artificial Intelligence","author":"Maclean Ewen","key":"e_1_3_2_1_37_1","unstructured":"Ewen Maclean . 1999. Generalisation as a critic to the induction strategy. Master\u2019s thesis. Department of Artificial Intelligence , University of Edinburgh. Ewen Maclean. 1999. Generalisation as a critic to the induction strategy. Master\u2019s thesis. Department of Artificial Intelligence, University of Edinburgh."},{"key":"e_1_3_2_1_38_1","volume-title":"Complementation is more difficult with automata on infinite words","author":"Michel Max","year":"1988","unstructured":"Max Michel . 1988. Complementation is more difficult with automata on infinite words . CNET , Paris , 15 ( 1988 ). Max Michel. 1988. Complementation is more difficult with automata on infinite words. CNET, Paris, 15 (1988)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567461"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_86"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_2_1_42_1","unstructured":"Dan Ros\u00e9n. [n. d.]. HipSpec Evaluation Results. http:\/\/danr.github.io\/hipspec\/  Dan Ros\u00e9n. [n. d.]. HipSpec Evaluation Results. http:\/\/danr.github.io\/hipspec\/"},{"volume-title":"Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis","author":"Ros\u00e9n Dan","key":"e_1_3_2_1_43_1","unstructured":"Dan Ros\u00e9n . 2012. Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis . University of Gothenburg , Sweden. Dan Ros\u00e9n. 2012. Proving equational Haskell properties using automated theorem provers. Master\u2019s thesis. University of Gothenburg, Sweden."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_10"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_27"},{"key":"e_1_3_2_1_47_1","unstructured":"Sorin Stratulat. 2019. Efficient Validation of FOL ID Cyclic Induction Reasoning.  Sorin Stratulat. 2019. Efficient Validation of FOL ID Cyclic Induction Reasoning."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC51798.2020.00025"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.342.11"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_30"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498725"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_30"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32254-2_12"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"San Diego CA USA","acronym":"PLDI '22"},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523731","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:31Z","timestamp":1750183831000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":55,"alternative-id":["10.1145\/3519939.3523731","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523731","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}