{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:41Z","timestamp":1725663821449},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_13","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:20:59Z","timestamp":1330269659000},"page":"177-191","source":"Crossref","is-referenced-by-count":1,"title":["A new application for explanation-based generalisation within automated deduction"],"prefix":"10.1007","author":[{"given":"S.","family":"Baker","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"unstructured":"Aubin, R.: Some generalization heuristics in proofs by induction. In G. Huet and G. Kahn, editors, Actes du Colloque Construction: Am\u00e9lioration et v\u00e9rification de Programmes. Institut de recherche d'informatique et d'automatique (1975)","key":"13_CR1"},{"unstructured":"Baker, S.: Aspects of the Constructive Omega Rule within Automated Deduction. PhD thesis, University of Edinburgh (1992)","key":"13_CR2"},{"key":"13_CR3","first-page":"214","volume-title":"Lecture Notes in Artificial Intelligence","author":"S. Baker","year":"1992","unstructured":"Baker, S., Ireland, A., Smaill, A.: On the use of the constructive omega rule within automated deduction. In A. Voronkov, editor, International Conference on Logic Programming and Automated Reasoning \u2014 LPAR 92, St. Petersburg, Lecture Notes in Artificial Intelligence, Springer-Verlag 624 (1992) 214\u2013225"},{"unstructured":"Boyer, R.S., Moore, J.S.: Proving theorems about LISP functions. In N. Nilsson, editor, Proceedings of the third IJCAI (1973) 486\u2013493","key":"13_CR4"},{"unstructured":"Castaing, J.: How to facilitate the proof of theorems by using induction-matching, and by generalisation. In A. Joshi, editor, Proceedings of the ninth IJCAI (1985) 1208\u20131213","key":"13_CR5"},{"key":"13_CR6","volume-title":"Oxford Logic Guides","author":"M. Dummett","year":"1977","unstructured":"Dummett, M.: Elements of Intuitionism. Oxford Logic Guides. Oxford Univ. Press, Oxford (1977)"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"259","DOI":"10.2307\/2964649","volume":"27","author":"S. Feferman","year":"1962","unstructured":"Feferman, S.: Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic 27 (1962) 259\u2013316","journal-title":"Journal of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"Gordon, M: HOL: A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis Kluwer (1988)","key":"13_CR8","DOI":"10.1007\/978-1-4613-2007-4_3"},{"doi-asserted-by":"crossref","unstructured":"Hagiya, M.: A Typed A-Calculus for Proving-by-Example and Bottom-Up Generalisation Procedure. Algorithmic Learning Theory 93, Lecture Notes in Artificial Intelligence 744 (1993)","key":"13_CR9","DOI":"10.1007\/3-540-57370-4_38"},{"unstructured":"Hesketh, J.T.: Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, University of Edinburgh (1991)","key":"13_CR10"},{"key":"13_CR11","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2307\/2267457","volume":"17","author":"G. Kreisel","year":"1952","unstructured":"Kreisel, G.: On the Interpretation of Non-Finitist Proofs. Journal of Symbolic Logic 17 (1952) 43\u201358","journal-title":"Journal of Symbolic Logic"},{"unstructured":"Madden, P.: The specialization and transformation of constructive existence proofs. In Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, Morgan Kaufmann (1989)","key":"13_CR12"},{"unstructured":"Mitchell, T.M.: Toward combining empirical and analytical methods for inferring heuristics. Technical Report LCSR-TR-27, Laboratory for Computer Science Research, Rutgers University (1982)","key":"13_CR13"},{"unstructured":"Plotkin, G.: A note on inductive generalization. In D. Michie and B. Meltzer, editors, Machine Intelligence 5 Edinburgh University Press (1969) 153\u2013164","key":"13_CR14"},{"key":"13_CR15","first-page":"129","volume":"2","author":"B. Rosser","year":"1937","unstructured":"Rosser, B.: G\u00f6del-theorems for non-constructive logics. JSL 2 (1937) 129\u2013137","journal-title":"JSL"},{"unstructured":"Rouveirol, C.: Saturation: Postponing choices when inverting resolution. In Proceedings of ECAI-90 (1990) 557\u2013562","key":"13_CR16"},{"key":"13_CR17","first-page":"405","volume":"7","author":"J. R. Shoenfield","year":"1959","unstructured":"Shoenfield, J.R.: On a restricted \u03a9-rule. Bull. Acad. Sc. Polon. Sci., Ser. des sc. math., astr. et phys. 7 (1959) 405\u20137","journal-title":"Bull. Acad. Sc. Polon. Sci., Ser. des sc. math., astr. et phys."},{"unstructured":"Takeuti, G.: Proof theory. North-Holland, 2 edition (1987)","key":"13_CR18"},{"key":"13_CR19","first-page":"252","volume-title":"Papers presented to Richard Rado on the occasion of his sixty-fifth birthday","author":"B. L. Waerden Van der","year":"1971","unstructured":"Van der Waerden, B.L.: How the proof of Baudet's conjecture was found. In L. Mirsky, editor, Papers presented to Richard Rado on the occasion of his sixty-fifth birthday, Academic Press, London-New York (1971) 252\u2013260"},{"key":"13_CR20","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-51486-4_101","volume":"379","author":"S. Yoccoz","year":"1989","unstructured":"Yoccoz, S.: Constructive aspects of the omega-rule: Application to proof systems in computer science and algorithmic logic. Lecture Notes in Computer Science 379 (1989) 553\u2013565","journal-title":"Lecture Notes in Computer Science"}],"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_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:32Z","timestamp":1605647852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}