{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:42Z","timestamp":1725663882186},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:24:54Z","timestamp":1330251894000},"page":"102-117","source":"Crossref","is-referenced-by-count":8,"title":["Induction using term orderings"],"prefix":"10.1007","author":[{"given":"Francois","family":"Bronsard","sequence":"first","affiliation":[]},{"given":"Uday S.","family":"Reddy","sequence":"additional","affiliation":[]},{"given":"Robert W.","family":"Hasker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Proof by consistency in equational theories. In Proc. 3rd LICS Symp., Edinburgh (UK), pages 228\u2013233, 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"E. Bevers and J. Lewi. Proof by consistency in conditional equational theories. In S. Kaplan and M. Okada, editors, 2nd CTRS Workshop, LNCS, vol. 516, pages 195\u2013205. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54317-1_91"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"S. Biundo, B. Hummel, D. Hutter, and C. Walther. The Karlsruhe induction theorem proving system. In 8th CADE Conf., LNCS, vol. 230. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_132"},{"key":"8_CR4","first-page":"88","volume-title":"Proc. 13th IJCAI Conf.","author":"A. Bouhoula","year":"1993","unstructured":"Adel Bouhoula and Micha\u00cbl Rusinowitch. Automatic case analysis in proof by induction. In Ruzena Bajcsy, editor, Proc. 13th IJCAI Conf., Chamb\u00e9ry (France), volume 1, pages 88\u201394. Morgan Kaufmann, August 1993"},{"key":"8_CR5","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979."},{"key":"8_CR6","series-title":"LNCS, vol. 449","first-page":"1","volume-title":"Proc. 10th CADE Conf.","author":"R. S. Boyer","year":"1990","unstructured":"R. S. Boyer and J. S. Moore. A theorem prover for a computational logic. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), LNCS, vol. 449, pages 1\u201315. Springer-Verlag, 1990"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"F. Bronsard and U. S. Reddy. Conditional rewriting in Focus. In S. Kaplan and M. Okada, editors, 2nd CTRS Workshop, LNCS, vol. 516, pages 2-13. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54317-1_77"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"F. Bronsard and U. S. Reddy. Reduction techniques for first-order reasoning. In M. Rusinowitch and J. L. R\u00e9my, editors, 3rd CTRS Workshop, LNCS, vol. 656, pages 242\u2013256. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-56393-8_18"},{"key":"8_CR9","unstructured":"A. Bundy. A rational reconstruction and extension of recursion analysis. In IJCAI, 1989."},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. M. Burstall","year":"1969","unstructured":"R. M. Burstall. Proving properties of programs by structural induction. Computer Journal, 12:41\u201348, 1969.","journal-title":"Computer Journal"},{"key":"8_CR11","series-title":"volume 2: Rewriting Techniques","first-page":"31","volume-title":"Resolution of Equations in Algebraic Structures","author":"N. Dershowitz","year":"1989","unstructured":"N. Dershowitz. Completion and its applications. In Resolution of Equations in Algebraic Structures, volume 2: Rewriting Techniques, pages 31\u201386. Academic Press, San Diego, 1989."},{"key":"8_CR12","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"issue":"8","key":"8_CR13","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Comm. ACM, 22(8):465\u2013476, August 1979.","journal-title":"Comm. ACM"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"S. J. Garland and J. V Guttag. Inductive methods for reasoning about abstract data types. In ACM POPL Symp., pages 219\u2013228. ACM, 1988.","DOI":"10.1145\/73560.73579"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"J. A. Goguen. How to prove inductive hypotheses without induction. In 5th CADE Conf., LNCS, vol. 87, pages 356\u2013372. Springer Verlag, Jul 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"8_CR16","series-title":"Technical Report SR-89-14","volume-title":"ECAI","author":"B. Gramlich","year":"1989","unstructured":"B. Gramlich. Induction theorem proving using refined unfailing completion techniques. In ECAI, 1989. (also vailable as Technical Report SR-89-14, Universit\u00e4t Kaiserslautern, Germany.)."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"D. Hofbauer and R. D. Kutsche. Proving inductive theorems based on term rewriting systems. In J. Grabowski, P. Lescanne, and W. Wechler, editors, Proc. 1st ALP Workshop, pages 180\u2013190. Akademie Verlag, 1988.","DOI":"10.1007\/3-540-50667-5_70"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. J. Comp. and System Sciences, 25:239\u2013266, 1982.","journal-title":"J. Comp. and System Sciences"},{"key":"8_CR19","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. Automatic proofs by induction in equational theories without constructors. Information and Computation, 82:1\u201333, 1989.","journal-title":"Information and Computation"},{"issue":"2","key":"8_CR20","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"D. Kapur and D. R. Musser. Proof by consistency. Artificial Intelligence, 31(2):125\u2013157, February 1987.","journal-title":"Artificial Intelligence"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0747-7171(08)80133-2","volume":"11","author":"D. Kapur","year":"1991","unstructured":"D. Kapur, P. Narendran, and H. Zhang. Automating inductionless induction using test sets. J. Symbolic Computation, 11:83\u2013112, 1991.","journal-title":"J. Symbolic Computation"},{"key":"8_CR22","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"8_CR23","unstructured":"E. Kounalis and M. Rusinowitch. Mechanizing inductive reasoning. In Proc. AAAI Conf., pages 240\u2013245. AAAI Press and MIT Press, July 1990."},{"key":"8_CR24","unstructured":"R. Kowalski. Studies in the completeness and efficiency of theorem-proving by resolution. PhD thesis, University of Edinburgh, 1970."},{"key":"8_CR25","unstructured":"D. McAllester. Term rewriting induction. theorem-provers@ai.mit.edu electronic bulletin board, 1990."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"D. R. Musser. On proving inductive properties of abstract data types. In ACM POPL Symp., pages 154\u2013162. ACM, 1980.","DOI":"10.1145\/567446.567461"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"U. S. Reddy. Term rewriting induction. In M. Stickel, editor, 10th CADE Conf., volume 449 of LNAI, pages 162\u2013177. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_86"},{"key":"8_CR28","volume-title":"Th. Etat","author":"J. R\u00e9my","year":"1982","unstructured":"Jean-Luc R\u00e9my. Etude des syst\u00e8mes de R\u00e9\u00e9criture Conditionnels et Applications aux Types Abstraits Alg\u00e9briques. Th. Etat, INPL, Nancy (France), 1982."},{"key":"8_CR29","unstructured":"G. A. Robinson and L. T. Wos. Paramodulation and first-order theorem proving. In B. Meltzer and D. Mitchie, editors, Machine Intelligence 4, pages 135\u2013150. Edinburgh University Press, 1969."},{"key":"8_CR30","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12:23\u201341, 1965.","journal-title":"J. ACM"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"C.-P. Wirth and B. Gramlich. On notions of inductive validity for first-order equational clauses. In 12th CADE Conf., 1994.","DOI":"10.1007\/3-540-58156-1_12"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In E. Lusk and R. Overbeek, editors, 9th CADE Conf., LNCS, vol. 310, pages 162\u2013181. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012831"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:17:48Z","timestamp":1605629868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}