{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:26:23Z","timestamp":1725549983105},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540289319"},{"type":"electronic","value":"9783540318224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11554554_20","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:02:57Z","timestamp":1127829777000},"page":"262-276","source":"Crossref","is-referenced-by-count":6,"title":["Automatic \u2018Descente Infinie\u2019 Induction Reasoning"],"prefix":"10.1007","author":[{"given":"Sorin","family":"Stratulat","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-44802-0_36","volume-title":"Computer Science Logic","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 513\u2013527. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Avenhaus, J., Madlener, K.: Theorem proving in hierarchical clausal specifications. Advances in Algorithms, Languages, and Complexity, 1\u201351 (1997)","key":"20_CR2","DOI":"10.1007\/978-1-4613-3394-4_1"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Proof by consistency in equational theories. In: Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh, UK, pp. 228\u2013233 (1988)","key":"20_CR3","DOI":"10.1109\/LICS.1988.5122"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, pp. 19\u201399 (2001)","key":"20_CR4","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/BFb0053582","volume-title":"Fundamental Approaches to Software Engineering","author":"N. Berregeb","year":"1998","unstructured":"Berregeb, N., Bouhoula, A., Rusinowitch, M.: Observational proofs with critical contexts. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol.\u00a01382, pp. 38\u201353. Springer, Heidelberg (1998)"},{"issue":"170","key":"20_CR6","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/S0304-3975(96)80708-0","volume":"1-2","author":"A. Bouhoula","year":"1996","unstructured":"Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science\u00a01-2(170), 245\u2013276 (1996)","journal-title":"Theoretical Computer Science"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. Journal of Symbolic Computation\u00a023, 47\u201377 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR8","first-page":"3","volume":"16","author":"F. Bronsard","year":"1996","unstructured":"Bronsard, F., Reddy, U., Hasker, R.W.: Induction using term orders. Journal of Symbolic Computation\u00a016, 3\u201337 (1996)","journal-title":"Journal of Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. Handbook of Automated Reasoning, pp. 913\u2013970 (2001)","key":"20_CR9","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"issue":"3","key":"20_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science\u00a017(3), 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/S0747-7171(08)80133-2","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of symbolic Computation\u00a011, 83\u2013112 (1991)","journal-title":"Journal of symbolic Computation"},{"key":"20_CR12","first-page":"216","volume":"41","author":"E. Kounalis","year":"1990","unstructured":"Kounalis, E., Rusinowitch, M.: Mechanizing inductive reasoning. Bulletin of European Association for Theoretical Computer Science\u00a041, 216\u2013226 (1990)","journal-title":"Bulletin of European Association for Theoretical Computer Science"},{"unstructured":"Kounalis, E., Rusinowitch, M.: Studies on the ground convergence property of conditional theories. In: AMAST 1991, pp. 363\u2013376 (1991)","key":"20_CR13"},{"unstructured":"Lankford, D.S.: Some remarks on inductionless induction. Technical Report MTP-11, Louisiana Tech University, Ruston, LA (1980)","key":"20_CR14"},{"unstructured":"Naidich, D.: On generic representation of implicit induction procedures. Technical Report CS-R9620, CWI (1996)","key":"20_CR15"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, pp. 371\u2013443 (2001)","key":"20_CR16","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","first-page":"162","volume-title":"Automated Deduction - CADE-12","author":"U. Reddy","year":"1994","unstructured":"Reddy, U.: Term rewriting induction. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 162\u2013177. Springer, Heidelberg (1994)"},{"issue":"4","key":"20_CR18","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1006\/jsco.2000.0469","volume":"32","author":"S. Stratulat","year":"2001","unstructured":"Stratulat, S.: A general framework to build contextual cover set induction provers. Journal of Symbolic Computation\u00a032(4), 403\u2013445 (2001)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"20_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C.-P. Wirth","year":"2004","unstructured":"Wirth, C.-P.: Descente Infinie + Deduction. Logic Journal of the IGPL\u00a012(1), 1\u201396 (2004)","journal-title":"Logic Journal of the IGPL"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60381-6_21","volume-title":"Conditional and Typed Rewriting Systems","author":"C.-P. Wirth","year":"1995","unstructured":"Wirth, C.-P., Becker, K.: Abstract notions and inference systems for proofs by mathematical induction. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 353\u2013373. Springer, Heidelberg (1995)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0012831","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. 162\u2013181. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11554554_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:46:45Z","timestamp":1605642405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11554554_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540289319","9783540318224"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11554554_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}