{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:11:40Z","timestamp":1763388700636},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_13","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"165-174","source":"Crossref","is-referenced-by-count":17,"title":["A Sufficient Completeness Reasoning Tool for Partial Specifications"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hendrix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Clavel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"13_CR2","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, 35\u2013132 (2000)","journal-title":"Theoretical Computer Science"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/3-540-45465-9_49","volume-title":"Automata, Languages and Programming","author":"J. Meseguer","year":"2002","unstructured":"Meseguer, J., Ro\u015fu, G.: A total approach to partial algebraic specification. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 572\u2013584. Springer, Heidelberg (2002)"},{"key":"13_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-45085-6_2","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Meseguer","year":"2003","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 2\u201316. Springer, Heidelberg (2003)"},{"key":"13_CR5","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00244459","volume":"16","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: New uses of linear arithmetic in automated theorem proving by induction. Journal of Automated Reasoning\u00a016, 39\u201378 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR6","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\u00b4\u0131-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":"13_CR7","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1145\/197320.197356","volume":"16","author":"J. Misra","year":"1994","unstructured":"Misra, J.: Powerlist: a structure for parallel recursion. ACM Transactions on Programming Languages and Systems\u00a016, 1737\u20131767 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications (extended technical report) (2005), Available on tool website at http:\/\/maude.cs.uiuc.edu\/tools\/scc\/","key":"13_CR8","DOI":"10.1007\/978-3-540-32033-3_13"},{"unstructured":"Clavel, M.: The ITP tool\u2019s home page (2005), http:\/\/maude.sip.ucm.es\/itp","key":"13_CR9"},{"unstructured":"Guttag, J.: The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto Computer Science Department, Report CSRG-59 (1975)","key":"13_CR10"},{"key":"13_CR11","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 Inf.\u00a010, 27\u201352 (1978)","journal-title":"Acta Inf."},{"key":"13_CR12","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)"},{"key":"13_CR13","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, 395\u2013415 (1987)","journal-title":"Acta Informatica"},{"key":"13_CR14","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, 311\u2013350 (1991)","journal-title":"Acta Informatica"},{"unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on: http:\/\/www.grappa.univ-lille3.fr\/tata release (October 1, 2002)","key":"13_CR15"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1007\/3-540-60043-4_79","volume-title":"Algebraic Methodology and Software Technology","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: SPIKE: A system for automatic inductive proofs. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol.\u00a0936, pp. 576\u2013577. Springer, Heidelberg (1995)"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/186258.186496","volume-title":"Proceedings of the 1994 International Symposium on Software Testing and Analysis (ISSTA)","author":"D. Kapur","year":"1994","unstructured":"Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of the 1994 International Symposium on Software Testing and Analysis (ISSTA), Seattle, WA, USA. Software Engineering Notes, Special Issue, August 17-19, pp. 28\u201343. ACM Press, New York (1994)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-44881-0_34","volume-title":"Rewriting Techniques and Applications","author":"H. Ohsaki","year":"2003","unstructured":"Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 483\u2013498. Springer, Heidelberg (2003)"},{"key":"13_CR19","volume-title":"Cafe: An Industrial-Strength Algebraic Formal Method","author":"M. Clavel","year":"2000","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: Cafe: An Industrial-Strength Algebraic Formal Method, Elsevier, Amsterdam (2000)"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/1014007.1014022","volume-title":"Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation","author":"F. Dur\u00e1n","year":"2004","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving termination of membership equational programs. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, Verona, Italy, August 24-25, pp. 147\u2013158. ACM Press, New York (2004)"},{"doi-asserted-by":"crossref","unstructured":"Lucas, S., Meseguer, J., March\u00e9, C.: Operational termination of generalized conditional term rewriting systems. Submitted (2004)","key":"13_CR21","DOI":"10.1016\/j.ipl.2005.05.002"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:33:56Z","timestamp":1605760436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}