{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:02:55Z","timestamp":1762459375923},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496299"},{"type":"electronic","value":"9783662496305"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_29","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:04:32Z","timestamp":1458551072000},"page":"493-509","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Order-Sorted Rewriting and Congruence Closure"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1954)"},{"issue":"2","key":"29_CR2","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. Reasoning 31(2), 129\u2013168 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR3","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. Theoret. Comput. Sci. 236, 35\u2013132 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"issue":"3","key":"29_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(3:16)2012","volume":"8","author":"S Conchon","year":"2012","unstructured":"Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories : design and implementation. Logical Methods Comput. Sci. 8(3), 1\u201329 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"29_CR6","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N Dershowitz","year":"1990","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 Publishing Company, Amsterdam (1990)"},{"issue":"4","key":"29_CR7","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. ACM 27(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"issue":"1\u20133","key":"29_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"AM Frisch","year":"1991","unstructured":"Frisch, A.M.: The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artif. Intell. 49(1\u20133), 161\u2013198 (1991)","journal-title":"Artif. Intell."},{"key":"29_CR9","volume-title":"CafeOBJ Report","author":"K Futatsugi","year":"1998","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Goguen, J., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of POPL 1985, pp. 52\u201366. ACM (1985)","DOI":"10.1145\/318593.318610"},{"key":"29_CR11","unstructured":"Gallier, J., Isakowitz, T.: Order-sorted congruence closure. Technical report CIS-686, UPenn (1988). \n                      http:\/\/repository.upenn.edu\/cis_reports\/686"},{"issue":"1","key":"29_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"JH Gallier","year":"1993","unstructured":"Gallier, J.H., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1\u201316 (1993)","journal-title":"J. ACM"},{"issue":"2\u20133","key":"29_CR13","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(90)90034-F","volume":"72","author":"I Gnaedig","year":"1990","unstructured":"Gnaedig, I., Kirchner, C., Kirchner, H.: Equational completion in order-sorted algebras. Theoret. Comput. Sci. 72(2\u20133), 169\u2013202 (1990)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0015747","volume-title":"Automata, Languages and Programming","author":"J Goguen","year":"1985","unstructured":"Goguen, J., Jouannaud, J.P., Meseguer, J.: Operational semantics of order-sorted algebra. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol. 194, pp. 221\u2013231. Springer, Heidelberg (1985)"},{"key":"29_CR15","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. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR16","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)"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-19488-6_123","volume-title":"Automata, Languages and Programming","author":"C Kirchner","year":"1988","unstructured":"Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepist\u00f6, T., Salomaa, A. (eds.) Automata, Languages and Programming. LNCS, vol. 317, pp. 287\u2013301. Springer, Heidelberg (1988)"},{"key":"29_CR18","volume-title":"Computational Problems in Abstract Algebra","author":"D Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra. Pergamon Press, Oxford (1970)"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-53904-2_114","volume-title":"Rewriting Techniques and Applications","author":"C March\u00e9","year":"1991","unstructured":"March\u00e9, C.: On ground AC-completion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 411\u2013422. Springer, Heidelberg (1991)"},{"key":"29_CR20","unstructured":"Meseguer, J.: Order-sorted rewriting and congruence closure. Technical report, C.S. Department, University of Illinois at Urbana-Champaign, June 2015. \n                      http:\/\/hdl.handle.net\/2142\/78008"},{"key":"29_CR21","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: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-53904-2_115","volume-title":"Rewriting Techniques and Applications","author":"P Narendran","year":"1991","unstructured":"Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 423\u2013434. Springer, Heidelberg (1991)"},{"issue":"2","key":"29_CR23","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":"29_CR24","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"},{"key":"29_CR25","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. Theoret. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0024065","volume-title":"Computational Aspects of Order-Sorted Logic with Term Declarations","author":"M Schmidt-Schauss","year":"1989","unstructured":"Schmidt-Schauss, M.: Computational Aspects of Order-Sorted Logic with Term Declarations. LNCS (LNAI), vol. 395. Springer, Heidelberg (1989)"},{"issue":"7","key":"29_CR27","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"},{"issue":"1","key":"29_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"issue":"3\/4","key":"29_CR29","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/S0747-7171(89)80016-1","volume":"7","author":"G Smolka","year":"1989","unstructured":"Smolka, G., A\u00eft-Kaci, H.: Inheritance hierarchies: semantics and unification. J. Symb. Comput. 7(3\/4), 343\u2013370 (1989)","journal-title":"J. Symb. Comput."},{"key":"29_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C Tinelli","year":"2004","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 641\u2013653. Springer, Heidelberg (2004)"},{"key":"29_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-04222-5_4","volume-title":"Frontiers of Combining Systems","author":"A Tiwari","year":"2009","unstructured":"Tiwari, A.: Combining equational reasoning. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 68\u201383. Springer, Heidelberg (2009)"},{"issue":"2","key":"29_CR32","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0004-3702(85)90029-3","volume":"26","author":"C Walther","year":"1985","unstructured":"Walther, C.: A mechanical solution of Schubert\u2019s steamroller by many-sorted resolution. Artif. Intell. 26(2), 217\u2013224 (1985)","journal-title":"Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:08:57Z","timestamp":1585012137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}