{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:35Z","timestamp":1761597215073},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_20","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"275-290","source":"Crossref","is-referenced-by-count":2,"title":["Coverset Induction with Partiality and Subsorts: A Powerlist Case Study"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hendrix","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Maude ITP website at UIUC, \n                    \n                      http:\/\/maude.cs.uiuc.edu\/tools\/itp\/"},{"key":"20_CR2","unstructured":"Adams, W.: Verifying adder circuits using powerlists. Technical report, University of Texas, Austin, Department of Computer Science, Austin, TX, USA (1994)"},{"issue":"1","key":"20_CR3","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. J. Symb. Comput.\u00a023(1), 47\u201377 (1997)","journal-title":"J. Symb. Comput."},{"key":"20_CR4","unstructured":"Bouhoula, A., Jacquemard, F.: Automatic verification of sufficient completeness for conditional constrained term rewriting systems. Technical Report LSC-05-17, ENS de Cachan (2006), \n                    \n                      http:\/\/www.lsv.ens-cachan.fr\/Publis\/"},{"key":"20_CR5","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 Comput. Sci.\u00a0236, 35\u2013132 (2000)","journal-title":"Theoretical Comput. Sci."},{"key":"20_CR6","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","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":"20_CR8","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.C.: 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":"1-2","key":"20_CR9","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., March\u00e9, C., Meseguer, J., 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":"20_CR10","unstructured":"Gamboa, R.: Defthms about zip and tie: Reasoning about powerlists in ACL2. Technical Report TR87-02, University of Texas Computer Science (1997)"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19\/20","author":"M. Hanus","year":"1994","unstructured":"Hanus, M.: The integration of functions into logic programming: From theory to practice. J. Log. Program.\u00a019\/20, 583\u2013628 (1994)","journal-title":"J. Log. Program."},{"key":"20_CR12","unstructured":"Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (2008)"},{"key":"20_CR13","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)"},{"key":"20_CR14","first-page":"177","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Constructors can be partial too. In: Automated Reasoning and its Applications: Essays in Honor of Larry Wos, pp. 177\u2013210. MIT Press, Cambridge (1997)"},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell.\u00a031(2), 125\u2013157 (1987)","journal-title":"Artif. Intell."},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0747-7171(08)80133-2","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation\u00a011, 83\u2013111 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-60043-4_68","volume-title":"Algebraic Methodology and Software Technology","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Subramaniam, M.: Automated reasoning about parallel algorithms using powerlists. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol.\u00a0936, pp. 416\u2013430. Springer, Heidelberg (1995)"},{"issue":"1-2","key":"20_CR18","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. J.\u00a0Automated Reasoning\u00a016(1-2), 39\u201378 (1996)","journal-title":"J.\u00a0Automated Reasoning"},{"issue":"2","key":"20_CR19","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1023\/A:1008610818519","volume":"13","author":"D. Kapur","year":"1998","unstructured":"Kapur, D., Subramaniam, M.: Mechanical verification of adder circuits using Rewrite Rule Laboratory. Formal Methods in System Design\u00a013(2), 127\u2013158 (1998)","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"20_CR20","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1145\/322217.322232","volume":"27","author":"R.E. Ladner","year":"1980","unstructured":"Ladner, R.E., Fischer, M.J.: Parallel prefix computation. Journal of the ACM\u00a027(4), 831\u2013838 (1980)","journal-title":"Journal of the ACM"},{"issue":"6","key":"20_CR21","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 Trans. Prog. Lang. Syst.\u00a016(6), 1737\u20131767 (1994)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1145\/567446.567461","volume-title":"Proc.\u00a0of POPL \u201980","author":"D.R. Musser","year":"1980","unstructured":"Musser, D.R.: On proving inductive properties of abstract data types. In: Proc.\u00a0of POPL \u201980, pp. 154\u2013162. ACM, New York (1980)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"9th International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E.R., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 162\u2013181. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:21Z","timestamp":1619785041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}