{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:26:43Z","timestamp":1763389603489,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031124402"},{"type":"electronic","value":"9783031124419"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-12441-9_9","type":"book-chapter","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:34Z","timestamp":1659090214000},"page":"171-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Checking Sufficient Completeness by\u00a0Inductive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,30]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Bouhoula, A.: Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Trans. Comput. Log. 10(3), 20:1\u201320:33 (2009)","key":"9_CR1","DOI":"10.1145\/1507244.1507250"},{"issue":"1","key":"9_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.2001.3036","volume":"169","author":"A Bouhoula","year":"2001","unstructured":"Bouhoula, A., Jouannaud, J.P.: Automata-driven automated induction. Inf. Comput. 169(1), 1\u201322 (2001)","journal-title":"Inf. Comput."},{"key":"9_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. Theor. Comput. Sci. 236, 35\u2013132 (2000)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Department University of Illinois at Urbana-Champaign (2014). http:\/\/hdl.handle.net\/2142\/47117","key":"9_CR4"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude-A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude-A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","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 completeness, term rewriting systems and \u201canti-unification\u2019\u2019. In: Siekmann, J. (ed.) CADE 1986. LNCS, vol. 230, pp. 128\u2013140. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16780-3_85"},{"key":"9_CR7","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-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"doi-asserted-by":"crossref","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 (1990)","key":"9_CR8","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"Frontiers of Combining Systems","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 (LNAI), vol. 5749, pp. 246\u2013262. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_15"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic Logic Program. 81, 816\u2013850 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"100513","DOI":"10.1016\/j.jlamp.2019.100513","volume":"111","author":"F Dur\u00e1n","year":"2020","unstructured":"Dur\u00e1n, F., Meseguer, J., Rocha, C.: Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebraic Methods Program. 111, 100513 (2020)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Logic Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Logic Program."},{"doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific (1998)","key":"9_CR13","DOI":"10.1142\/3831"},{"key":"9_CR14","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. 105, 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, JP.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ. Advances in Formal Methods, vol 2. Springer, Boston (2000). https:\/\/doi.org\/10.1007\/978-1-4757-6541-0_1","key":"9_CR15","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"JV Guttag","year":"1978","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27\u201352 (1978). https:\/\/doi.org\/10.1007\/BF00260922","journal-title":"Acta Informatica"},{"key":"9_CR17","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. 3467, pp. 165\u2013174. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_13"},{"key":"9_CR18","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. 4533, pp. 229\u2013245. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_18"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science (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. 4130, pp. 151\u2013155. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_14"},{"issue":"1","key":"9_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"JP Jouannaud","year":"1989","unstructured":"Jouannaud, J.P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Inf. Comput. 82(1), 1\u201333 (1989)","journal-title":"Inf. Comput."},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01212959","volume":"36","author":"D Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Int. J. Biometeorol. 36(4), 311\u2013350 (1991). https:\/\/doi.org\/10.1007\/BF01212959","journal-title":"Int. J. Biometeorol."},{"unstructured":"Kikuchi, K., Aoto, T.: Simple derivation systems for proving sufficient completeness of non-terminating term rewriting systems. In: 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021. LIPIcs, vol. 213, pp. 49:1\u201349:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)","key":"9_CR22"},{"issue":"3","key":"9_CR23","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/bf00243794","volume":"3","author":"JL Lassez","year":"1987","unstructured":"Lassez, J.L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reasoning 3(3), 301\u2013317 (1987). https:\/\/doi.org\/10.1007\/bf00243794","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","volume":"85","author":"S Lucas","year":"2016","unstructured":"Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Meth. Program. 85(1), 67\u201397 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"doi-asserted-by":"crossref","unstructured":"Meseguer, J., Skeirik, S.: On ground convergence and completeness of conditional equational program hierarchies. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 191\u2013211. Springer, Cham (2022)","key":"9_CR25","DOI":"10.1007\/978-3-031-12441-9_10"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-030-63595-4_7","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J., Skeirik, S.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 114\u2013135. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_7"},{"issue":"1","key":"9_CR27","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. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR28","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: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64299-4_26"},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3\u201341 (2018)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"9_CR30","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00165-017-0415-5","volume":"29","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Formal Aspects Comput. 29(3), 423\u2013452 (2017). https:\/\/doi.org\/10.1007\/s00165-017-0415-5","journal-title":"Formal Aspects Comput."},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-54624-2_5","volume-title":"Specification, Algebra, and Software","author":"M Nakamura","year":"2014","unstructured":"Nakamura, M., Ogata, K., Futatsugi, K.: Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 92\u2013109. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_5"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-030-85315-0_22","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2021","author":"T Shiraishi","year":"2021","unstructured":"Shiraishi, T., Kikuchi, K., Aoto, T.: A proof method for local sufficient completeness of term rewriting systems. In: Cerone, A., \u00d6lveczky, P.C. (eds.) ICTAC 2021. LNCS, vol. 12819, pp. 386\u2013404. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_22"},{"doi-asserted-by":"crossref","unstructured":"Thiel, J.J.: Stop losing sleep over incomplete data type specification. In: Kennedy, K. (ed.) Proceedings, Eleventh Symposium on Principles of Programming Languages. Association for Computing Machinery (1984)","key":"9_CR33","DOI":"10.1145\/800017.800518"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-12441-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,12]],"date-time":"2023-02-12T23:33:25Z","timestamp":1676244805000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-12441-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031124402","9783031124419"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-12441-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sv.postech.ac.kr\/wrla2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}