{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:42Z","timestamp":1759638822069},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055727X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0013063","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:02:07Z","timestamp":1132711327000},"page":"214-225","source":"Crossref","is-referenced-by-count":11,"title":["On the use of the constructive omega-rule within automated deduction"],"prefix":"10.1007","author":[{"given":"S.","family":"Baker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Ireland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"R. Aubin. 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":"20_CR2","volume-title":"Discussion Paper 102","author":"S. Baker","year":"1990","unstructured":"S. Baker. Notes on the constructive omega rule and a new method of generalisation. Discussion Paper 102, Dept. of Artificial Intelligence, Edinburgh, 1990."},{"key":"20_CR3","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"M.R. Donat and L.A. Wallen. Learning and applying generalised solutions using higher order resolution. In E. Lusk and R. Overbeek, editors, Lecture Notes in Computer Science, volume 310, pages 41\u201360. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012822"},{"key":"20_CR5","doi-asserted-by":"crossref","first-page":"259","DOI":"10.2307\/2964649","volume":"27","author":"S. Feferman","year":"1962","unstructured":"S. Feferman. Transfinite recursive progressions of axiomatic theories. Journal of Symbolic Logic, 27:259\u2013316, 1962.","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0743-1066(90)90041-3","volume":"9","author":"E.B. Kinber","year":"1990","unstructured":"E.B. Kinber and A.N. Brazma. Models of inductive synthesis. Journal of Logic Programming, 9:221\u2013233, 1990.","journal-title":"Journal of Logic Programming"},{"key":"20_CR7","doi-asserted-by":"crossref","first-page":"159","DOI":"10.4064\/fm-90-2-159-172","volume":"90","author":"E.G.K. L\u00f6pez-Escobar","year":"1976","unstructured":"E.G.K. L\u00f6pez-Escobar. On an extremely restricted \u03c9-rule. Fundamenta Mathematicae, 90:159\u201372, 1976.","journal-title":"Fundamenta Mathematicae"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"E.G.K. L\u00f6pez-Escobar. Infinite rules in finite systems. In Da Costa Arruda and Chuaqui, editors, Non-classical Logics, Model Theory and Computability. North Holland, 1977. Studies in Logic 89.","DOI":"10.1016\/S0049-237X(08)70646-3"},{"key":"20_CR9","unstructured":"S. Muggleton. A strategy for constructing new predicates in first-order logic. In Proceedings of the Third European Working Session on Learning. Pitman Publishing, 1988."},{"key":"20_CR10","doi-asserted-by":"crossref","first-page":"246","DOI":"10.2307\/2269096","volume":"21","author":"S. Orey","year":"1956","unstructured":"S. Orey. On \u03c9-consistency and related properties. Journal of Symbolic Logic, 21:246\u2013252, 1956.","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"R. Penrose. The Emperor's New Mind. Vintage, 1989.","DOI":"10.1093\/oso\/9780198519737.001.0001"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"B. Rosser. Godel-theorems for non-constructive logics, volume 2. JSL, 1937.","DOI":"10.2307\/2266293"},{"key":"20_CR13","unstructured":"K. Sch\u00fctte. Beweistheorie. Springer Verlag, 1960."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg. Proof theory: Some applications of cut-elimination. In Barwise, editor, Handbook of Mathematical Logic, pages 867\u2013896. North-Holland, 1977.","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"20_CR15","first-page":"405","volume":"7","author":"J.R. Shoenfield","year":"1959","unstructured":"J.R. Shoenfield. On a restricted \u03c9-rule. Bull. Acad. Sc. Polon. Sci., Ser. des sc. math., astr. et phys., 7:405\u20137, 1959.","journal-title":"Bull. Acad. Sc. Polon. Sci., Ser. des sc. math., astr. et phys."},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"M. Takahashi. A theorem on the second order arithmetic with the \u03c9-rule. Journal of the Mathematical Society of Japan, 22, 1970.","DOI":"10.2969\/jmsj\/02210015"},{"key":"20_CR17","unstructured":"G. Takeuti. Proof theory. North-Holland, 2 edition, 1987."},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"M. Thomas and K.P. Jantke. Inductive inference for solving divergance in Knuth-Bendix. In K.P. Jantke, editor, Analogical and Inductive Inference, Procs. of AII'89, pages 288\u2013303. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51734-0_69"},{"key":"20_CR19","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-51486-4_101","volume":"379","author":"S. Yoccoz","year":"1989","unstructured":"S. Yoccoz. Constructive aspects of the omega-rule: Application to proof systems in computer science and algorithmic logic. Lecture Notes in Computer Science, 379:553\u2013565, 1989.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0013063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T03:22:35Z","timestamp":1626751355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0013063"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055727X"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0013063","relation":{},"subject":[]}}