{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T21:23:44Z","timestamp":1784150624287,"version":"3.55.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"National Science Foundation","award":["2242786"],"award-info":[{"award-number":["2242786"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,1,31]]},"abstract":"<jats:p>\n                    Equational problems are fundamental in computer science, frequently arising as subproblems across diverse domains, including program analysis and learning from examples and counterexamples. This article focuses on equational problems in languages with binding operators, formulating them within the nominal framework and referring to them as\n                    <jats:italic toggle=\"yes\">Nominal Equational Problems<\/jats:italic>\n                    . We provide a comprehensive definition of solutions for nominal equational problems and introduce a set of simplification rules for computing these solutions within the nominal ground term algebra. We rigorously prove that the simplification rules are\n                    <jats:italic toggle=\"yes\">sound<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">solution-preserving<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">complete<\/jats:italic>\n                    . Moreover, we establish that, under a specific strategy for rule application, the simplification process always terminates, thereby providing an effective algorithm for solving nominal equational problems. Finally, we demonstrate the practical relevance of our results by showcasing how nominal equational problems can serve as a framework for learning from examples and counterexamples. We also illustrate their applicability in addressing sufficient completeness problems, emphasising their utility in theoretical and practical contexts.\n                  <\/jats:p>","DOI":"10.1145\/3767744","type":"journal-article","created":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T16:39:01Z","timestamp":1758127141000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Nominal Approach to Equational Problems in Languages with Binders"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1959-8730","authenticated-orcid":false,"given":"Daniele","family":"Nantes-Sobrinho","sequence":"first","affiliation":[{"name":"Department of Mathematics, Universidade de Bras\u00edlia, Brazil and Department of Computing, Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8325-5815","authenticated-orcid":false,"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[{"name":"Informatics, King\u2019s College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1350-3478","authenticated-orcid":false,"given":"Deivid","family":"Vale","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Augusta University, Augusta, Georgia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0089-3905","authenticated-orcid":false,"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[{"name":"Departments of Mathematics and Computer Science, Universidade de Bras\u00edlia, Brasilia, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,11,17]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11558-0_40"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2014.01.006"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000050"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:19)2020"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_2"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-42753-4_4"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.02.002"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00277-0"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.FUTURE.2017.07.024"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2015.57"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507250"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JAL.2011.09.001"},{"key":"e_1_3_3_15_2","article-title":"An evaluation of duplicate code detection using anti-unification","author":"Bulychev Petr","year":"2009","unstructured":"Petr Bulychev and Marius Minea. 2009. An evaluation of duplicate code detection using anti-unification. In Proceedings of the 3rd International Workshop on Software Clones.","journal-title":"Proceedings of the 3rd International Workshop on Software Clones"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/179812.179813"},{"key":"e_1_3_3_17_2","unstructured":"William E. Byrd and Daniel P. Friedman. 2008. \\(\\alpha\\) Kanren A Fresh Name in Nominal Logic Programming. Technical Report. Indiana University Bloomington CS Dept. Retrieved from http:\/\/webyrd.net\/alphamk\/alphamk.pdf"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2008.05.012"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2020.10.020"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2023\/736"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1140641176"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27775-0_19"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2007.02.009"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16780-3_85"},{"key":"e_1_3_3_27_2","volume-title":"Unification et Disunification: Th\u00e9orie et Applications","author":"Comon Hubert","year":"1988","unstructured":"Hubert Comon. 1988. Unification et Disunification: Th\u00e9orie et Applications. Ph.D. Dissertation. Institut National Polytechnique de Grenoble, France."},{"key":"e_1_3_3_28_2","first-page":"322","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"Comon Hubert","year":"1991","unstructured":"Hubert Comon. 1991. Disunification: A survey. In Computational Logic: Essays in Honor of Alan Robinson. Jean-Louis Lassez and Gordon Plotkin (Eds.), MIT Press, 322\u2013359."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1994.1056"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55808-X_17"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"e_1_3_3_32_2","volume-title":"Introduction to Algorithms, Second Edition","author":"Cormen Thomas H.","year":"2001","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2001. Introduction to Algorithms, Second Edition. The MIT Press and McGraw-Hill Book Company."},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10994-021-06089-1"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10994-020-05934-Z"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10994-019-05862-7"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01189020"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0041"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1998.0203"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.34.5"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn055"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-007-0056-1"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp033"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_13"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_14"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01893885"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00292110"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54345-7_72"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76928-6_29"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243794"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0016848"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56503-5_51"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5132"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SAT.2023.15"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-12441-9_9"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89982-2_26"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v38i9.28938"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(03)00029-4"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"issue":"1","key":"e_1_3_3_66_2","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin Gordon D.","year":"1970","unstructured":"Gordon D. Plotkin. 1970. A note on inductive generalization. Machine Intelligence 5, 1 (1970), 153\u2013163.","journal-title":"Machine Intelligence"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632857"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.24963\/IJCAI.2022\/378"},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22102-7_23"},{"key":"e_1_3_3_70_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.7"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_26"},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2024.27"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704893"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3767744","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T12:59:55Z","timestamp":1763384395000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3767744"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,17]]},"references-count":75,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1,31]]}},"alternative-id":["10.1145\/3767744"],"URL":"https:\/\/doi.org\/10.1145\/3767744","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,17]]},"assertion":[{"value":"2025-01-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-22","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}