{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T00:30:45Z","timestamp":1745281845735,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031659409"},{"type":"electronic","value":"9783031659416"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-65941-6_4","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"62-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Equivalence, and Property Internalization and Preservation for Equational Programs"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"4_CR1","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":"4_CR2","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR3","unstructured":"Dur\u00e1n, F., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: NuITP alpha 21\u2014an inductive theorem prover for maude equational theories. Available at https:\/\/nuitp.webs.upv.es\/"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05749, pp. 246\u2013262. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04222-5_15"},{"key":"4_CR6","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. Algebraic Methods Program. 111, 100513 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"4_CR7","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 Logic Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Futatsugi, K.: Advances of proof scores in CafeOBJ. Sci. Comput. Program. 224, 102893 (2022). https:\/\/doi.org\/10.1016\/j.scico.2022.102893","DOI":"10.1016\/j.scico.2022.102893"},{"key":"4_CR10","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":"4_CR11","doi-asserted-by":"crossref","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3\u2013167. Kluwer (2000)","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"4_CR12","unstructured":"Goguen, J.A.: Theorem proving and algebra. CoRR abs\/2101.02690 (2021). https:\/\/arxiv.org\/abs\/2101.02690"},{"key":"4_CR13","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge, UP (1997)"},{"issue":"1","key":"4_CR14","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."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Skeirik, S.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. In: Proceedings of WRLA 2020. LNCS, vol. 12328, pp. 114\u2013135. Springer, Berlin (2020)","DOI":"10.1007\/978-3-030-63595-4_7"},{"issue":"1","key":"4_CR16","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":"4_CR17","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Proceedings of WADT\u201997, pp. 18\u201361. Springer LNCS 1376 (1998)","DOI":"10.1007\/3-540-64299-4_26"},{"key":"4_CR18","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":"4_CR19","unstructured":"Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, pp. 459\u2013541. Cambridge University Press (1985)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Skeirik, S.: On ground convergence and completeness of conditional equational program hierarchies. In: Rewriting Logic and Its Applications\u201414th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022. Lecture Notes in Computer Science, vol. 13252, pp. 191\u2013211. Springer, Berlin (2022)","DOI":"10.1007\/978-3-031-12441-9_10"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65941-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:11:29Z","timestamp":1722496289000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wrla2024.gitlab.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}