{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:02:39Z","timestamp":1771059759527,"version":"3.50.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,7,24]],"date-time":"2010-07-24T00:00:00Z","timestamp":1279929600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,10]]},"DOI":"10.1007\/s10817-010-9193-y","type":"journal-article","created":{"date-parts":[[2010,7,23]],"date-time":"2010-07-23T04:14:46Z","timestamp":1279858486000},"page":"251-289","source":"Crossref","is-referenced-by-count":53,"title":["Conjecture Synthesis for Inductive Theories"],"prefix":"10.1007","volume":"47","author":[{"given":"Moa","family":"Johansson","sequence":"first","affiliation":[]},{"given":"Lucas","family":"Dixon","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,7,24]]},"reference":[{"key":"9193_CR1","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: SEFM \u201904: Proceedings of the Software Engineering and Formal Methods, Second International Conference, Washington, DC, USA, pp. 230\u2013239. IEEE Computer Society (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"issue":"4","key":"9193_CR2","doi-asserted-by":"crossref","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., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkrantz, M., Windsteiger, W.: Theorema: towards computer-aided mathematical theory exploration. Journal of Applied Logic 4(4), 470\u2013504 (2006)","journal-title":"Journal of Applied Logic"},{"key":"9193_CR3","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: 9th International Conference on Automated Deduction, pp. 111\u2013120 (1988)","DOI":"10.1007\/BFb0012826"},{"key":"9193_CR4","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511543326"},{"issue":"3","key":"9193_CR5","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A Bundy","year":"1992","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. J. Autom. Reason. 7(3), 303\u2013324 (1992)","journal-title":"J. Autom. Reason."},{"key":"9193_CR6","doi-asserted-by":"crossref","unstructured":"Colton, S.: Automated Theory Formation in Pure Mathematics. Springer (2002)","DOI":"10.1007\/978-1-4471-0147-5"},{"key":"9193_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. In: 20th Annual Symposium on Foundations of Computer Science, pp. 123\u2013131 (1979)","DOI":"10.1109\/SFCS.1979.32"},{"key":"9193_CR8","unstructured":"Dixon, L.: A Proof Planning Framework for Isabelle. PhD thesis, University of Edinburgh (2005)"},{"key":"9193_CR9","doi-asserted-by":"crossref","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: a prototype proof planner in Isabelle. In: Proceedings of CADE\u201903, pp. 279\u2013283 (2003)","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"9193_CR10","doi-asserted-by":"crossref","unstructured":"Dixon, L., Fleuriot, J.: Higher-order rippling in IsaPlanner. In: Proceedings of TPHOLs\u201904, pp. 83\u201398 (2004)","DOI":"10.1007\/978-3-540-30142-4_7"},{"key":"9193_CR11","doi-asserted-by":"crossref","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF\u2014A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol.\u00a078. Springer (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9193_CR12","doi-asserted-by":"crossref","unstructured":"Hodorog, M., Craciun, A.: Scheme-based systematic exploration of natural numbers. In: Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 26\u201334 (2006)","DOI":"10.1109\/SYNASC.2006.67"},{"key":"9193_CR13","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Properties of IsaCoSy\u2019s Constraint Generation Algorithm. University of Edinburgh Technical Report from 2010 with number EDI-INF-RR-1378. Available online: http:\/\/dream.inf.ed.ac.uk\/projects\/lemmadiscovery\/publications\/IsaCoSyProperties.pdf (2010)"},{"key":"9193_CR14","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra (1967)"},{"key":"9193_CR15","unstructured":"Lenat, D.B.: AM: discovery in mathematics as heuristic search. In: Heiberg, D., Damstra, D.A. (eds.) Knoledge-based Systems in Artificial Intelligence, Chapter 1. McGraw-Hill (1982)"},{"key":"9193_CR16","unstructured":"Maclean, E., Ireland, A., Atkey, R., Dixon, L.: Refinement and term synthesis in loop invariant generation. In: WING 09: Workshop on Invariant Generation (2009)"},{"key":"9193_CR17","doi-asserted-by":"crossref","unstructured":"McCasland, R., Bundy, A.: MATHsAiD: a mathematical theorem discovery tool. In: Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 17\u201322. IEEE Computer Society Press (2006)","DOI":"10.1109\/SYNASC.2006.51"},{"issue":"23","key":"9193_CR18","first-page":"135","volume":"10","author":"R McCasland","year":"2007","unstructured":"McCasland, R., Bundy, A., Autexier, S.: Automated discovery of inductive theorems. Special Issue of Studies in Logic, Grammar and Rhetoric on Computer Reconstruction of the Body of Mathematics: From Insight to Proof: Festschrift in Honor of A. Trybulec 10(23), 135\u2013149 (2007)","journal-title":"Trybulec"},{"key":"9193_CR19","unstructured":"Monroy-Borja, R.: The Use of Abduction to Correct Faulty Conjectures. Master\u2019s thesis, University of Edinburgh (1993)"},{"key":"9193_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-order Logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9193_CR21","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: the next seven hundred theorem provers. In: 9th International Conference on Automated Deduction. LNCS, vol. 310, pp. 772\u2013773. Springer (1988)","DOI":"10.1007\/BFb0012891"},{"key":"9193_CR22","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: Proceedings of the 19th International FLAIRS Conference, pp. 49\u201354 (2006)"},{"issue":"2","key":"9193_CR23","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9193-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9193-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9193-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T07:53:04Z","timestamp":1740297184000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9193-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,24]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["9193"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9193-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7,24]]}}}