{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:10Z","timestamp":1762458850956},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"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-16242-8_42","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"594-609","source":"Crossref","is-referenced-by-count":9,"title":["Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories"],"prefix":"10.1007","author":[{"given":"Camilo","family":"Rocha","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"42_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":"42_CR2","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":"42_CR3","doi-asserted-by":"crossref","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) ISBN 3-540-56610-4","DOI":"10.1007\/3-540-56610-4_55"},{"issue":"1-2","key":"42_CR4","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/S0304-3975(96)80708-0","volume":"170","author":"A. Bouhoula","year":"1996","unstructured":"Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science\u00a0170(1-2), 245\u2013276 (1996)","journal-title":"Theoretical Computer Science"},{"key":"42_CR5","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"},{"key":"42_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-540-71070-7_44","volume-title":"Automated Reasoning","author":"A. Bouhoula","year":"2008","unstructured":"Bouhoula, A., Jacquemard, F.: Automated induction with constrained tree automata. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 539\u2013554. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"42_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-2), 35\u2013132 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1-3","key":"42_CR8","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R. Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science\u00a0360(1-3), 386\u2013414 (2006)","journal-title":"Theoretical Computer Science"},{"key":"42_CR9","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science\u00a0285, 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"42_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-16780-3_85","volume-title":"8th International Conference on Automated Deduction","author":"H. Comon","year":"1986","unstructured":"Comon, H.: Sufficient completness, term rewriting systems and \u201canti-unification\u201d. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 3\u2013540. Springer, Heidelberg (1986), ISBN 3-540-16780-3"},{"key":"42_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-50667-5_62","volume-title":"Algebraic and Logic Programming","author":"H. Comon","year":"1989","unstructured":"Comon, H.: An effective method for handling initial algebras. In: Grabowski, J., Wechler, W., Lescanne, P. (eds.) ALP 1988. LNCS, vol.\u00a0343, pp. 108\u2013118. Springer, Heidelberg (1989), ISBN 3-540-50667-5"},{"key":"42_CR12","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007)"},{"issue":"1","key":"42_CR13","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0890-5401(03)00134-2","volume":"187","author":"H. Comon","year":"2003","unstructured":"Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation\u00a0187(1), 123\u2013153 (2003)","journal-title":"Information and Computation"},{"key":"42_CR14","doi-asserted-by":"crossref","unstructured":"Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Bossi, A., Maher, M.J. (eds.) PPDP, pp. 121\u2013132. ACM, New York (2006) ISBN 1-59593-388-3","DOI":"10.1145\/1140335.1140351"},{"key":"42_CR15","unstructured":"Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Computer Science Department (1975)"},{"key":"42_CR16","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica\u00a010, 27\u201352 (1978)","journal-title":"Acta Informatica"},{"key":"42_CR17","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)"},{"key":"42_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"Term Rewriting and Applications","author":"J. Hendrix","year":"2005","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 165\u2013174. Springer, Heidelberg (2005), ISBN 3-540-25596-6"},{"key":"42_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-73449-9_18","volume-title":"Term Rewriting and Applications","author":"J. Hendrix","year":"2007","unstructured":"Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 229\u2013245. Springer, Heidelberg (2007), ISBN 978-3-540-73447-5"},{"key":"42_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11805618_5","volume-title":"Term Rewriting and Applications","author":"J. Hendrix","year":"2006","unstructured":"Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 50\u201365. Springer, Heidelberg (2006), ISBN 3-540-36834-5"},{"key":"42_CR21","first-page":"96","volume-title":"FOCS","author":"G.P. Huet","year":"1980","unstructured":"Huet, G.P., Hullot, J.-M.: Proofs by induction in equational theories with constructors. In: FOCS, pp. 96\u2013107. IEEE, Los Alamitos (1980)"},{"issue":"1","key":"42_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation\u00a082(1), 1\u201333 (1989)","journal-title":"Information and Computation"},{"issue":"1","key":"42_CR23","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"},{"issue":"4","key":"42_CR24","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica\u00a028(4), 311\u2013350 (1991)","journal-title":"Acta Informatica"},{"issue":"4","key":"42_CR25","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica\u00a024(4), 395\u2013415 (1987)","journal-title":"Acta Informatica"},{"issue":"1","key":"42_CR26","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(92)90279-O","volume":"106","author":"E. Kounalis","year":"1992","unstructured":"Kounalis, E.: Testing for the ground (co-)reducibility property in term-rewriting systems. Theoretical Computer Science\u00a0106(1), 87\u2013117 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"42_CR27","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0890-5401(90)90033-E","volume":"84","author":"A. Lazrek","year":"1990","unstructured":"Lazrek, A., Lescanne, P., Thiel, J.-J.: Tools for proving inductive equalities, relative completeness, and omega-completeness. Information and Computation\u00a084(1), 47\u201370 (1990)","journal-title":"Information and Computation"},{"key":"42_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), ISBN 3-540-52885-7"},{"issue":"1","key":"42_CR29","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. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"42_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0036486","volume-title":"Theoretical Computer Science","author":"T. Nipkow","year":"1982","unstructured":"Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) GI-TCS 1983. LNCS, vol.\u00a0145, pp. 257\u2013268. Springer, Heidelberg (1982), ISBN 3-540-11973-6"},{"key":"42_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":"42_CR32","doi-asserted-by":"crossref","unstructured":"Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of generalized rewrite theories. Technical report, University of Illinois at Urbana-Champaign (2010)","DOI":"10.1007\/978-3-642-16242-8_42"},{"key":"42_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, 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T02:02:16Z","timestamp":1559700136000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}