{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:26Z","timestamp":1749124046261},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1996,3,1]],"date-time":"1996-03-01T00:00:00Z","timestamp":825638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1996,3]]},"DOI":"10.1007\/bf00244458","type":"journal-article","created":{"date-parts":[[2004,9,17]],"date-time":"2004-09-17T22:43:55Z","timestamp":1095461035000},"page":"3-37","source":"Crossref","is-referenced-by-count":5,"title":["Induction using term orders"],"prefix":"10.1007","volume":"16","author":[{"given":"Francois","family":"Bronsard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uday S.","family":"Reddy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert W.","family":"Hasker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF00244458_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Proof by consistency in equational theories, in Proc. 3rd LICS Symp., 1988, pp. 228\u2013233.","DOI":"10.1109\/LICS.1988.5122"},{"key":"BF00244458_CR2","first-page":"1","volume-title":"Resolutions of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, Chapter 1","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., and Plaisted, D. A.: Completion without failure, in H.A\u00eft-Kaci and M.Nivat (eds), Resolutions of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, Chapter 1, Academic Press, New York, 1989, pp. 1\u201330."},{"key":"BF00244458_CR3","doi-asserted-by":"crossref","unstructured":"Biundo, S., Hummel, B., Hutter, D., and Walther, C.: The Karlsruhe induction theorem proving system, in 8th CADE Conf., LNCS 230, Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_132"},{"key":"BF00244458_CR4","unstructured":"Bouhoula, A. and Rusinowitch, M.: Automatic case analysis in proof by induction, in R. Bajcsy (ed.), Proc. 13th IJCAI Conf., Vol. 1, Morgan Kaufmann, August 1993, pp. 88\u201394."},{"key":"BF00244458_CR5","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":"BF00244458_CR6","doi-asserted-by":"crossref","unstructured":"Boyer, R. S. and Moore, J. S.: A theorem prover for a computational logic, in M. E. Stickel (ed.), Proc. 10th CADE Conf., LNCS 449, Springer-Verlag, 1990, pp. 1\u201315.","DOI":"10.1007\/3-540-52885-7_75"},{"key":"BF00244458_CR7","unstructured":"Bronsard, F.: Using term ordering to control clausal deductions, PhD thesis, University of Illinois, Urbana, 1995."},{"key":"BF00244458_CR8","doi-asserted-by":"crossref","unstructured":"Bronsard, F. and Reddy, U. S.: Conditional rewriting in Focus, in S. Kaplan and M. Okada (eds), Proc. 2nd CTRS Workshop, LNCS 516, Springer-Verlag, 1991, pp. 2\u201313.","DOI":"10.1007\/3-540-54317-1_77"},{"key":"BF00244458_CR9","doi-asserted-by":"crossref","unstructured":"Bronsard, F. and Reddy, U. S.: Reduction techniques for first-order reasoning, in M. Rusinowitch and J. L. R\u00e9my (eds), Proc. 3rd CTRS Workshop, LNCS 656, Springer-Verlag, 1992, pp. 242\u2013256.","DOI":"10.1007\/3-540-56393-8_18"},{"key":"BF00244458_CR10","doi-asserted-by":"crossref","unstructured":"Bronsard, F., Reddy, U. S., and Hasker, R. W.: Induction using term orderings, in Alan Bundy (ed.), Proc. 12th CADE Conf., LNAI 814, Springer-Verlag, 1994, pp. 102\u2013117.","DOI":"10.1007\/3-540-58156-1_8"},{"key":"BF00244458_CR11","doi-asserted-by":"crossref","unstructured":"Bundy, A.: A rational reconstruction and extension of recursion analysis, in IJCAI, 1989.","DOI":"10.2307\/1073174"},{"key":"BF00244458_CR12","first-page":"31","volume-title":"Resolution of Equations in Algebraic Structures","author":"N. Dershowitz","year":"1989","unstructured":"Dershowitz, N.: Completion and its applications, in Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, Academic Press, San Diego, 1989, pp. 31\u201386."},{"key":"BF00244458_CR13","unstructured":"Dershowitz, N. and Hoot, C.: Natural termination, in C. Kirchner (ed.), Proc. 5th RTA Conf., LNCS 690, Montreal (Canada), Springer-Verlag, 1993, pp. 405\u2013420."},{"key":"BF00244458_CR14","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N. and Jouannaud, J.-P.: Rewrite systems, in J.vanLeeuwen (ed.), Handbook of Theoretical Computer Science B: Formal Methods and Semantics, Chapter 6, North-Holland, Amsterdam, 1990, pp. 243\u2013320."},{"issue":"3","key":"BF00244458_CR15","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Fribourg, L.: A strong restriction of the inductive completion procedure, J. Symbolic Computation, 8(3) (1989), 253\u2013276.","journal-title":"J. Symbolic Computation"},{"key":"BF00244458_CR16","doi-asserted-by":"crossref","unstructured":"Goguen, J. A.: How to prove inductive hypotheses without induction, in 5th CADE Conf., LNCS 87, Springer-Verlag, 1980, pp. 356\u2013372.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"BF00244458_CR17","series-title":"Technical Report SR-89-14","volume-title":"ECAI","author":"B. Gramlich","year":"1989","unstructured":"Gramlich, B.: Induction theorem proving using refined unfailing completion techniques, in ECAI, 1989 (also Technical Report SR-89\u201314, Universit\u00e4t Kaiserslautern, Germany)."},{"key":"BF00244458_CR18","doi-asserted-by":"crossref","unstructured":"Hofbauer, D. and Kutsche, R. D.: Proving inductive theorems based on term rewriting systems, in J. Grabowski, P. Lescanne, and W. Wechler (eds), Proc. 1st ALP Workshop, Akademie Verlag, 1988, pp. 180\u2013190.","DOI":"10.1007\/3-540-50667-5_70"},{"key":"BF00244458_CR19","doi-asserted-by":"crossref","unstructured":"Hsiang, J. and Rusinowitch, M.: On word problems in equational theories, in T. Ottmann (ed.), 14th Intern. Colloq. Automata, Languages and Programming, LNCS 267, Springer-Verlag, July 1987, pp. 54\u201371.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"BF00244458_CR20","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G. and Hullot, J.-M.: Proofs by induction in equational theories with constructors, J. of Computer and System Sciences 25 (1982), 239\u2013266.","journal-title":"J. of Computer and System Sciences"},{"key":"BF00244458_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"Jouannaud, J.-P. and Kounalis, E.: Automatic proofs by induction in equational theories without constructors, Information and Computation 82 (1989), 1\u201333. Original version in Symp. LICS, IEEE, 1986.","journal-title":"Information and Computation"},{"issue":"2","key":"BF00244458_CR22","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D. and Musser, D. R.: Proof by consistency, Artificial Intelligence 31(2) (Feb. 1987), 125\u2013157.","journal-title":"Artificial Intelligence"},{"key":"BF00244458_CR23","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0747-7171(08)80133-2","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., and Zhang, H.: Automating inductionless induction using test sets, J. Symbolic Computation 11 (1991), 83\u2013112.","journal-title":"J. Symbolic Computation"},{"key":"BF00244458_CR24","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D. and Bendix, P.: Simple word problems in universal algebras, in J.Leech (ed.), Computational Problems in Abstract Algebra, Pergamon, Oxford, 1970, pp. 263\u2013297."},{"key":"BF00244458_CR25","first-page":"240","volume-title":"Proc. AAAI Conf.","author":"E. Kounalis","year":"1990","unstructured":"Kounalis, E. and Rusinowitch, M.: Mechanizing inductive reasoning, in Proc. AAAI Conf., AAAI Press and MIT Press, Boston, 1990, pp. 240\u2013245."},{"key":"BF00244458_CR26","unstructured":"Kowalski, R.: Studies in the completeness and efficiency of theorem-proving by resolution, PhD thesis, University of Edinburgh, 1970."},{"key":"BF00244458_CR27","first-page":"211","volume-title":"Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques","author":"W. K\u00fcchlin","year":"1989","unstructured":"K\u00fcchlin, W.: Inductive completion by ground proof transformation, in H.A\u00eft-Kaci and M.Nivat (eds), Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, Academic Press, San Diego, 1989, pp. 211\u2013245."},{"key":"BF00244458_CR28","unstructured":"Lankford, D. S.: A simple explanation of inductionless induction, Memo MTP-14, Dept. of Mathematics, Louisiana Tech. Univ., August 1981."},{"key":"BF00244458_CR29","unstructured":"McAllester, D.: Term rewriting induction, theorem-provers@ai.mit.edu electronic bulletin board, 1990."},{"key":"BF00244458_CR30","doi-asserted-by":"crossref","unstructured":"Musser, D. R.: On proving inductive properties of abstract data types, in ACM Symp. on Princ. of Program. Lang., ACM, 1980, pp. 154\u2013162.","DOI":"10.1145\/567446.567461"},{"key":"BF00244458_CR31","doi-asserted-by":"crossref","unstructured":"Reddy, U. S.: Term rewriting induction, in M. Stickel (ed.), 10th CADE Conf., LNAI 449, Springer-Verlag, 1990, pp. 162\u2013177.","DOI":"10.1007\/3-540-52885-7_86"},{"key":"BF00244458_CR32","unstructured":"R\u00e9my, J.-L.: Etude des Syst\u00e8mes de R\u00e9\u00e9criture Conditionnels et Applications aux Types Abstraits Alg\u00e9briques, Th. Etat, INPL, Nancy (France), 1982."},{"key":"BF00244458_CR33","unstructured":"Robinson, G. A. and Wos, L. T.: Paramodulation and first-order theorem proving, in B. Meltzer and D. Mitchie (eds), Machine Intelligence 4, Edinburgh University Press, 1969, pp. 135\u2013150."},{"key":"BF00244458_CR34","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine-oriented logic based on the resolution principle, JACM 12 (1965), 12\u201323.","journal-title":"JACM"},{"key":"BF00244458_CR35","unstructured":"Rouyer, J. and Lescanne, P.: Verification and programming of first-order unification in the calculus of constructions with inductive types, November 1992."},{"key":"BF00244458_CR36","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/BF02945004","volume":"2","author":"A. Selman","year":"1972","unstructured":"Selman, A.: Completeness of calculi for axiomatically defined classes of algebras, Algebra Universalis 2 (1972), 20\u201332.","journal-title":"Algebra Universalis"},{"key":"BF00244458_CR37","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P. and Gramlich, B.: On notions of inductive validity for first-order equational clauses, in 12th CADE Conf., LNCS 814, Springer-Verlag, 1994, pp. 162\u2013176.","DOI":"10.1007\/3-540-58156-1_12"},{"key":"BF00244458_CR38","doi-asserted-by":"crossref","unstructured":"Zhang, H. and Kapur, D., and Krishnamoorthy, M. S.: A mechanizable induction principle for equational specifications, in E. Lusk and R. Overbeek (eds), 9th CADE Conf., LNCS 310, Springer-Verlag, 1988, pp. 162\u2013181.","DOI":"10.1007\/BFb0012831"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00244458.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00244458\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00244458","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T05:05:22Z","timestamp":1585890322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00244458"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":38,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["BF00244458"],"URL":"https:\/\/doi.org\/10.1007\/bf00244458","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}