{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:00:43Z","timestamp":1725490843007},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_16","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"231-246","source":"Crossref","is-referenced-by-count":3,"title":["Improvements in Formula Generalization"],"prefix":"10.1007","author":[{"given":"Markus","family":"Aderhold","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"http:\/\/www.verifun.org"},{"key":"16_CR2","unstructured":"Aderhold, M.: Formula generalization in erifun. Diploma thesis, Technische Universit\u00e4t Darmstadt (2004)"},{"key":"16_CR3","unstructured":"Aderhold, M., Walther, C., Szallies, D., Schlosser, A.: A fast disprover for erifun. In: Ahrendt, W., Baumgartner, P., de Nivelle, H. (eds.) Proc. of the 3rd Workshop on Disproving, pp. 59\u201369 (2006)"},{"key":"16_CR4","unstructured":"Aubin, R.: Mechanizing Structural Induction. PhD thesis, University of Edinburgh (1976)"},{"key":"16_CR5","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J S.: A Computational Logic. Academic Press, San Diego (1979)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning, ch. 13","author":"A. Bundy","year":"2001","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 13, vol.\u00a0I, pp. 845\u2013911. Elsevier, Amsterdam (2001)"},{"key":"16_CR7","series-title":"ch. 3, no. 56","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"A. Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. In: Cambridge Tracts in Theoretical Computer Science. ch. 3, no. 56, Cambridge University Press, Cambridge (2005)"},{"key":"16_CR8","unstructured":"Dixon, L.: A Proof Planning Framework For Isabelle. PhD thesis, University of Edinburgh (2005)"},{"key":"16_CR9","unstructured":"Hummel, B.: Generierung von Induktionsformeln und Generalisierung beim automatischen Beweisen mit vollst\u00e4ndiger Induktion. Doctoral dissertation, Universit\u00e4t Karlsruhe (1990)"},{"key":"16_CR10","unstructured":"Kapur, D.: Theorem proving support for hardware verification. In: Third Intl. Workshop on First-Order Theorem Proving, (2000), Invited talk, paper available at http:\/\/www.cs.unm.edu\/~kapur\/myabstracts\/tphardware00.html"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/3-540-61511-3_112","volume-title":"Automated Deduction \u2013 CADE-13","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction \u2013 CADE-13. LNCS, vol.\u00a01104, pp. 538\u2013552. Springer, Heidelberg (1996)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction \u2013 CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction \u2013 CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"16_CR13","unstructured":"Schweitzer, S.: Symbolische Auswertung und Heuristiken zur Verifikation funktionaler Programme. Doctoral dissertation, TU Darmstadt (2007)"},{"key":"16_CR14","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., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013228. Oxford University Press, Oxford (1994)"},{"key":"16_CR15","unstructured":"Walther, C., Aderhold, M., Schlosser, A.: The L\u00a01.0 Primer. Technical Report VFR\u00a006\/01, Technische Universit\u00e4t Darmstadt (2006)"},{"key":"16_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-540-45085-6_28","volume-title":"Automated Deduction \u2013 CADE-19","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About eriFun. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 322\u2013327. Springer, Heidelberg (2003)"},{"issue":"1","key":"16_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/B:JARS.0000021872.64036.41","volume":"32","author":"C. Walther","year":"2004","unstructured":"Walther, C., Schweitzer, S.: Verification in the classroom. Journal of Automated Reasoning\u00a032(1), 35\u201373 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11591191_30","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Walther","year":"2005","unstructured":"Walther, C., Schweitzer, S.: Reasoning about incompletely defined programs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 427\u2013442. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T17:33:00Z","timestamp":1708191180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}