{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:11:46Z","timestamp":1791061906505,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642163098","type":"print"},{"value":"9783642163104","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16310-4_6","type":"book-chapter","created":{"date-parts":[[2010,9,30]],"date-time":"2010-09-30T23:44:29Z","timestamp":1285890269000},"page":"69-85","source":"Crossref","is-referenced-by-count":16,"title":["A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1-2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0747-7171(03)00024-5","volume":"36","author":"J. Avenhaus","year":"2003","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On using ground joinable equations in equational theorem proving. Journal of Symbolic Computation\u00a036(1-2), 217\u2013233 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-58216-9_40","volume-title":"Logic Programming and Automated Reasoning","author":"J. Avenhaus","year":"1994","unstructured":"Avenhaus, J., Lor\u00eda-S\u00e1enz, C.: On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 215\u2013229. Springer, Heidelberg (1994)"},{"key":"6_CR3","series-title":"Rewriting Techniques","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Kaci, A.H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol.\u00a02, pp. 1\u201330. Academic Press, New York (1989)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-56610-4_55","volume-title":"TAPSOFT \u201993: Theory and Practice of Software Development","author":"K. Becker","year":"1993","unstructured":"Becker, K.: Proving ground confluence and inductive validity in constructor based equational specifications. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 46\u201360. Springer, Heidelberg (1993)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-10003-2_61","volume-title":"Seventh Colloquium on Automata, Languages and Programming","author":"J. Bergstra","year":"1980","unstructured":"Bergstra, J., Tucker, J.: Characterization of computable data types by means of a finite equational specification method. In: de Bakker, J.W., van Leeuwen, J. (eds.) Seventh Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a081, pp. 76\u201390. Springer, Heidelberg (1980)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Bouhoula, A.: Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Transactions on Computational Logic\u00a010(3) (2009)","DOI":"10.1145\/1507244.1507250"},{"issue":"1","key":"6_CR7","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. Theoretical Computer Science\u00a0236(1), 35\u2013132 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"6_CR8","first-page":"286","volume":"351","author":"R. Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science\u00a0351(1), 286\u2013414 (2006)","journal-title":"Theoretical Computer Science"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"6_CR10","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.4 manual (November 2008), http:\/\/maude.cs.uiuc.edu"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73859-6_12","volume-title":"Algebra and Coalgebra in Computer Science","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Hendrix, J., Lucas, S., Meseguer, J., \u00d6lveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol.\u00a04624, pp. 173\u2013178. Springer, Heidelberg (2007)"},{"issue":"11","key":"6_CR12","first-page":"1618","volume":"12","author":"M. Clavel","year":"2006","unstructured":"Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science\u00a012(11), 1618\u20131650 (2006)","journal-title":"Journal of Universal Computer Science"},{"key":"6_CR13","unstructured":"Dur\u00e1n, F.: A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, Universidad de M\u00e1laga, Spain (June 1999), http:\/\/maude.csl.sri.com\/papers"},{"key":"6_CR14","series-title":"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.\u00a05195, pp. 313\u2013319. Springer, Heidelberg (2008)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"FroCoS 2009","author":"F. Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 246\u2013262. Springer, Heidelberg (2009)"},{"issue":"2","key":"6_CR16","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","volume":"66","author":"F. Dur\u00e1n","year":"2007","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Science of Computer Programming\u00a066(2), 125\u2013153 (2007)","journal-title":"Science of Computer Programming"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: CRC 3: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (2009), http:\/\/maude.lcc.uma.es\/CRChC","DOI":"10.1007\/978-3-642-16310-4_6"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-642-16310-4_7","volume-title":"WRLA 2010","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Olveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 86\u2013103. Springer, Heidelberg (2010)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Meseguer, J.: A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications. In: \u00d6lveczky, P.C. (ed.) 8th Intl. Workshop on Rewriting Logic and its Applications (2010)","DOI":"10.1007\/978-3-642-16310-4_6"},{"key":"6_CR20","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings 7th International Workshop on Rewriting Logic and its Applications (WRLA 2008)","author":"F. Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., \u00d6lveczky, P.C.: A guide to extending Full Maude illustrated with the implementation of Real-Time Maude. In: Ro\u015fu, G. (ed.) Proceedings 7th International Workshop on Rewriting Logic and its Applications (WRLA 2008). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2008)"},{"key":"6_CR21","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":"6_CR22","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. Theoretical Computer Science\u00a072, 169\u2013202 (1990)","journal-title":"Theoretical Computer Science"},{"key":"6_CR23","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. Theoretical Computer Science\u00a0105, 217\u2013273 (1992)","journal-title":"Theoretical Computer Science"},{"key":"6_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 151\u2013155. Springer, Heidelberg (2006)"},{"issue":"4","key":"6_CR25","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":"6_CR26","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/0890-5401(90)90023-B","volume":"86","author":"D. Kapur","year":"1990","unstructured":"Kapur, D., Narendran, P., Otto, F.: On ground-confluence of term rewriting systems. Information and Computation\u00a086(1), 14\u201331 (1990)","journal-title":"Information and Computation"},{"key":"6_CR27","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":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-52885-7_100","volume-title":"10th International Conference on Automated Deduction","author":"U. Martin","year":"1990","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 366\u2013380. Springer, Heidelberg (1990)"},{"key":"6_CR29","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)"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.: Complete sets of reductions for some equational theories. Journal of ACM\u00a028(2), 233\u2013264 (1981)","journal-title":"Journal of ACM"},{"key":"6_CR31","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"Plaisted, D.: Semantic confluence tests and completion methods. Information and Control\u00a065, 182\u2013215 (1985)","journal-title":"Information and Control"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Rocha, C., Meseguer, J.: Constructors, sufficient completeness, deadlock states of rewrite theories. Technical Report 2010-05-1, CS Dept., University of Illinois at Urbana-Champaign (May 2010), http:\/\/ideals.illinois.edu","DOI":"10.1007\/978-3-642-16242-8_42"},{"issue":"2","key":"6_CR33","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. Theoretical Computer Science\u00a0285(2), 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16310-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T01:02:51Z","timestamp":1559696571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16310-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642163098","9783642163104"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16310-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}