{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T18:40:47Z","timestamp":1791484847783,"version":"4.3.4"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030684457","type":"print"},{"value":"9783030684464","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":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","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":[[2021]]},"DOI":"10.1007\/978-3-030-68446-4_1","type":"book-chapter","created":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T19:06:39Z","timestamp":1613156799000},"page":"3-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Computation in Maude: Some Tapas"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,2,13]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.3233\/FI-2020-1991","volume":"177","author":"M Alpuente","year":"2020","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: Order-sorted homeomorphic embedding modulo combinations of associativity and\/or commutativity axioms. Fundamenta Informaticae 177, 297\u2013329 (2020)","journal-title":"Fundamenta Informaticae"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-030-19570-0_11","volume-title":"Logics in Artificial Intelligence","author":"M Alpuente","year":"2019","unstructured":"Alpuente, M., Ballis, D., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: $$ACUOS^{2}$$: a high-performance system for modular ACU generalization with subtyping and inheritance. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 171\u2013181. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-19570-0_11"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"100501","DOI":"10.1016\/j.jlamp.2019.100501","volume":"110","author":"M Alpuente","year":"2020","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110, 100501 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.ic.2014.01.006","volume":"235","author":"M Alpuente","year":"2014","unstructured":"Alpuente, M., Escobar, S., Espert, J., Meseguer, J.: A modular order-sorted equational generalization algorithm. Inf. Comput. 235, 98\u2013136 (2014)","journal-title":"Inf. Comput."},{"key":"1_CR5","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (1999)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Siekmann, J.H.: Unification theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 41\u2013126. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198537465.003.0002"},{"key":"1_CR7","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-40885-4_23","volume-title":"Frontiers of Combining Systems","author":"C Bouchard","year":"2013","unstructured":"Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 327\u2013342. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_23"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236, 35\u2013132 (2000)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"1_CR10","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.scico.2015.06.001","volume":"112","author":"A Cholewa","year":"2015","unstructured":"Cholewa, A., Escobar, S., Meseguer, J.: Constrained narrowing for conditional equational theories modulo axioms. Sci. Comput. Program. 112, 24\u201357 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1_CR12","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Department University of Illinois at Urbana-Champaign, February 2014. http:\/\/hdl.handle.net\/2142\/47117"},{"key":"1_CR13","unstructured":"Ciobaca., S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011)"},{"key":"1_CR14","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":"1_CR15","unstructured":"Clavel, M., et al.: Maude Manual (Version 3.1), October 2020. http:\/\/maude.cs.uiuc.edu"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.12.009","volume":"373","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. Theor. Comput. Sci. 373, 70\u201391 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR17","unstructured":"Comon, H.: Unification et disunification: Th\u00e9orie et applications. Ph.D. thesis, Institute National Polytechnique de Grenoble, France (1988)"},{"key":"1_CR18","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":"1_CR19","unstructured":"CVC4: https:\/\/cvc4.github.io"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebr. Meth. Program. 110 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100497","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-99840-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F Dur\u00e1n","year":"2018","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Associative unification and symbolic reasoning modulo associativity in Maude. In: Rusu, V. (ed.) WRLA 2018. LNCS, vol. 11152, pp. 98\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_6"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-71070-7_27","volume-title":"Automated Reasoning","author":"F Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: MTT: the Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313\u2013319. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_27"},{"key":"1_CR23","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"},{"key":"1_CR24","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. Algebraic Log. Program. 81, 816\u2013850 (2012)","journal-title":"J. Algebraic Log. Program."},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-24933-4_15","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"S Eker","year":"2011","unstructured":"Eker, S.: Fast sort computations for order-sorted matching and unification. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 299\u2013314. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24933-4_15"},{"key":"1_CR26","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":"1_CR27","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. Algebraic Log. Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Log. Program."},{"key":"1_CR28","unstructured":"Fay, M.: First-order unification in an equational theory. In: Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, pp. 161\u2013167 (1979)"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-319-94460-9_18","volume-title":"Logic-Based Program Synthesis and Transformation","author":"R Guti\u00e9rrez","year":"2018","unstructured":"Guti\u00e9rrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 306\u2013322. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94460-9_18"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2012.11.010","volume":"290","author":"J Hendrix","year":"2012","unstructured":"Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electr. Notes Theor. Comput. Sci. 290, 37\u201350 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151\u2013155. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_14"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Herbrand, J.: Logical Writings. Reidel (1971)","DOI":"10.1007\/978-94-010-3072-4"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980","author":"J-M Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 318\u2013334. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_25"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J-P Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361\u2013373. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/BFb0036921"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 257\u2013321. MIT Press (1991)","DOI":"10.1016\/0743-1066(92)90027-Z"},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"JP Jouannaud","year":"1986","unstructured":"Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"issue":"7","key":"1_CR38","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"1_CR39","unstructured":"Lankford, D.S.: Canonical inference. Technical report ATP-32, Southwestn University (1975)"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/3-540-07389-2_211","volume-title":"Mathematical Foundations of Computer Science 1975 4th Symposium, Mari\u00e1nsk\u00e9 L\u00e1zn\u011b, September 1\u20135, 1975","author":"G Levi","year":"1975","unstructured":"Levi, G., Sirovich, F.: Proving program properties, symbolic evaluation and logical procedural semantics. In: Be\u010dv\u00e1\u0159, J. (ed.) MFCS 1975. LNCS, vol. 32, pp. 294\u2013301. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07389-2_211"},{"issue":"1","key":"1_CR41","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","volume":"85","author":"S Lucas","year":"2016","unstructured":"Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Meth. Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"2","key":"1_CR42","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. Math. USSR Sbornik 32(2), 129\u2013198 (1977)","journal-title":"Math. USSR Sbornik"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn, pp. 1\u201387. Kluwer Academic Publishers (2002). first published as SRI Technical report SRI-CSL-93-05, August 1993","DOI":"10.1007\/978-94-017-0464-9_1"},{"key":"1_CR44","volume-title":"Hilbert\u2019s 10th Problem","author":"YV Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s 10th Problem. MIT Press, Cambridge (1993)"},{"key":"1_CR45","volume-title":"LISP 1.5 Programmer\u2019s Manual","author":"J McCarthy","year":"1985","unstructured":"McCarthy, J., Abrahams, P., Edwards, D., Hart, T., Levin, M.: LISP 1.5 Programmer\u2019s Manual. MIT Press, Cambridge (1985)"},{"key":"1_CR46","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":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-04164-8_4","volume-title":"Semantics and Algebraic Specification","author":"J Meseguer","year":"2009","unstructured":"Meseguer, J.: Order-sorted parameterization and induction. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol. 5700, pp. 43\u201380. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04164-8_4"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-030-63595-4_6","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J.: Variant satisfiability of parameterized strings. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 96\u2013113. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_6"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-63595-4_5","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J.: Variants in the infinitary unification wonderland. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 75\u201395. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_5"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-030-63595-4_7","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J., Skeirik, S.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 114\u2013135. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_7"},{"issue":"1\u20132","key":"1_CR51","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 the verification of cryptographic protocols. J. Higher-Order Symbolic Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. Higher-Order Symbolic Comput."},{"issue":"1","key":"1_CR52","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64299-4_26"},{"key":"1_CR54","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic Log. Program. 81, 721\u2013781 (2012)","journal-title":"J. Algebraic Log. Program."},{"key":"1_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.12.026","volume":"672","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci. 672, 1\u201335 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR56","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3\u201341 (2018)","journal-title":"Sci. Comput. Program."},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion and symbolic methods. J. Log. Algebraic Methods Program. (2019)","DOI":"10.1016\/j.jlamp.2019.100483"},{"issue":"1","key":"1_CR58","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1006\/inco.1993.1016","volume":"103","author":"J Meseguer","year":"1993","unstructured":"Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Inf. Comput. 103(1), 114\u2013158 (1993)","journal-title":"Inf. Comput."},{"key":"1_CR59","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/S0747-7171(89)80036-7","volume":"8","author":"J Meseguer","year":"1989","unstructured":"Meseguer, J., Goguen, J., Smolka, G.: Order-sorted unification. J. Symbolic Comput. 8, 383\u2013413 (1989)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"1_CR60","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR61","series-title":"Undergraduate Topics in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-6687-0","volume-title":"Designing Reliable Distributed Systems","author":"PC \u00d6lveczky","year":"2017","unstructured":"\u00d6lveczky, P.C.: Designing Reliable Distributed Systems. UTCS. Springer, London (2017). https:\/\/doi.org\/10.1007\/978-1-4471-6687-0"},{"key":"1_CR62","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"1_CR63","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"GE Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Mach. 28(2), 233\u2013264 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"1_CR64","first-page":"73","volume":"7","author":"G Plotkin","year":"1972","unstructured":"Plotkin, G.: Building-in equational theories. Mach. Intell. 7, 73\u201390 (1972)","journal-title":"Mach. Intell."},{"key":"1_CR65","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach."},{"key":"1_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024065","volume-title":"Computational Aspects of an Order-Sorted Logic with Term Declarations","year":"1989","unstructured":"Schmidt-Schau\u00df, M. (ed.): Computational Aspects of an Order-Sorted Logic with Term Declarations. LNCS, vol. 395. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0024065"},{"key":"1_CR67","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2307\/1969640","volume":"60","author":"A Seidenberg","year":"1954","unstructured":"Seidenberg, A.: A new decision method for elementary algebra. Ann. Math. 60, 365\u2013374 (1954)","journal-title":"Ann. Math."},{"key":"1_CR68","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.jlamp.2017.12.006","volume":"96","author":"S Skeirik","year":"2018","unstructured":"Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. J. Log. Algebr. Meth. Program. 96, 81\u2013110 (2018)","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"4","key":"1_CR69","doi-asserted-by":"publisher","first-page":"315","DOI":"10.3233\/FI-2020-1926","volume":"173","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fundam. Inform. 173(4), 315\u2013382 (2020)","journal-title":"Fundam. Inform."},{"issue":"4","key":"1_CR70","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"JR Slagle","year":"1974","unstructured":"Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622\u2013642 (1974)","journal-title":"J. ACM"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., A\u00eft-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 297\u2013367. Academic Press (1989)","DOI":"10.1016\/B978-0-12-046371-8.50016-X"},{"key":"1_CR72","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951). prepared with the assistance of J.C.C. McKinsey"},{"key":"1_CR73","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR74","unstructured":"Yices: https:\/\/yices.csl.sri.com"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-68446-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T03:46:09Z","timestamp":1724471169000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-68446-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030684457","9783030684464"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-68446-4_1","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":"13 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bologna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nms.kcl.ac.uk\/maribel.fernandez\/LOPSTR2020\/","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":"31","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":"15","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":"48% - 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","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":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","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":"In addition, two invited talks are included in the proceedings. Due to the COVID-19 pandemic the conference was held virtually.","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)"}}]}}