{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:11Z","timestamp":1765617731557,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","funder":[{"name":"JSPS KAKENHI","award":["JP24K14817, and JP24K02900"],"award-info":[{"award-number":["JP24K14817, and JP24K02900"]}]},{"name":"FWF (Austrian Science Fund) project","award":["I~5943-N"],"award-info":[{"award-number":["I~5943-N"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756916","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-0015-5954","authenticated-orcid":false,"given":"Kanta","family":"Takahata","sequence":"first","affiliation":[{"name":"Niigata University, Niigata, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5908-8519","authenticated-orcid":false,"given":"Jonas","family":"Sch\u00f6pf","sequence":"additional","affiliation":[{"name":"University of Innsbruck, Innsbruck, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8697-4970","authenticated-orcid":false,"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[{"name":"Nagoya University, Nagoya, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0027-0759","authenticated-orcid":false,"given":"Takahito","family":"Aoto","sequence":"additional","affiliation":[{"name":"Niigata University, Niigata, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2024.31"},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/505863.505888"},{"key":"e_1_3_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Carsten Fuhs Cynthia Kop and Naoki Nishida. 2017. Verifying Procedural Programs via Constrained Rewriting Induction. ACM Transactions on Computational Logic 18 2 (2017) 14:1\u201314:50. 10.1145\/3060143","DOI":"10.1145\/3060143"},{"key":"e_1_3_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Misaki Kojima Naoki Nishida and Yutaka Matsubara. 2025. Transforming concurrent programs with semaphores into logically constrained term rewrite systems. Journal of Logical and Algebraic Methods in Programming 143 (2025) 1\u201323. 10.1016\/j.jlamp.2024.101033","DOI":"10.1016\/j.jlamp.2024.101033"},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Cynthia Kop. 2016. Termination of LCTRSs. CoRR abs\/1601.03206 (2016) 1\u20135. 10.48550\/ARXIV.1601.03206","DOI":"10.48550\/ARXIV.1601.03206"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Cynthia Kop. 2017. Quasi-reductivity of Logically Constrained Term Rewriting Systems. CoRR abs\/1702.02397 (2017) 1\u20138. 10.48550\/arXiv.1702.02397","DOI":"10.48550\/arXiv.1702.02397"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40885-4_24"},{"key":"e_1_3_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_18"},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_38"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_18"},{"key":"e_1_3_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"e_1_3_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Camilo Rocha Jos\u00e9 Meseguer and C\u00e9sar\u00a0A. Mu\u00f1oz. 2017. Rewriting modulo SMT and open system analysis. Journal of Logic and Algebraic Programming 86 1 (2017) 269\u2013297. 10.1016\/J.JLAMP.2016.10.001","DOI":"10.1016\/J.JLAMP.2016.10.001"},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-827"},{"key":"e_1_3_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90643-5_7"},{"key":"e_1_3_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63501-416"},{"key":"e_1_3_3_2_17_2","series-title":"(Lecture Notes in Computer Science)","volume-title":"Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation","author":"Takahata Kanta","year":"2025","unstructured":"Kanta Takahata, Jonas Sch\u00f6pf, Naoki Nishida, and Takahito Aoto. 2025. Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms. In Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation(Lecture Notes in Computer Science), Santiago Escobar and Laura Titolo (Eds.). Springer. to appear."},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Kanta Takahata Jonas Sch\u00f6pf Naoki Nishida and Takahito Aoto. 2025. Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version). CoRR abs\/2507.09326 (2025) 1\u201315. 10.48550\/arXiv.2507.09326","DOI":"10.48550\/arXiv.2507.09326"},{"key":"e_1_3_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.30"},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_2"}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:20Z","timestamp":1765617560000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756916"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":19,"alternative-id":["10.1145\/3756907.3756916","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756916","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}