{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:02Z","timestamp":1725475802029},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_26","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"324-345","source":"Crossref","is-referenced-by-count":9,"title":["Extending Decision Procedures with Induction Schemes"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"Mahadavan","family":"Subramaniam","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Gupta, A.: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. Ph.D. Thesis, Department of Computer Sci- ence, Carnegie Mellon University, Pittsburgh (1994)"},{"key":"26_CR2","unstructured":"Boyer, R.S., Moore, J S.: A Computational Logic. ACM Monographs in Computer Science (1979)"},{"key":"26_CR3","unstructured":"Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Hayes, J.E., Mitchie, D., Richards, J. (eds.) Machine Intelligence, vol.\u00a011 (1988)"},{"key":"26_CR4","unstructured":"Fribourg, L.: Mixing list recursion and arithmetic. In: Proc. Seventh Symp. on Logic in Computer Science (1992)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. Technical Report, Department of Computer Science, University of New Mexico (February 2000)","DOI":"10.1007\/3-540-45744-5_41"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Automated tools for analyzing completeness of specifications. In: Proc. 1994 Intl. Symp. on Software Testing and Analysis (ISSTA), Seattle, WA, August 1994, pp. 28\u201343 (1994)","DOI":"10.1145\/186258.186496"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028393","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Rewriting, decision procedures and lemma speculation for automated hardware verification. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275. Springer, Heidelberg (1997)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Methodologies for Intelligent Systems","author":"D. Kapur","year":"1994","unstructured":"Kapur, D., Nie, X.: Reasoning about numbers in Tecton. In: Ra\u015b, Z.W., Zemankova, M. (eds.) ISMIS 1994. LNCS, vol.\u00a0869. Springer, Heidelberg (1994)"},{"issue":"1-2","key":"26_CR9","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 inductive theorem proving. J. Automated Reasoning\u00a016(1-2), 39\u201378 (1996)","journal-title":"J. Automated Reasoning"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-61474-5_64","volume-title":"Computer Aided Verification","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: Mechanically verifying a family of multiplier circuits. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 135\u2013146. Springer, Heidelberg (1996)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0058026","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D. Kapur","year":"1997","unstructured":"Kapur, D., Subramaniam, M.: Mechanizing reasoning about arithmetic circuits: SRT division. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol.\u00a01346, p. 103. Springer, Heidelberg (1997)"},{"key":"26_CR12","unstructured":"Kapur, D., Subramaniam, M.: Mechanical verification of adder circuits using powerlists. J. of Formal Methods in System Design (November 1998)"},{"key":"26_CR13","volume-title":"J. of Software Tools for Technology Transfer","author":"D. Kapur","year":"1999","unstructured":"Kapur, D., Subramaniam, M.: Using an induction prover for verifying arithmetic circuits. J. of Software Tools for Technology Transfer. Springer (1999) (to appear)"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Zhang, H.: An overview of Rewrite Rule Laboratory (RRL). J. of Computer and Mathematics with Applications\u00a029(2), 91\u2013114 (1995)","journal-title":"J. of Computer and Mathematics with Applications"},{"key":"26_CR15","unstructured":"Subramaniam, M.: Failure Analyses in Inductive Theorem Provers. Ph.D. Thesis, Department of Computer Science, University at Albany, State University of New York (1997)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","first-page":"250","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. Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 250\u2013265. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:31:17Z","timestamp":1558294277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/10721959_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}