{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:54:52Z","timestamp":1780563292748,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642042218","type":"print"},{"value":"9783642042225","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04222-5_15","type":"book-chapter","created":{"date-parts":[[2009,9,16]],"date-time":"2009-09-16T12:42:11Z","timestamp":1253104931000},"page":"246-262","source":"Crossref","is-referenced-by-count":23,"title":["Termination Modulo Combinations of Equational Theories"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Salvador","family":"Lucas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Applied Logic Series","first-page":"225","volume-title":"Automated Deduction","author":"F. Baader","year":"1998","unstructured":"Baader, F., Schulz, K.U.: Unification Theory. In: Automated Deduction. Applied Logic Series, vol.\u00a0I, 8, pp. 225\u2013263. Kluwer, Dordrecht (1998)"},{"issue":"2,3","key":"15_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theor. Comput. Sci.\u00a067(2,3), 173\u2013201 (1989)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A.B. Cherifa","year":"1987","unstructured":"Cherifa, A.B., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.\u00a09(2), 137\u2013159 (1987)","journal-title":"Sci. Comput. Program."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"15_CR5","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","year":"2005","unstructured":"Comon, H., Delaune, S.: The Finite Variant Property: How to Get Rid of Some Algebraic Properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"15_CR6","series-title":"LNAI","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.\u00a05195, pp. 313\u2013319. Springer, Heidelberg (2008)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination Modulo Combinations of Equational Theories (Long Version). University of Illinois Tech. Rep. (June 2009), http:\/\/hdl.handle.net\/2142\/12311","DOI":"10.1007\/978-3-642-04222-5_15"},{"issue":"1-2","key":"15_CR8","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10990-008-9028-2","volume":"21","author":"F. Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving operational termination of membership equational programs. Higher-Order and Symbolic Computation\u00a021(1-2), 59\u201388 (2008)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-70590-1_6","volume-title":"Rewriting Techniques and Applications","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Effectively Checking the Finite Variant Property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol.\u00a05117, pp. 79\u201393. Springer, Heidelberg (2008)"},{"key":"15_CR10","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant Narrowing and Equational Unification. In: Proc. of WRLA 2008. ENTCS (2008) (to appear, 2009)"},{"key":"15_CR11","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant Narrowing and Extreme Termination. University of Illinois Tech. Rep. UIUCDCS-R-2009-3049 (March 2009)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61464-8_44","volume-title":"Rewriting Techniques and Applications","author":"M.C.F. Ferreira","year":"1996","unstructured":"Ferreira, M.C.F.: Dummy elimination in equational rewriting. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103. Springer, Heidelberg (1996)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45127-7_9","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Dependency Pairs for Equational Rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 93\u2013108. Springer, Heidelberg (2001)"},{"key":"15_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"15_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: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci.\u00a0105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM\u00a027, 797\u2013821 (1980)","journal-title":"Journal of the ACM"},{"issue":"4","key":"15_CR17","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal of Computing\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM Journal of Computing"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0304-3975(92)90165-C","volume":"104","author":"J.-P. Jouannaud","year":"1992","unstructured":"Jouannaud, J.-P., March\u00e9, C.: Termination and completion modulo associativity, commutativity and identity. Theor. Comput. Sci.\u00a0104(1), 29\u201351 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR19","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.) ICALP 1988. LNCS, vol.\u00a0317, pp. 287\u2013301. Springer, Heidelberg (1988)"},{"key":"15_CR20","unstructured":"Lucas, S., Meseguer, J.: Operational Termination of Membership Equational Programs: the Order-Sorted Way. In: Proc. of WRLA 2008. ENTCS (2008) (to appear, 2009)"},{"key":"15_CR21","first-page":"394","volume-title":"Proc. LICS 1994","author":"C. March\u00e9","year":"1994","unstructured":"March\u00e9, C.: Normalised rewriting and normalised completion. In: Proc. LICS 1994, pp. 394\u2013403. IEEE, Los Alamitos (1994)"},{"key":"15_CR22","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/BFb0052374","volume-title":"Rewriting Techniques and Applications","author":"C. March\u00e9","year":"1998","unstructured":"March\u00e9, C., Urbain, X.: Termination of associative-commutative rewriting by dependency pairs. In: Nipkow, T. (ed.) RTA 1998, vol.\u00a01379, pp. 241\u2013255. Springer, Heidelberg (1998)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/S0747-7171(08)80145-9","volume":"12","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Combining Matching Algorithms: The Regular Case. Journal of Symbolic Computation\u00a012, 633\u2013653 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/3-540-44622-2_31","volume-title":"Computer Science Logic","author":"H. Ohsaki","year":"2000","unstructured":"Ohsaki, H., Middeldorp, A., Giesl, J.: Equational termination by semantic labelling. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 457\u2013471. Springer, Heidelberg (2000)"},{"issue":"2","key":"15_CR26","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete Sets of Reductions for Some Equational Theories. Journal of the ACM\u00a028(2), 233\u2013264 (1981)","journal-title":"Journal of the ACM"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-57785-8_141","volume-title":"STACS 94","author":"C. Ringeissen","year":"1994","unstructured":"Ringeissen, C.: Combination of matching algorithms. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol.\u00a0775, pp. 187\u2013198. Springer, Heidelberg (1994)"},{"issue":"2","key":"15_CR28","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(94)00276-2","volume":"142","author":"A. Rubio","year":"1995","unstructured":"Rubio, A., Nieuwenhuis, R.: A total AC-compatible ordering based on RPO. Theor. Comput. Sci.\u00a0142(2), 209\u2013227 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR29","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. Comp. Sci.\u00a0285, 487\u2013517 (2002)","journal-title":"Theor. Comp. Sci."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04222-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T13:17:26Z","timestamp":1558531046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04222-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042218","9783642042225"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04222-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}