{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:40Z","timestamp":1749124060410},"publisher-location":"Berlin\/Heidelberg","reference-count":31,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012831","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"162-181","source":"Crossref","is-referenced-by-count":43,"title":["A mechanizable induction principle for equational specifications"],"prefix":"10.1007","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mukkai S.","family":"Krishnamoorthy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"Mechanizing structural induction","author":"J. Aubin","year":"1976","unstructured":"Aubin, J., Mechanizing structural induction. Ph.D. Thesis, University of Edinburgh, Edinburgh, 1976."},{"key":"12_CR2","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S. and Moore, J S., A computational logic. (Academic Press, New York, 1979)."},{"key":"12_CR3","volume-title":"Overview of a theorem-prover for a computational logic","author":"R.S. Boyer","year":"1986","unstructured":"Boyer, R.S. and Moore, J S., \u201cOverview of a theorem-prover for a computational logic,\u201d in: Proc. 8th Intl. Conf. on Automated Deduction (CADE-8), Oxford, U.K., 1986, LNCS, Springer-Verlag, NY."},{"key":"12_CR4","volume-title":"Proving theorems by mathematical induction","author":"D. Brotz","year":"1976","unstructured":"Brotz, D., Proving theorems by mathematical induction. Ph.D. Thesis, Computer Science Dept., Stanford University, Stanford 1976."},{"issue":"1","key":"12_CR5","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. Burstall","year":"1969","unstructured":"Burstall, R., \u201cProving properties of programs by structural induction,\u201d Computer Journal 12(1), 41\u201348, 1969.","journal-title":"Computer Journal"},{"key":"12_CR6","unstructured":"Dershowitz, N., Applications of the Knuth-Bendix Completion Procedure. Laboratory Operation, Aerosapce Corporation, Aerospace Report No. ATR-83(8478)-2, 15 May, 1983."},{"key":"12_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N., \u201cTermination of rewriting,\u201d J. of Symbolic Computation 3, 1987, 69\u2013116.","journal-title":"J. of Symbolic Computation"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., \u201cHow to prove algebraic inductive hypotheses without induction,\u201d Proc. of the Fifth Conference on Automated Deduction, 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"12_CR9","volume-title":"Data Structuring, Current Trends in Programming Methodology","author":"J.A. Goguen","year":"1978","unstructured":"Goguen, J.A., Thatcher, J.W. and Wagner, E.W., \u201cInitial algebra approach to the specification, correctness, and implementation of abstract data types,\u201d in: R.T. Yeh (ed.), Data Structuring, Current Trends in Programming Methodology, 4 (Prentice-Hall, Englewood Cliffs, NJ, 1978)."},{"key":"12_CR10","unstructured":"Guttag, J., The Specification and Application to Programming of Abstract Data Types. Department of Computer Science, Univ. of Toronto, Ph.D. Thesis, CSRG-59, 1975."},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"Guttag, J.V. and Homing, J.J., \u201cThe algebraic specification of abstract data types,\u201d Acta Informatica 10(1), 1978, 27\u201352.","journal-title":"Acta Informatica"},{"key":"12_CR12","unstructured":"Hsiang, J. and Dershowitz, N., \u201cRewrite methods for clausal and nonclausal theorem proving,\u201d in: Proc. Tenth EATCS, Inter. Collo. on Automata, Languages, and Programming, Barcelona, Spain, 1983."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Huet, G., \u201cConfluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,\u201d JACM 27(4), October 1980.","DOI":"10.1145\/322217.322230"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Huet, G. and Hullot, J.M., \u201cProofs by induction in equational theories with constructors,\u201d in: 21st IEEE Symposium on Foundations of Computer Science, Syracuse, NY. 1980, 96\u2013107.","DOI":"10.1109\/SFCS.1980.37"},{"key":"12_CR15","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G. and Oppen, D., \u201cEquations and rewrite rules: a survey,\u201d in: R. Book (ed.), Formal Languages: Perspectives and Open Problems, (Academic Press, New York, 1980)."},{"key":"12_CR16","unstructured":"Jouannaud, J.-P., and Kounalis, E., \u201cProofs by Induction in Equational Theories Without Constructors,\u201d in: Proc. of Logic in Computer Science Conference, Cambridge, MA, 1986."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Kanamori, T., Fujita, H., \u201cFormulation of induction formulas in verification of Prolog programs,\u201d Proc. of 8th Intl Conf. on Automated Deduction (CADE-8), Oxford, U.K., 1986.","DOI":"10.1007\/3-540-16780-3_97"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Kapur, D., and Musser, D.R., \u201cProof by Consistency,\u201d Proc. of an NSF Workshop on the Rewrite Rule Laboratory, Sept. 4\u20136, 1983. Schenectady, G.E. R&D Center Report GEN84008, April 1984. (also in Artificial Intelligence 31, 1987, 125\u201357).","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"12_CR19","unstructured":"Kapur, D., and Musser, D.R., \u201cInductive reasoning with incomplete specifications,\u201d in: Proc. of Logic in Computer Science Conference, Cambridge, MA, 1986."},{"key":"12_CR20","unstructured":"Kapur, D., Narendran, P., and Zhang, H., \u201cOn Sufficient Completeness and Related Properties of Term Rewriting Systems,\u201d Unpublished Manuscript, General Electric R&D Center, Schenectady, NY, Oct. 1985. To appear in Acta Informatica."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Kapur, D., Narendran, P., and Zhang, H., \u201cProof by induction using test sets,\u201d Proc. of 8th Intl Conf. on Automated Deduction (CADE-8), Oxford, U.K., 1986.","DOI":"10.1007\/3-540-16780-3_83"},{"key":"12_CR22","unstructured":"Kapur, D. and Sivakumar, G., \u201cExperiments with and Architecture of RRL, a Rewrite Rule Laboratory,\u201d Proc. of An NSF Workshop on the Rewrite Rule Lab., Sept. 1983. General Electric R&D Center Report 84GEN008, 33\u201356, April 1984."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Kapur, D., Sivakumar, G., and Zhang, H., \u201cRRL: A Rewrite Rule Laboratory,\u201d Proc. of 8th Intl Conf. on Automated Deduction (CADE-8), Oxford, U.K., 1986.","DOI":"10.1007\/3-540-16780-3_140"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Kirchner, H., \u201cA General Inductive Algorithm and Application to Abstract Data Types,\u201d Proc. 7th Intl. Conf. on Automated Deduction (CADE-7), LNCS 170, Springer-Verlag, May 1984.","DOI":"10.1007\/978-0-387-34768-4_17"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Knuth, D., and Bendix, P., \u201cSimple Word Problems in Universal Algebras,\u201d in: Leech (ed.) Computational Problems in Abstract Algebra, Pergamon Press, 1970, 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"12_CR26","volume-title":"A simple explanation of inductionless induction. MTP-14","author":"D.S. Lankford","year":"1981","unstructured":"Lankford, D.S., A simple explanation of inductionless induction. MTP-14, Louisiana Tech University, Ruston, LA, 1981."},{"key":"12_CR27","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/S0049-237X(08)72018-4","volume-title":"Computer Programming and Formal Systems","author":"J. McCarthy","year":"1963","unstructured":"McCarthy, John, \u201cA basis for a mathematical theory of computation,\u201d Computer Programming and Formal Systems, P. Braffort and d. Hirschberg [ed.], Norht-Holland, Amsterdam, 1963, 33\u201370."},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Musser, D.R., \u201cOn Proving Inductive Properties of Abstract Data Types,\u201d Proc. 7th Principles of Programming Languages, Las Vegas, Jan. 1980.","DOI":"10.1145\/567446.567461"},{"key":"12_CR29","first-page":"77","volume":"144","author":"D.R. Musser","year":"1982","unstructured":"Musser, D.R., and Kapur, D., \u201cRewrite Rule Theory and Abstract Data Type Analysis,\u201d EUROCAM 1982 LNCS 144 (ed. Calmet), Springer-Verlag, 77\u201390, April 1982.","journal-title":"EUROCAM 1982 LNCS"},{"key":"12_CR30","first-page":"211","volume-title":"Ninth Colloquium on Trees in Algebra and Programming","author":"E. Paul","year":"1984","unstructured":"Paul, E., \u201cProof by induction in equational theories with relations between constructors,\u201d in: B. Courcelle (ed.), Ninth Colloquium on Trees in Algebra and Programming, Bordeaux, France, 1984, 211\u2013215."},{"issue":"2","key":"12_CR31","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1145\/321941.321957","volume":"23","author":"B. Wegbreit","year":"1976","unstructured":"Wegbreit, B., and Spitzen, J.M., \u201cProving properties of complex data structures,\u201d JACM 23(2), 1976, 389\u2013396.","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012831","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:00Z","timestamp":1586579040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012831"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/bfb0012831","relation":{},"subject":[]}}