{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:48Z","timestamp":1725664368553},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601562"},{"type":"electronic","value":"9783540495338"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60156-2_9","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:46:33Z","timestamp":1330260393000},"page":"115-130","source":"Crossref","is-referenced-by-count":1,"title":["A proof environment for arithmetic with the omega rule"],"prefix":"10.1007","author":[{"given":"Siani","family":"Baker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Smaill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"9_CR1","unstructured":"Baker, S.: Aspects of the Constructive Omega Rule within Automated Deduction. PhD thesis, University of Edinburgh (1992)"},{"key":"9_CR2","volume-title":"Technical Paper 10","author":"S. Baker","year":"1992","unstructured":"Baker, S.: CORE manual. Technical Paper 10, Dept. of Artificial Intelligence, Edinburgh (1992)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Baker, S.: A new application for explanation-based generalisation within automated deduction. In A. Bundy, editor, 12th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag (1994) 177\u2013191. Also available from Cambridge as Computer Laboratory Technical Report 327.","DOI":"10.1007\/3-540-58156-1_13"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag 449 (1990) 647\u2013648","DOI":"10.1007\/3-540-52885-7_123"},{"key":"9_CR5","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62 (1993) 185\u2013253","journal-title":"Artificial Intelligence"},{"key":"9_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":"9_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"},{"key":"9_CR8","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)","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"9_CR9","unstructured":"Kreisel, G.: Mathematical logic. In T.L. Saaty, editor, Lectures on Modern Mathematics, John Wiley and Sons III (1965) 95\u2013195"},{"key":"9_CR10","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":"L\u00f6pez-Escobar, E.G.K.: On an extremely restricted \u03a9-rule. Fundamenta Mathematicae 90 (1976) 159\u201372","journal-title":"Fundamenta Mathematicae"},{"key":"9_CR11","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":"9_CR12","doi-asserted-by":"crossref","unstructured":"Nelson, G.C.: A further restricted \u03a9-rule. Colloquium Mathematicum 23 (1971)","DOI":"10.4064\/cm-23-1-1-3"},{"key":"9_CR13","unstructured":"Plotkin, G.: A note on inductive generalization. In D. Michie and B. Meltzer, editors, Machine Intelligence, Edinburgh University Press 5 (1969) 153\u2013164"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: Ideas and results in proof theory. In J.E. Fenstad, editor, Studies in Logic and the Foundations of Mathematics: Proceedings of the Second Scandinavian Logic Symposium, North Holland 63 (1971) 235\u2013307","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"9_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"},{"key":"9_CR16","unstructured":"Rouveirol, C.: Saturation: Postponing choices when inverting resolution. In Proceedings of ECAI-90, Stockholm (1990) 557\u2013562"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Proof Theory. Springer-Verlag (1977)","DOI":"10.1007\/978-3-642-66473-1"},{"key":"9_CR18","unstructured":"Schwichtenberg, H.: Proof theory: Some applications of cut-elimination. In Barwise, editor, Handbook of Mathematical Logic, North-Holland (1977) 867\u2013896"},{"key":"9_CR19","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."},{"key":"9_CR20","unstructured":"Takeuti, G.: Proof theory. North-Holland, 2 edition (1987)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Tucker, J.V., Wainer, S.S., Zucker, J.I.: Provable computable functions on abstract-data-types. In M.S. Paterson, editor, Automata, Languages and Programming, Lecture Notes in Computer Science, Springer-Verlag 443 (1990) 660\u2013673","DOI":"10.1007\/BFb0032065"},{"key":"9_CR22","unstructured":"Yoccoz, S.: Constructive aspects of the omega-rule: Application to proof systems in computer science and algorithmic logic. Lecture Notes in Computer Science, Springer-Verlag 379 (1989) 553\u2013565"}],"container-title":["Lecture Notes in Computer Science","Integrating Symbolic Mathematical Computation and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60156-2_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:55:25Z","timestamp":1605628525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60156-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601562","9783540495338"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-60156-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}