{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:49:50Z","timestamp":1742921390036,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642167607"},{"type":"electronic","value":"9783642167614"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16761-4_31","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:11:14Z","timestamp":1288703474000},"page":"348-361","source":"Crossref","is-referenced-by-count":9,"title":["Scheme-Based Synthesis of Inductive Theories"],"prefix":"10.1007","author":[{"given":"Omar","family":"Montano-Rivas","sequence":"first","affiliation":[]},{"given":"Roy","family":"McCasland","sequence":"additional","affiliation":[]},{"given":"Lucas","family":"Dixon","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random Testing in Isabelle\/HOL. In: SEFM, pp. 230\u2013239 (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"31_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-30210-0_20","volume-title":"Artificial Intelligence and Symbolic Computation","author":"B. Buchberger","year":"2004","unstructured":"Buchberger, B.: Algorithm Supported Mathematical Theory Exploration: A Personal View and Stragegy. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 236\u2013250. Springer, Heidelberg (2004)"},{"issue":"4","key":"31_CR3","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B., Craciun, A., Jebelean, T., Kov\u00e1cs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M.: Theorema: Towards computer-aided mathematical theory exploration. J. Applied Logic\u00a04(4), 470\u2013504 (2006)","journal-title":"J. Applied Logic"},{"key":"31_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-level Guidance for Mathematical Reasoning","author":"A. Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol.\u00a056. Cambridge University Press, Cambridge (2005)"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Colton, S.: Automated Theory Formation in Pure Mathematics. PhD thesis, Division of Informatics, University of Edinburgh (2001)","DOI":"10.1007\/978-1-4471-0147-5"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Craciun, A., Hodorog, M.: Decompositions of Natural Numbers: From A Case Study in Mathematical Theory Exploration. In: SYNASC 2007 (2007)","DOI":"10.1109\/SYNASC.2007.55"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60381-6_6","volume-title":"Conditional and Typed Rewriting Systems","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N.: Hierachical Termination. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 89\u2013105. Springer, Heidelberg (1995)"},{"key":"31_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L. Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.D.: IsaPlanner: A Prototype Proof Planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"31_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture Synthesis for Inductive Theories. Journal of Automated Reasoning (2010) (to appear)","DOI":"10.1007\/s10817-010-9193-y"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. PhD thesis, Dept. of Informatics, T. U. M\u00fcnchen (2009)","DOI":"10.1007\/s10817-009-9157-2"},{"key":"31_CR12","unstructured":"Lenat, D.B.: AM: An Artificial Intelligence approach to discovery in Mathematics as Heuristic Search. In: Knowledge-Based Systems in Artificial Intelligence (1982)"},{"issue":"1","key":"31_CR13","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2005.11.021","volume":"151","author":"R. McCasland","year":"2006","unstructured":"McCasland, R., Bundy, A., Smith, P.F.: Ascertaining Mathematical Theorems. Electr. Notes Theor. Comput. Sci.\u00a0151(1), 21\u201338 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"31_CR14","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\u2019s Logics: HOL (2000)"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"31_CR16","unstructured":"Sutcliffe, G., Gao, Y., Colton, S.: A Grand Challenge of Theorem Discovery (June 2003)"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Wehrman, I., Stump, A., Westbrook, E.: Slothrop: KnuthBendix Completion with a Modern Termination Checker. In: Webster University, St. Louis, Missouri M.Sc. Computer Science, Washington University, pp. 268\u2013279 (2006)","DOI":"10.1007\/11805618_22"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16761-4_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T13:27:22Z","timestamp":1740662842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16761-4_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642167607","9783642167614"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16761-4_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}