{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:28Z","timestamp":1725568168501},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_29","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"328-333","source":"Crossref","is-referenced-by-count":5,"title":["How to Prove Inductive Theorems? QuodLibet!"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Avenhaus","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"K\u00fchler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Schmidt-Samoa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus-Peter","family":"Wirth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","first-page":"228","volume-title":"3rd IEEE symposium on Logic In Computer Sci.","author":"L. Bachmair","year":"1988","unstructured":"Bachmair, L.: Proof By Consistency in Equational Theories. In: 3rd IEEE symposium on Logic In Computer Sci., pp. 228\u2013233. IEEE Press, Los Alamitos (1988)"},{"key":"29_CR2","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Strother Moore, J.: A Computational Logic Handbook. Academic Press, London (1988)"},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(94)90192-9","volume":"133","author":"D. Kapur","year":"1994","unstructured":"Kapur, D., Musser, D.R., Nie, X.: An Overview of the Tecton Proof System. Theoretical Computer Sci.\u00a0133, 307\u2013339 (1994)","journal-title":"Theoretical Computer Sci."},{"key":"29_CR4","unstructured":"K\u00fchler, U.: A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Ph.D. thesis, Infix, Sankt Augustin (2000)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/3-540-62950-5_60","volume-title":"Rewriting Techniques and Applications","author":"U. K\u00fchler","year":"1997","unstructured":"K\u00fchler, U., Wirth, C.-P.: Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 38\u201352. Springer, Heidelberg (1997)"},{"key":"29_CR6","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-58156-1_4","volume-title":"Automated Deduction - CADE-12","author":"M. Protzen","year":"1994","unstructured":"Protzen, M.: Lazy Generation of Induction Hypotheses. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 42\u201356. Springer, Heidelberg (1994)"},{"key":"29_CR7","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/oso\/9780198537465.003.0003","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"C. Walther","year":"1994","unstructured":"Walther, C.: Mathematical Induction. In: Gabbay, D.M., Hogger, C.J., Alan Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013228, 1993. Clarendon Press, Oxford (1994)"},{"key":"29_CR8","unstructured":"Wirth, C.-P.: Descente Infinie + Deduction. Report 737\/2000, FB Informatik, Univ. Dortmund. Extd. version, November 17 (December 02, 2002), http:\/\/ags.uni-sb.de\/~cp\/p\/tab99\/new.html"},{"key":"29_CR9","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1006\/jsco.1994.1004","volume":"17","author":"C.-P. Wirth","year":"1994","unstructured":"Wirth, C.-P., Gramlich, B.: A Constructor-Based Approach for Positive\/Negative-Conditional Equational Specifications. J. Symbolic Computation\u00a017, 51\u201390 (1994)","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,31]],"date-time":"2024-03-31T20:35:02Z","timestamp":1711917302000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}