{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:21:04Z","timestamp":1770286864950,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030719944","type":"print"},{"value":"9783030719951","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We define <jats:italic>nominal equational problems<\/jats:italic> of the form <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\exists \\overline{W} \\forall \\overline{Y} : P$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>\u2203<\/mml:mo>\n                    <mml:mover>\n                      <mml:mrow>\n                        <mml:mi>W<\/mml:mi>\n                      <\/mml:mrow>\n                      <mml:mrow>\n                        <mml:mo>\u00af<\/mml:mo>\n                      <\/mml:mrow>\n                    <\/mml:mover>\n                    <mml:mo>\u2200<\/mml:mo>\n                    <mml:mover>\n                      <mml:mrow>\n                        <mml:mi>Y<\/mml:mi>\n                      <\/mml:mrow>\n                      <mml:mrow>\n                        <mml:mo>\u00af<\/mml:mo>\n                      <\/mml:mrow>\n                    <\/mml:mover>\n                    <mml:mo>:<\/mml:mo>\n                    <mml:mi>P<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, where <jats:inline-formula><jats:alternatives><jats:tex-math>$$P$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>P<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> consists of conjunctions and disjunctions of equations <jats:inline-formula><jats:alternatives><jats:tex-math>$$s\\approx _\\alpha t$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>s<\/mml:mi>\n                    <mml:msub>\n                      <mml:mo>\u2248<\/mml:mo>\n                      <mml:mi>\u03b1<\/mml:mi>\n                    <\/mml:msub>\n                    <mml:mi>t<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, freshness constraints <jats:inline-formula><jats:alternatives><jats:tex-math>$$a\\#t$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>a<\/mml:mi>\n                    <mml:mo>#<\/mml:mo>\n                    <mml:mi>t<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and their negations: <jats:inline-formula><jats:alternatives><jats:tex-math>$$s \\not \\approx _\\alpha t$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>s<\/mml:mi>\n                    <mml:msub>\n                      <mml:mo>\u2249<\/mml:mo>\n                      <mml:mi>\u03b1<\/mml:mi>\n                    <\/mml:msub>\n                    <mml:mi>t<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and \"Equation missing\", where <jats:inline-formula><jats:alternatives><jats:tex-math>$$a$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>a<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is an atom and <jats:inline-formula><jats:alternatives><jats:tex-math>$$s, t$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>s<\/mml:mi>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>t<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\alpha $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03b1<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-equality) is decidable.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_2","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"22-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Nominal Equational Problems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0089-3905","authenticated-orcid":false,"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8325-5815","authenticated-orcid":false,"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1959-8730","authenticated-orcid":false,"given":"Daniele","family":"Nantes-Sobrinho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1350-3478","authenticated-orcid":false,"given":"Deivid","family":"Vale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Nantes-Sobrinho, D., Vale, D.: On Solving Nominal Disunification Constraints. ENTCS 348, 3 \u2013 22 (2020). https:\/\/doi.org\/10.1016\/j.entcs.2020.02.002, proc. 14th Int. Workshop on Logical and Semantic Frameworks, with Applications LSFA 2019","DOI":"10.1016\/j.entcs.2020.02.002"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229\u2013255 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00277-0.","DOI":"10.1016\/0304-3975(94)00277-0"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Buntine, W.L., B\u00fcrckert, H.J.: On solving equations and disequations. J. ACM 41(4), 591\u2013629 (Jul 1994). https:\/\/doi.org\/10.1145\/179812.179813","DOI":"10.1145\/179812.179813"},{"key":"2_CR4","unstructured":"Byrd, W.E., Friedman, D.P.: $$\\alpha $$Kanren A Fresh Name in Nominal Logic Programming (2008), http:\/\/webyrd.net\/alphamk\/alphamk.pdf, earlier version available in the Proc. 2007 Workshop on Scheme and Functional Programming, Universit\u00e9 Laval Technical Report DIUL-RT-0701"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: Matching and alpha-equivalence check for nominal terms. Journal of Computer and System Sciences 76(5), 283 \u2013 301 (2010). https:\/\/doi.org\/10.1016\/j.jcss.2009.10.003","DOI":"10.1016\/j.jcss.2009.10.003"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Cheney, J., Urban, C.: $$\\alpha $$Prolog: A Logic Programming Language with Names, Binding and $$\\alpha $$-Equivalence. In: Proc. 20th International Conference on Logic Programming ICLP. LNCS, vol.\u00a03132, pp. 269\u2013283. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27775-0_19","DOI":"10.1007\/978-3-540-27775-0_19"},{"key":"2_CR7","unstructured":"Comon, H.: Unification et disunification: Th\u00e9orie et applications. Ph.D. thesis, Institut National Polytechnique de Grenoble, France (1988)"},{"key":"2_CR8","unstructured":"Comon, H.: Disunification: a Survey. In: Lassez, J.L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 322\u2013359. MIT Press (1991)"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Comon, H., Fern\u00e1ndez, M.: Negation elimination in equational formulae. In: Proc. 17th International Symposium on Mathematical Foundations of Computer Science MFCS. LNCS, vol.\u00a0629, pp. 191\u2013199. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55808-X_17","DOI":"10.1007\/3-540-55808-X_17"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. J. Symb. Comput. 7(3\/4), 371\u2013425 (1989). https:\/\/doi.org\/10.1016\/S0747-7171(89)80017-3","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M.: Narrowing based procedures for equational disunification. Appl. Algebra Eng. Commun. Comput. 3, 1\u201326 (1992). https:\/\/doi.org\/10.1007\/BF01189020","DOI":"10.1007\/BF01189020"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M.: AC complement problems: Satisfiability and negation elimination. Journal of Symbolic Computation 22(1), 49\u201382 (1996). https:\/\/doi.org\/10.1006\/jsco.1996.0041","DOI":"10.1006\/jsco.1996.0041"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M.: Negation elimination in empty or permutative theories. Journal of Symbolic Computation 26(1), 97\u2013133 (1998). https:\/\/doi.org\/10.1006\/jsco.1998.0203","DOI":"10.1006\/jsco.1998.0203"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Nominal rewriting. Information and Computation 205(6), 917 \u2013 965 (2007). https:\/\/doi.org\/10.1016\/j.ic.2006.12.002","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Gabbay, M.J., Mathijssen, A.: Nominal (Universal) algebra: equational logic with names and binding. J. of Logic and Computation 19(6), 1455\u20131508 (2009). https:\/\/doi.org\/10.1093\/logcom\/exp033","DOI":"10.1093\/logcom\/exp033"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Kounalis, E., Lugiez, D., Pottier, L.: A Solution of the Complement Problem in Associative-Commutative Theories. In: Proc. 16th International Symposium on Mathematical Foundations of Computer Science MFCS. LNCS, vol. 520, pp. 287\u2013297. Springer (1991). https:\/\/doi.org\/10.1007\/3-540-54345-7_72.","DOI":"10.1007\/3-540-54345-7_72"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Levy, J., Villaret, M.: An efficient nominal unification algorithm. In: Proc. of the 21st International Conference on Rewriting Techniques and Applications, RTA. LIPIcs, vol.\u00a06, pp. 209\u2013226 (2010). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2010.209","DOI":"10.4230\/LIPIcs.RTA.2010.209"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Lugiez, D.: Higher order disunification: Some decidable cases. In: First International Conference on Constraints in Computational Logics, CCL. LNCS, vol.\u00a0845, pp. 121\u2013135. Springer (1994). https:\/\/doi.org\/10.1007\/BFb0016848","DOI":"10.1007\/BFb0016848"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Lugiez, D., Moysset, J.L.: Complement problems and tree automata in AC-like theories (extended abstract). In: Proc. 10th Annual Symposium on Theoretical Aspects of Computer Science STACS. LNCS, vol.\u00a0665, pp. 515\u2013524. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-56503-5_51","DOI":"10.1007\/3-540-56503-5_51"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Near, J.P., Byrd, W.E., Friedman, D.P.: $$\\alpha $$leanTAP: A Declarative Theorem Prover for First-Order Classical Logic. In: Proc. 24th International Conference on Logic Programming ICLP. LNCS, vol.\u00a05366, pp. 238\u2013252. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89982-2_26","DOI":"10.1007\/978-3-540-89982-2_26"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press (2013). https:\/\/doi.org\/10.1017\/CBO9781139084673","DOI":"10.1017\/CBO9781139084673"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Ravishankar, V., Cornell, K.A., Narendran, P.: Asymmetric Unification and Disunification. In: Description Logic, Theory Combination, and All That. vol. 11560 (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_23","DOI":"10.1007\/978-3-030-22102-7_23"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.: Nominal unification. Theor. Comput. Sci. 323(1-3), 473\u2013497 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2004.06.016","DOI":"10.1016\/j.tcs.2004.06.016"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:58Z","timestamp":1616432638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"88","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}