{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:37:03Z","timestamp":1742920623417,"version":"3.40.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031314759"},{"type":"electronic","value":"9783031314766"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-31476-6_2","type":"book-chapter","created":{"date-parts":[[2023,5,16]],"date-time":"2023-05-16T07:02:46Z","timestamp":1684220566000},"page":"21-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Optimizing Maude Programs via\u00a0Program Specialization"],"prefix":"10.1007","author":[{"given":"Mar\u00eda","family":"Alpuente","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Demis","family":"Ballis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,17]]},"reference":[{"key":"2_CR1","unstructured":"Albert, E., Alpuente, M., Falaschi, M., Vidal, G.: Indy User\u2019s Manual. Technical report DSIC-II\/12\/98, Department of Computer Systems and Computation, Universitat Polit\u00e8cnica de Val\u00e8ncia (1998)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-48242-3_23","volume-title":"Logic for Programming and Automated Reasoning","author":"E Albert","year":"1999","unstructured":"Albert, E., Alpuente, M., Harms, M., Vidal, G.: A partial evaluation framework for curry programs. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol. 1705, pp. 376\u2013395. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48242-3_23"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Alpuente, M., Ballis, D., Baggi, M., Falaschi, F.: A fold\/unfold transformation framework for rewrite theories extended to CCT. In: Gallagher, J., Voigtl\u00e4nder, J. (eds.) ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2010), pp. 43\u201352. ACM. https:\/\/doi.org\/10.1145\/1706356.1706367","DOI":"10.1145\/1706356.1706367"},{"issue":"5\u20136","key":"2_CR4","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1017\/S1471068416000375","volume":"16","author":"M Alpuente","year":"2016","unstructured":"Alpuente, M., Ballis, D., Frechina, F., Sapi\u00f1a, J.: Assertion-based analysis via slicing with ABETS (system description). Theory Pract. Logic Program. 16(5\u20136), 515\u2013532 (2016)","journal-title":"Theory Pract. Logic Program."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1016\/j.jlamp.2016.03.001","volume":"85","author":"M Alpuente","year":"2016","unstructured":"Alpuente, M., Ballis, D., Frechina, F., Sapi\u00f1a, J.: Debugging Maude programs via runtime assertion checking and trace slicing. J. Log. Algebr. Methods Program. 85, 707\u2013736 (2016)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.scico.2013.07.014","volume":"81","author":"M Alpuente","year":"2014","unstructured":"Alpuente, M., Ballis, D., Romero, D.: A rewriting logic approach to the formal specification and verification of web applications. Sci. Comput. Program. 81, 79\u2013107 (2014)","journal-title":"Sci. Comput. Program."},{"key":"2_CR7","first-page":"1","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. Algebr. Methods Program. 110, 1\u201336 (2020)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"3\u20134","key":"2_CR8","first-page":"297","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. Fund. Inform. 177(3\u20134), 297\u2013329 (2020)","journal-title":"Fund. Inform."},{"issue":"5\u20136","key":"2_CR9","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1017\/S147106841700031X","volume":"17","author":"M Alpuente","year":"2017","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Sapi\u00f1a, J.: Inspecting Maude variants with GLINTS. Theory Pract. Logic Program. 17(5\u20136), 689\u2013707 (2017)","journal-title":"Theory Pract. Logic Program."},{"key":"2_CR10","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."},{"issue":"46","key":"2_CR11","doi-asserted-by":"publisher","first-page":"4608","DOI":"10.1016\/j.tcs.2009.07.037","volume":"410","author":"M Alpuente","year":"2009","unstructured":"Alpuente, M., Escobar, S., Iborra, J.: Termination of narrowing revisited. Theoret. Comput. Sci. 410(46), 4608\u20134625 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Falaschi, M., Juli\u00e1n, P., Vidal, G.: Specialization of lazy functional logic programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 1997), pp. 151\u2013162. Association for Computing Machinery (1997)","DOI":"10.1145\/258994.259015"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0026999","volume-title":"Algebraic and Logic Programming","author":"M Alpuente","year":"1997","unstructured":"Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: Safe folding\/unfolding with conditional narrowing. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP\/HOA -1997. LNCS, vol. 1298, pp. 1\u201315. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0026999"},{"issue":"3es","key":"2_CR14","doi-asserted-by":"publisher","first-page":"9es","DOI":"10.1145\/289121.289130","volume":"30","author":"M Alpuente","year":"1998","unstructured":"Alpuente, M., Falaschi, M., Vidal, G.: A unifying view of functional and logic program specialization. ACM Comput. Surv. 30(3es), 9es (1998)","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"2_CR15","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1145\/291891.291896","volume":"20","author":"M Alpuente","year":"1998","unstructured":"Alpuente, M., Falaschi, M., Vidal, G.: Partial evaluation of functional logic programs. ACM Trans. Program. Lang. Syst. 20(4), 768\u2013844 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1017\/S1471068404002303","volume":"5","author":"M Alpuente","year":"2005","unstructured":"Alpuente, M., Lucas, S., Hanus, M., Vidal, G.: Specialization of functional logic programs based on needed narrowing. Theory Pract. Logic Program. 5(3), 273\u2013303 (2005)","journal-title":"Theory Pract. Logic Program."},{"key":"2_CR17","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), vol. 21, pp. 81\u201396. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Baelde, D., Delaune, S., Gazeau, I., Kremer, S.: Symbolic verification of privacy-type properties for security protocols with XOR. In: Proceedings of the 30th International Symposium on Computer Security Foundations (CSF 2017), pp. 234\u2013248. IEEE Computer Society Press (2017)","DOI":"10.1109\/CSF.2017.22"},{"key":"2_CR19","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"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977)","journal-title":"J. ACM"},{"key":"2_CR21","unstructured":"Clavel, M., et al.: Maude Manual (Version 3.0). Technical report, SRI International Computer Science Laboratory (2020). http:\/\/maude.cs.uiuc.edu"},{"key":"2_CR22","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":"2_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61580-6","volume-title":"Partial Evaluation, International Seminar, Dagstuhl Castle, Germany","author":"O Danvy","year":"1996","unstructured":"Danvy, O., Gl\u00fcck, R., Thiemann, P.: Partial Evaluation, International Seminar, Dagstuhl Castle, Germany. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61580-6"},{"key":"2_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100497","volume":"110","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebr. Methods Program. 110, 100497 (2020)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"2_CR25","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":"2_CR26","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":"2_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100513","volume":"111","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., Meseguer, J., Rocha, C.: Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebr. Methods Program. 111, 100513 (2020)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"2_CR28","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":"2_CR29","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"},{"issue":"3","key":"2_CR30","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","volume":"238","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theor. Comput. Sci. 238(3), 103\u2013119 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"7\u20138","key":"2_CR31","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":"2_CR32","doi-asserted-by":"crossref","unstructured":"Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Proceedings of the 8th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2006), pp. 121\u2013132. Association for Computing Machinery (2006)","DOI":"10.1145\/1140335.1140351"},{"key":"2_CR33","volume-title":"Partial Evaluation and Automatic Program Generation","author":"ND Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Hoboken (1993)"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-48958-4_11","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M Leuschel","year":"1999","unstructured":"Leuschel, M.: Improving homeomorphic embedding for online termination. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 199\u2013218. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48958-4_11"},{"issue":"3\u20134","key":"2_CR35","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0743-1066(91)90027-M","volume":"11","author":"JW Lloyd","year":"1991","unstructured":"Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. J. Logic Program. 11(3\u20134), 217\u2013242 (1991)","journal-title":"J. Logic Program."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Martens, B., Gallagher, J.: Ensuring global termination of partial deduction while allowing flexible polyvariance. In: Proceedings of the 12th International Conference on Logic Programming (ICLP 1995), pp. 597\u2013611. The MIT Press (1995)","DOI":"10.7551\/mitpress\/4298.003.0059"},{"key":"2_CR37","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"},{"issue":"1","key":"2_CR38","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. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR39","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"},{"key":"2_CR40","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":"2_CR41","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.100483","volume":"110","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebr. Methods Program. 110, 100483 (2020)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"2\u20133","key":"2_CR42","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. Theoret. Comput. Sci. 403(2\u20133), 239\u2013264 (2008)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"2_CR43","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 Symb. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"Higher-Order Symb. Comput."},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0013830","volume-title":"Algebraic and Logic Programming","author":"A Middeldorp","year":"1992","unstructured":"Middeldorp, A., Hamoen, E.: Counterexamples to completeness results for basic narrowing (extended abstract). In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 244\u2013258. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0013830"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"key":"2_CR46","unstructured":"The Presto Website (2020). http:\/\/safe-tools.dsic.upv.es\/presto"},{"key":"2_CR47","unstructured":"Ro\u015fu, G.: $$\\mathbb{K} $$: a semantic framework for programming languages and formal analysis tools. In: Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 50, pp. 186\u2013206. IOS Press (2017)"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, A., Dur\u00e1n, F., Rutle, A., Kristensen, L.M.: Executing multilevel domain-specific models in Maude. J. Object Technol. 18(2), 4:1\u20134:21 (2019)","DOI":"10.5381\/jot.2019.18.2.a4"},{"issue":"4","key":"2_CR49","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"},{"issue":"2","key":"2_CR50","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. Theoret. Comput. Sci. 285(2), 487\u2013517 (2002)","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-31476-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T01:09:28Z","timestamp":1702429768000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-31476-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031314759","9783031314766"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-31476-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 May 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}