{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:02:51Z","timestamp":1743148971576,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031712937"},{"type":"electronic","value":"9783031712944"}],"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-71294-4_5","type":"book-chapter","created":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:03:47Z","timestamp":1725631427000},"page":"82-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Combined Abstract Congruence Closure for\u00a0Theories with\u00a0Associativity or\u00a0Commutativity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5937-6059","authenticated-orcid":false,"given":"Christophe","family":"Ringeissen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0764-3646","authenticated-orcid":false,"given":"Laurent","family":"Vigneron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,7]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-63104-6_3","volume-title":"Automated Deduction\u2014CADE-14","author":"F Baader","year":"1997","unstructured":"Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 19\u201333. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63104-6_3"},{"issue":"2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reason. 31(2), 129\u2013168 (2003)","journal-title":"J. Autom. Reason."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-45988-X_11","volume-title":"Frontiers of Combining Systems","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Armando, A. (ed.) FroCoS 2002. LNCS (LNAI), vol. 2309, pp. 132\u2013146. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45988-X_11"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd Edn., Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"5_CR6","unstructured":"Erbatur, S., Marshall, A.M., Ringeissen, C.: Combined hierarchical matching: the regular case. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction, FSCD, Haifa, Israel, August 2022. LIPIcs, vol.\u00a0228, pp. 6:1\u20136:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23\u201337. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_59"},{"key":"5_CR8","unstructured":"Kapur, D.: A modular associative commutative (AC) congruence closure algorithm. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD, Buenos Aires, Argentina, July 2021 (Virtual Conference). LIPIcs, vol.\u00a0195, pp. 15:1\u201315:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Modularity and combination of associative commutative congruence closure algorithms enriched with semantic properties. Log. Methods Comput. Sci. 19(1) (2023)","DOI":"10.46298\/lmcs-19(1:19)2023"},{"key":"5_CR10","unstructured":"Kim, D.: Congruence closure modulo groups. CoRR abs\/2310.05014 (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.05014"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Kim, D., Lynch, C.: Congruence closure modulo permutation equations. In: Kutsia, T. (ed.) 9th International Symposium on Symbolic Computation in Software Science, SCSS, Hagenberg, Austria, September 2021, Proceedings. EPTCS, vol.\u00a0342, pp. 86\u201398 (2021)","DOI":"10.4204\/EPTCS.342.8"},{"key":"5_CR12","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2023.100877","volume":"134","author":"J Meseguer","year":"2023","unstructured":"Meseguer, J.: Variants and satisfiability in the infinitary unification wonderland. J. Log. Algebr. Methods Program. 134, 100877 (2023)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"2","key":"5_CR13","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."},{"issue":"2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"issue":"2","key":"5_CR16","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. ACM 28(2), 233\u2013264 (1981)","journal-title":"J. ACM"},{"key":"5_CR17","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":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-31862-0_27","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"S Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Tran, D.-K.: Nelson-Oppen, Shostak and the extended Canonizer: a family picture with a newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 372\u2013386. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_27"},{"issue":"1","key":"5_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1\u201331 (2003)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.jsc.2008.10.006","volume":"45","author":"D Tran","year":"2010","unstructured":"Tran, D., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261\u2013286 (2010)","journal-title":"J. Symb. Comput."},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/3-540-61377-3_54","volume-title":"Computer Science Logic","author":"L Vigneron","year":"1996","unstructured":"Vigneron, L.: Positive deduction modulo regular theories. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 468\u2013485. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61377-3_54"}],"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-031-71294-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:04:44Z","timestamp":1725631484000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71294-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712937","9783031712944"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71294-4_5","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":"7 September 2024","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":"Milan","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=63#lopstrppdp2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}