{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:02:47Z","timestamp":1776553367296,"version":"3.51.2"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,11,14]],"date-time":"2024-11-14T00:00:00Z","timestamp":1731542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,14]],"date-time":"2024-11-14T00:00:00Z","timestamp":1731542400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["409003\/21-2"],"award-info":[{"award-number":["409003\/21-2"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Funda\u00e7\u00e3o de Amparo \u00e0 Pesquisa do Distrito Federal, Brazil","award":["00193-00001175\/2021-11"],"award-info":[{"award-number":["00193-00001175\/2021-11"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10817-024-09714-5","type":"journal-article","created":{"date-parts":[[2024,11,14]],"date-time":"2024-11-14T12:49:46Z","timestamp":1731588586000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Certified First-Order AC-Unification and Applications"],"prefix":"10.1007","volume":"68","author":[{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Ferreira Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Temur","family":"Kutsia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniele","family":"Nantes-Sobrinho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,14]]},"reference":[{"issue":"1","key":"9714_CR1","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0747-7171(92)90025-Y","volume":"14","author":"M Adi","year":"1992","unstructured":"Adi, M., Kirchner, C.: AC-unification race: the system solving approach, implementation and benchmarks. J. Sym. Comput. 14(1), 51\u201370 (1992)","journal-title":"J. Sym. Comput."},{"key":"9714_CR2","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Nantes-Sobrinho, D.: A certified algorithm for AC-unification. In: 7th international conference on formal structures for computation and deduction, FSCD, Volume 228 of LIPIcs, pp. 8:1\u20138:21. Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022)"},{"key":"9714_CR3","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Nantes-Sobrinho, D.: Nominal narrowing. In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, p.\u00a011. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"9714_CR4","first-page":"57","volume":"323","author":"M Ayala-Rinc\u00f3n","year":"2016","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Rocha-Oliveira, A.C.: Completeness in PVS of a nominal unification algorithm. ENTCS 323, 57\u201374 (2016)","journal-title":"ENTCS"},{"key":"9714_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2019.02.020","volume":"781","author":"M Ayala-Rinc\u00f3n","year":"2019","unstructured":"Ayala-Rinc\u00f3n, M., de Carvalho-Segundo, W., Fern\u00e1ndez, M., Nantes-Sobrinho, D., Rocha-Oliveira, A.C.: A formalisation of nominal $$\\alpha $$-equivalence with A, C, and AC function symbols. Theor. Comput. Sci. 781, 3\u201323 (2019)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9714_CR6","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1017\/S0960129521000050","volume":"31","author":"M Ayala-Rinc\u00f3n","year":"2021","unstructured":"Ayala-Rinc\u00f3n, M., de Carvalho-Segundo, W., Fern\u00e1ndez, M., Silva, G.F., Nantes-Sobrinho, D.: Formalising nominal C-unification generalised with protected variables. Math. Struct. Comput. Sci. 31(3), 286\u2013311 (2021)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"9714_CR7","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1017\/S0960129521000050","volume":"31","author":"M Ayala-Rinc\u00f3n","year":"2021","unstructured":"Ayala-Rinc\u00f3n, M., de Carvalho-Segundo, W., Fern\u00e1ndez, M., Silva, G.F., Nantes-Sobrinho, D.: Formalising nominal C-unification generalised with protected variables. Math. Struct. Comput. Sci. 31(3), 286\u2013311 (2021)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9714_CR8","doi-asserted-by":"crossref","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Silva, G.F., Kutsia, T., Nantes-Sobrinho, D.: Nominal AC-matching. In: 16th International Conference on Intelligent Computer Mathematics CICM. Volume 14101 of LNCS, pp. 53\u201368. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-42753-4_4"},{"key":"9714_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"1\/2","key":"9714_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0747-7171(87)80027-5","volume":"3","author":"D Benanav","year":"1987","unstructured":"Benanav, D., Kapur, D., Narendran, P.: Complexity of matching problems. J. Sym. Comput. 3(1\/2), 203\u2013216 (1987)","journal-title":"J. Sym. Comput."},{"key":"9714_CR11","doi-asserted-by":"crossref","unstructured":"Boudet, A., Contejean, E., Devie, H.: A new AC unification algorithm with an algorithm for solving systems of diophantine equations. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS \u201990), pp. 289\u2013299. IEEE Computer Society, Washington (1990)","DOI":"10.1109\/LICS.1990.113755"},{"issue":"2","key":"9714_CR12","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BF00881905","volume":"11","author":"A Boudet","year":"1993","unstructured":"Boudet, A.: Competing for the AC-unification race. J. Autom. Reason. 11(2), 185\u2013212 (1993)","journal-title":"J. Autom. Reason."},{"key":"9714_CR13","doi-asserted-by":"crossref","unstructured":"Cheney, J., Urban, C.: Alpha-Prolog: a logic programming language with names, binding and $$\\alpha $$-equivalence. In: Logic Programming, 20th International Conference, ICLP 2004, Volume 3132 of LNCS, pp. 269\u2013283. Springer (2004)","DOI":"10.1007\/978-3-540-27775-0_19"},{"issue":"1\u20132","key":"9714_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0747-7171(89)80025-2","volume":"8","author":"M Clausen","year":"1989","unstructured":"Clausen, M., Fortenbacher, A.: Efficient solution of linear diophantine equations. J. Sym. Comput. 8(1\u20132), 201\u2013216 (1989)","journal-title":"J. Sym. Comput."},{"key":"9714_CR15","doi-asserted-by":"crossref","unstructured":"Contejean, E.: A certified AC matching algorithm. In: Rewriting Techniques and Applications. 15th International Conference, RTA 2004, Aachen, Germany, June 3\u20135, 2004, Proceedings, Volume 3091 of LNCS, pp. 70\u201384. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-25979-4_5"},{"key":"9714_CR16","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description). In: 11th International Joint Conference on Automated Reasoning IJCAR. Volume 13385 of LNCS, pp. 529\u2013540. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-10769-6_31"},{"key":"9714_CR17","doi-asserted-by":"crossref","unstructured":"Fages, F.: Associative-commutative unification. In: Proceedings 7th International Conference on Automated Deduction CADE. Volume 170 of LNCS, pp. 194\u2013208. Springer, Heidelberg (1984)","DOI":"10.1007\/978-0-387-34768-4_12"},{"issue":"3","key":"9714_CR18","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0747-7171(87)80004-4","volume":"3","author":"F Fages","year":"1987","unstructured":"Fages, F.: Associative-commutative unification. J. Sym. Comput. 3(3), 257\u2013275 (1987)","journal-title":"J. Sym. Comput."},{"issue":"6","key":"9714_CR19","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","volume":"205","author":"M Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.: Nominal rewriting. Inf. Comput. 205(6), 917\u2013965 (2007)","journal-title":"Inf. Comput."},{"key":"9714_CR20","unstructured":"Ferreira-Silva, G.: Towards nominal AC-unification. Ph.D Thesis, University of Brasilia (UnB) (2024)"},{"key":"9714_CR21","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Computational Logic\u2014Essays in Honor of Alan Robinson, pp. 257\u2013321. The MIT Press, Cambridge (1991)","DOI":"10.1016\/0743-1066(92)90027-Z"},{"key":"9714_CR22","doi-asserted-by":"crossref","unstructured":"Kapur, D., Narendran, P.: Double-exponential complexity of computing a complete set of AC-unifiers. In: Proceedings of 7th Annual Symposium on Logic in Computer Science (LICS), pp. 11\u201321. IEEE Computer Society, Washington (1992)","DOI":"10.1109\/LICS.1992.185515"},{"key":"9714_CR23","doi-asserted-by":"crossref","unstructured":"Kumar, R., Norrish, M.: (Nominal) unification by recursive descent with triangular substitutions. In: 1st International Conference on Interactive Theorem Proving ITP. Volume 6172 of LNCS, pp. 51\u201366. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14052-5_6"},{"issue":"7","key":"9714_CR24","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L Lamport","year":"1995","unstructured":"Lamport, L.: How to write a proof. Am. Math. Mon. 102(7), 600\u2013608 (1995)","journal-title":"Am. Math. Mon."},{"issue":"1","key":"9714_CR25","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","volume":"11","author":"L Lamport","year":"2012","unstructured":"Lamport, L.: How to write a 21st century proof. J. Fixed Point Theory appl. 11(1), 43\u201363 (2012)","journal-title":"J. Fixed Point Theory appl."},{"key":"9714_CR26","doi-asserted-by":"crossref","unstructured":"Me\u00dfner, F., Parsert, J., Sch\u00f6pf, J., Sternagel, C.: A formally verified solver for homogeneous linear diophantine equations. In: Interactive theorem proving\u20139th international conference. ITP, Volume 10895 of LNCS, pp. 441\u2013458. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-94821-8_26"},{"key":"9714_CR27","unstructured":"Mu\u00f1oz, C., Butler, R.: Rapid prototyping in PVS. Technical Report NASA\/CR-2003-212418, NIA-2003-03, NASA Langley Research Center (NIA) (2003)"},{"key":"9714_CR28","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Automated Deduction\u2013CADE-11. 11th International Conference on Automated Deduction, Volume 607 of LNCS, pp. 748\u2013752. Springer, Berlin, Heidelberg (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9714_CR29","volume-title":"PVS language reference","author":"S Owre","year":"2000","unstructured":"Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS language reference. Technical report, Computer Science Laboratory, SRI International, Menlo Park (2000)"},{"key":"9714_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673","volume-title":"Nominal Sets: Names and Symmetry in Computer Science","author":"AM Pitts","year":"2013","unstructured":"Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2013)"},{"key":"9714_CR31","doi-asserted-by":"crossref","unstructured":"Stickel, M.E.: A complete unification algorithm for associative-commutative functions. In: Advance Papers of the Fourth International Joint Conference on Artificial Intelligence, pp. 71\u201376 (1975)","DOI":"10.21236\/ADA015846"},{"issue":"3","key":"9714_CR32","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"ME Stickel","year":"1981","unstructured":"Stickel, M.E.: A unification algorithm for associative-commutative functions. J. ACM 28(3), 423\u2013434 (1981)","journal-title":"J. ACM"},{"issue":"1\u20133","key":"9714_CR33","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C Urban","year":"2004","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.: Nominal unification. Theor. Comput. Sci. 323(1\u20133), 473\u2013497 (2004)","journal-title":"Theor. Comput. Sci."}],"updated-by":[{"DOI":"10.1007\/s10817-024-09715-4","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T00:00:00Z","timestamp":1739836800000}}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09714-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09714-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09714-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T11:16:55Z","timestamp":1739877415000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09714-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,14]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["9714"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09714-5","relation":{"correction":[{"id-type":"doi","id":"10.1007\/s10817-024-09715-4","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,14]]},"assertion":[{"value":"16 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 November 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2025","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10817-024-09715-4","URL":"https:\/\/doi.org\/10.1007\/s10817-024-09715-4","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no Conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to Participate"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for Publication"}}],"article-number":"25"}}