{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:40Z","timestamp":1778914180140,"version":"3.51.4"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319998398","type":"print"},{"value":"9783319998404","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99840-4_6","type":"book-chapter","created":{"date-parts":[[2018,9,7]],"date-time":"2018-09-07T11:29:08Z","timestamp":1536319748000},"page":"98-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Associative Unification and Symbolic Reasoning Modulo Associativity in Maude"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Eker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Narciso","family":"Mart\u00ed-Oliet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,8]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-55124-7_3","volume-title":"Word Equations and Related Topics","author":"H Abdulrab","year":"1992","unstructured":"Abdulrab, H.: Implementation of Makanin\u2019s algorithm. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 61\u201384. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55124-7_3"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-56730-5_35","volume-title":"Word Equations and Related Topics","author":"H Abdulrab","year":"1993","unstructured":"Abdulrab, H.: LOP: toward a new implementation of Makanin\u2019s algorithm. In: Abdulrab, H., P\u00e9cuchet, J.-P. (eds.) IWWERT 1991. LNCS, vol. 677, pp. 133\u2013149. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56730-5_35"},{"issue":"5","key":"6_CR3","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1016\/S0747-7171(89)80056-2","volume":"8","author":"H Abdulrab","year":"1989","unstructured":"Abdulrab, H., P\u00e9cuchet, J.-P.: Solving word equations. J. Symbolic Comput. 8(5), 499\u2013521 (1989)","journal-title":"J. Symbolic Comput."},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63139-4_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M Alpuente","year":"2017","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Partial evaluation of order-sorted equational programs modulo axioms. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 3\u201320. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63139-4_1"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y Auffray","year":"1992","unstructured":"Auffray, Y., Enjalbert, P.: Modal theorem proving: an equational viewpoint. J. Logic Comput. 2(3), 247\u2013295 (1992)","journal-title":"J. Logic Comput."},{"key":"6_CR6","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, 24\u201326 June 2013, Eindhoven, The Netherlands, vol. 21. LIPIcs, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/10705424_6","volume-title":"Functional and Logic Programming","author":"R Caballero","year":"1999","unstructured":"Caballero, R., L\u00f3pez-Fraguas, F.J.: A functional-logic perspective of parsing. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 85\u201399. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/10705424_6"},{"key":"6_CR8","unstructured":"Clavel, M., et al.: Maude Manual (Version 2.7.1) (2016). http:\/\/maude.cs.illinois.edu"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-02348-4_27","volume-title":"Rewriting Techniques and Applications","author":"M Clavel","year":"2009","unstructured":"Clavel, M., et al.: Unification and narrowing in Maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 380\u2013390. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_27"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-662-54455-6_6","volume-title":"Principles of Security and Trust","author":"J Dreier","year":"2017","unstructured":"Dreier, J., Dum\u00e9nil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117\u2013140. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_6"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-40229-1_13","volume-title":"Automated Reasoning","author":"F Dur\u00e1n","year":"2016","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Built-in variant generation and unification, and their applications in Maude 2.7. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 183\u2013192. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_13"},{"key":"6_CR14","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Meseguer, J., Talcott, C.L.: Variants, unification, narrowing, and symbolic reachability in Maude 2.6. In: Schmidt-Schau\u00df, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, 30 May\u20131 June 2011, Novi Sad, Serbia, vol. 10. LIPIcs, pp. 31\u201340. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"Frontiers of Combining Systems","author":"F Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 246\u2013262. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_15"},{"issue":"7\u20138","key":"6_CR16","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Logic Algebraic Program. 81(7\u20138), 816\u2013850 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-56730-5_32","volume-title":"Word Equations and Related Topics","author":"P Enjalbcrt","year":"1993","unstructured":"Enjalbcrt, P., Clerin-Debart, F.\u00c7.: A case of termination for associative unification. In: Abdulrab, H., P\u00e9cuchet, J.-P. (eds.) IWWERT 1991. LNCS, vol. 677, pp. 79\u201389. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56730-5_32"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-73449-9_13","volume-title":"Term Rewriting and Applications","author":"S Escobar","year":"2007","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153\u2013168. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_13"},{"key":"6_CR20","unstructured":"Escobar, S., Meseguer, J., Meadows, C.: Maude-NPA manual v3.1 (2017). http:\/\/maude.cs.illinois.edu\/w\/index.php?title=Maude_Tools:_Maude-NPA"},{"issue":"7\u20138","key":"6_CR21","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Logic Algebraic Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"6_CR22","unstructured":"Goguen, J., Meseguer, J.: EQLOG: equality, types and generic modules for logic programming. In: DeGroot, D., Lindstrom, G. (eds.) Logic Programming, Functions, Relations and Equations, pp. 295\u2013363. Prentice-Hall (1986)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Guti\u00e9rrez, C.: Satisfiability of word equations with constants is in exponential space. In: Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1998), pp. 112\u2013119. IEEE Computer Society Press (1998)","DOI":"10.1109\/SFCS.1998.743434"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/BFb0054336","volume-title":"LATIN\u201998: Theoretical Informatics","author":"C Guti\u00e9rrez","year":"1998","unstructured":"Guti\u00e9rrez, C.: Solving equations in strings: on Makanin\u2019s algorithm. In: Lucchesi, C.L., Moura, A.V. (eds.) LATIN 1998. LNCS, vol. 1380, pp. 358\u2013373. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054336"},{"key":"6_CR25","unstructured":"Hmelevskii, J.I.: Equations in free semigroups. Number 107 in Proceedings of the Steklov Institute of Mathematics, Moscow (1971)"},{"issue":"1","key":"6_CR26","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/78935.78938","volume":"37","author":"J Jaffa","year":"1990","unstructured":"Jaffa, J.: Minimal and complete word unification. J. ACM 37(1), 47\u201385 (1990)","journal-title":"J. ACM"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Lothaire, M.: Algebraic Combinatorics on Words. Number 90 in Encyclopedia of Mathematics and its Applications. Cambridge University Press (2002)","DOI":"10.1017\/CBO9781107326019"},{"issue":"2","key":"6_CR28","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"GS Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii USSR Sbornik 32(2), 129\u2013198 (1977)","journal-title":"Matematicheskii USSR Sbornik"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0013826","volume-title":"Algebraic and Logic Programming","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 158\u2013200. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0013826"},{"key":"6_CR31","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-29510-7_1","volume-title":"Formal Techniques for Safety-Critical Systems","author":"J Meseguer","year":"2016","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 3\u201334. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29510-7_1"},{"issue":"1\u20132","key":"6_CR32","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"Higher-Order Symbolic Comput."},{"issue":"3","key":"6_CR33","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W Plandowski","year":"2004","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3), 483\u2013496 (2004)","journal-title":"J. ACM"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the Thirty-eighth Annual ACM Symposium on Theory of Computing (STOC 2006), pp. 467\u2013476. ACM, New York (2007)","DOI":"10.1145\/1132516.1132584"},{"key":"6_CR35","first-page":"73","volume":"7","author":"GD Plotkin","year":"1972","unstructured":"Plotkin, G.D.: Building in equational theories. Mach. Intell. 7, 73\u201390 (1972)","journal-title":"Mach. Intell."},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-07151-0_4","volume-title":"Functional and Logic Programming","author":"A Riesco","year":"2014","unstructured":"Riesco, A.: Using big-step and small-step semantics in maude to perform declarative debugging. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 52\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07151-0_4"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-13977-2_12","volume-title":"Tests and Proofs","author":"V Rusu","year":"2010","unstructured":"Rusu, V.: Combining theorem proving and narrowing for rewriting-logic specifications. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 135\u2013150. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13977-2_12"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/BFb0052364","volume-title":"Rewriting Techniques and Applications","author":"RA Schmidt","year":"1998","unstructured":"Schmidt, R.A.: E-unification for subsystems of S4. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 106\u2013120. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0052364"},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-55124-7_4","volume-title":"Word Equations and Related Topics","author":"KU Schulz","year":"1992","unstructured":"Schulz, K.U.: Makanin\u2019s algorithm for word equations-two improvements and a generalization. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 85\u2013150. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55124-7_4"},{"issue":"2","key":"6_CR40","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF00881904","volume":"11","author":"KU Schulz","year":"1993","unstructured":"Schulz, K.U.: Word unification and transformation of generalized equations. J. Autom. Reasoning 11(2), 149\u2013184 (1993)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR41","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2014.02.005","volume":"99","author":"E Tushkanova","year":"2015","unstructured":"Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. Sci. Comput. Program. 99, 3\u201323 (2015)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99840-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T23:47:56Z","timestamp":1751845676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99840-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319998398","9783319998404"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99840-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}