{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:08Z","timestamp":1725664448611},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540587156"},{"type":"electronic","value":"9783540490548"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58715-2_144","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:42:09Z","timestamp":1330274529000},"page":"438-449","source":"Crossref","is-referenced-by-count":1,"title":["Using linear arithmetic procedure for generating induction schemes"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"M.","family":"Subramaniam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"36_CR1","unstructured":"R.S. Boyer and J S. Moore, A Computational Logic. ACM Monographs in Computer Science, 1979."},{"key":"36_CR2","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J. S. Moore, A Computational Logic Handbook. New York: Academic Press, 1988."},{"key":"36_CR3","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J. S. Moore, \u201cIntegrating decision procedures into heuristic theorem provers: A case study of linear arithmetic,\u201d Machine Intelligence 11 (1988) 83\u2013157.","journal-title":"Machine Intelligence"},{"key":"36_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz, \u201cTermination of rewriting,\u201d J. Symbolic Computation 3, 69\u2013116, 1987.","journal-title":"J. Symbolic Computation"},{"key":"36_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"J.-P. Jouannaud and E. Kounalis, \u201cAutomatic proofs by induction in theories without constructors,\u201d Information and Computation 82, 1\u201333, 1989.","journal-title":"Information and Computation"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"D. Kapur, \u201cAn automated tool for analyzing completeness of equational specifications,\u201d Proc. of 1994 International Symposiumm on Software Testing and Analysis (ISSTA), Seattle, August 1994, 28\u201343.","DOI":"10.1145\/186258.186496"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"D. Kapur, D.R. Musser, and X. Nie, \u201cAn Overview of the Tecton Proof System,\u201d to appear in Theoretical Computer Science Journal, special issue on Formal Methods in Databases and Soft. Engg, (ed. V. Alagar), Vol. 133, October, 1994.","DOI":"10.1016\/0304-3975(94)90192-9"},{"key":"36_CR8","unstructured":"D. Kapur and X. Nie, \u201cReasoning about numbers in Tecton,\u201d Dept. Tech. Report, March 1994. Accepted at ISMIS'94, October 1994."},{"key":"36_CR9","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"D. Kapur, P. Narendran, D. Rosenkrantz, H. Zhang., \u201cSufficient-completeness, quasi-reducibility and their complexity,\u201d Acta Informatica, 28, 1991, 311\u2013350.","journal-title":"Acta Informatica"},{"key":"36_CR10","series-title":"Tech. Report","volume-title":"New Uses of Linear Arithmetic in Automated Theorem Proving by Induction","author":"D. Kapur","year":"1994","unstructured":"D. Kapur and M. Subramaniam, New Uses of Linear Arithmetic in Automated Theorem Proving by Induction, Tech. Report, Dept. of Computer Science, State University of New York, Albany, Aug. 1994."},{"key":"36_CR11","unstructured":"D. Kapur and H. Zhang, \u201cAn overview of Rewrite Rule Laboratory (RRL),\u201d to appear in a special issue of Computers in Math. with Applications, 1994. Earlier descriptions in CADE-88 and RTA-89."},{"key":"36_CR12","series-title":"Ph.D. Thesis","volume-title":"Reduction, superposition and induction: automated reasoning in an equational logic","author":"H. Zhang","year":"1988","unstructured":"H. Zhang, Reduction, superposition and induction: automated reasoning in an equational logic. Ph.D. Thesis, Department of Computer Science, RPI, Troy, NY, 1988."},{"key":"36_CR13","first-page":"250","volume-title":"Proc. of (CADE-9)","author":"H. Zhang","year":"1988","unstructured":"H. Zhang, D. Kapur, and M.S. Krishnamoorthy, \u201cA mechanizable induction principle for equational specifications,\u201d Proc. of (CADE-9), Argonne, IL. Springer-Verlag LNCS 310, 250\u2013265, 1988."}],"container-title":["Lecture Notes in Computer Science","Foundation of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58715-2_144.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:23:48Z","timestamp":1605648228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58715-2_144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540587156","9783540490548"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-58715-2_144","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}