{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:31Z","timestamp":1785202231416,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:00:00Z","timestamp":1725840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,9]]},"DOI":"10.1145\/3678232.3678236","type":"proceedings-article","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:17Z","timestamp":1725489317000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["NuITP: An Inductive Theorem Prover for Equational Program Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-8094","authenticated-orcid":false,"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[{"name":"University of M\u00e1laga, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4779-3848","authenticated-orcid":false,"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2994-6986","authenticated-orcid":false,"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Val\u00e8ncia, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,9,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"F. Baader and T. Nipkow. 1998. Term Rewriting and All That. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5122"},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 15th International Workshop on Rewriting Logic and its Applications (WRLA 2024)","author":"Bae K.","unstructured":"K. Bae, S. Escobar, R. L\u00f3pez-Rueda, J. Meseguer, and J. Sapi\u00f1a. 2024. Verifying Invariants by Deductive Model Checking. In Proceedings of the 15th International Workshop on Rewriting Logic and its Applications (WRLA 2024)(Lecture Notes in Computer Science). Springer. To appear."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881856"},{"key":"e_1_3_2_1_6_1","volume-title":"A Computational Logic Handbook","author":"Boyer R.S.","unstructured":"R.S. Boyer. 1998. A Mechanical Checking of a Theorem About a Card Trick. In A Computational Logic Handbook: Second Edition, R.\u00a0Boyer and J.\u00a0Moore (Eds.). Formal Methods Series, Vol.\u00a023. Academic Press, Inc."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.06.001"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"M. Clavel F. Dur\u00e1n S. Eker P. Lincoln N. Mart\u00ed-Oliet J. Meseguer and C. Talcott. 2007. All About Maude: A High-Performance Logical Framework. Lecture Notes in Computer Science Vol.\u00a04350. Springer. https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","unstructured":"M. Clavel F. Dur\u00e1n S. Eker and J. Meseguer. 2000. Building Equational Proving Tools by Reflection in Rewriting Logic. In CAFE: An Industrial-Strength Algebraic Formal Method K.\u00a0Futatsugi A.T. Nakagawa and T.\u00a0Tamai (Eds.). Elsevier Science 1\u201331. https:\/\/doi.org\/10.1016\/B978-0-444-50556-9.X5059-X","DOI":"10.1016\/B978-0-444-50556-9.X5059-X"},{"key":"e_1_3_2_1_10_1","unstructured":"M. Clavel and M. Palomino. 2005. The ITP Tool\u2019s Manual. Technical Report. Available at: http:\/\/maude.sip.ucm.es\/itp."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2875"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"R. Diaconescu and K. Futatsugi. 1998. CafeOBJ Report. AMAST Series in Computing Vol.\u00a06. World Scientific. https:\/\/doi.org\/10.1142\/3831","DOI":"10.1142\/3831"},{"key":"e_1_3_2_1_14_1","unstructured":"F. Dur\u00e1n S. Escobar J. Meseguer and J. Sapi\u00f1a. 2024. NuITP User\u2019s Manual. Technical Report. Available at: https:\/\/nuitp.webs.upv.es."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100887"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102893"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"D. G\u00e2in\u00e2 D. Lucanu K. Ogata and K. Futatsugi. 2014. On Automation of OTS\/CafeOBJ Method. In Specification Algebra and Software - Essays Dedicated to Kokichi Futatsugi (SAS 2014)(Lecture Notes in Computer Science Vol.\u00a08373). Springer 578\u2013602. https:\/\/doi.org\/10.1007\/978-3-642-54624-2_29","DOI":"10.1007\/978-3-642-54624-2_29"},{"key":"e_1_3_2_1_19_1","first-page":"60","article-title":"Magnetic Colors","volume":"38","author":"Gilbreath N.","year":"1958","unstructured":"N. Gilbreath. 1958. Magnetic Colors. The Linking Ring 38, 5 (1958), 60.","journal-title":"The Linking Ring"},{"key":"e_1_3_2_1_20_1","first-page":"272","article-title":"Gilbreath\u2019s Second Principle","volume":"46","author":"Gilbreath N.","year":"1966","unstructured":"N. Gilbreath. 1966. Gilbreath\u2019s Second Principle. The Linking Ring 46, 6 (1966), 272.","journal-title":"The Linking Ring"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10009-1_27"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-53162-9_27"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2101.02690v2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.07.003"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"e_1_3_2_1_28_1","volume-title":"Decision Procedures for Equationally Based Reasoning. Ph.\u00a0D. Dissertation","author":"Hendrix J.","unstructured":"J. Hendrix. 2008. Decision Procedures for Equationally Based Reasoning. Ph.\u00a0D. Dissertation. University of Illinois at Urbana-Champaign. Available at: https:\/\/hdl.handle.net\/2142\/11487."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_20"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","unstructured":"T. Hoare and N. Shankar. 2010. Unraveling a Card Trick. In Time for Verification - Essays in Memory of Amir Pnueli(Lecture Notes in Computer Science Vol.\u00a06200). Springer 195\u2013201. https:\/\/doi.org\/10.1007\/978-3-642-13754-9_10","DOI":"10.1007\/978-3-642-13754-9_10"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51081-8_138"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-64299-4_26"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_29"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.09.001"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100877"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65941-6_4"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2405.02420"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567461"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_21"},{"key":"e_1_3_2_1_43_1","unstructured":"A. Rubio. 1994. Automated Deduction with Constrained Clauses. Ph.\u00a0D. Dissertation. Universitat Polit\u00e8cnica de Catalunya."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.12.006"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1142\/3163"}],"event":{"name":"PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming","location":"Milano Italy","acronym":"PPDP 2024"},"container-title":["Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678232.3678236","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3678232.3678236","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:09Z","timestamp":1750287249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678232.3678236"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,9]]},"references-count":44,"alternative-id":["10.1145\/3678232.3678236","10.1145\/3678232"],"URL":"https:\/\/doi.org\/10.1145\/3678232.3678236","relation":{},"subject":[],"published":{"date-parts":[[2024,9,9]]},"assertion":[{"value":"2024-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}