{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:03Z","timestamp":1774025763278,"version":"3.50.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T00:00:00Z","timestamp":1498176000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000848","name":"University of Edinburgh","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000848","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Appl Intell"],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1007\/s10489-017-0954-8","type":"journal-article","created":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T19:48:07Z","timestamp":1498160887000},"page":"585-606","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["MATHsAiD: Automated mathematical theory exploration"],"prefix":"10.1007","volume":"47","author":[{"given":"R. L.","family":"McCasland","sequence":"first","affiliation":[]},{"given":"A.","family":"Bundy","sequence":"additional","affiliation":[]},{"given":"P. F.","family":"Smith","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,23]]},"reference":[{"key":"954_CR1","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1109\/SEFM.2004.36","volume-title":"SEFM \u201904: Proceedings of the Software Engineering and Formal Methods, 2nd International Conference","author":"S Berghofer","year":"2004","unstructured":"Berghofer S, Nipkow T (2004) Random testing in Isabelle\/HOL. In: SEFM \u201904: Proceedings of the Software Engineering and Formal Methods, 2nd International Conference. doi: 10.1109\/SEFM.2004.36 . IEEE Computer Society, Washington, DC, USA, pp 230\u2013239"},{"key":"954_CR2","doi-asserted-by":"crossref","unstructured":"Blanchette J, Nipkow T (2010) Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann M, Paulson LC (eds) First International Conference on Interactive Theorem Proving (ITP 2010), vol LNCS 6172. Springer, pp 131\u2013146","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"954_CR3","unstructured":"Bundy A (1991) A science of reasoning. In: Lassez JL, Plotkin G (eds) Computational Logic: Essays in Honor of Alan Robinson. MIT Press, pp 178\u2013198"},{"key":"954_CR4","doi-asserted-by":"crossref","unstructured":"Bundy A, Basin D, Hutter D, Ireland A (2005) Rippling: Meta-level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science, vol 56, Cambridge University Press","DOI":"10.1017\/CBO9780511543326"},{"key":"954_CR5","doi-asserted-by":"crossref","unstructured":"Dixon L, Fleuriot JD (2003) IsaPlanner: A prototype proof planner in Isabelle. In: Proceedings of CADE\u201903, vol 2741. LNCS, pp 279\u2013283","DOI":"10.1007\/978-3-540-45085-6_22"},{"key":"954_CR6","doi-asserted-by":"crossref","unstructured":"Hungerford T (1980) Algebra. no. 73 in graduate texts in mathematics, Springer-Verlag","DOI":"10.1007\/978-1-4612-6101-8"},{"key":"954_CR7","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson M, Dixon L, Bundy A (2011) Conjecture synthesis for inductive theories. J Autom Reason 47:251\u2013289","journal-title":"J Autom Reason"},{"key":"954_CR8","doi-asserted-by":"crossref","unstructured":"Johansson M, Ros\u00e9n D, Smallbone N, Claessen K (2014) Hipster: Integrating theory exploration in a proof assistant. In: Proceedings of the conference on intelligent computer mathematics (CICM), vol LNCS 8543. Springer, pp 108\u2013122","DOI":"10.1007\/978-3-319-08434-3_9"},{"key":"954_CR9","doi-asserted-by":"publisher","unstructured":"Jouannaud JP, Rubio A (1999) Logic in Computer Science, Symposium on The higher-order recursive path ordering, 0, 402. doi: 10.1109\/LICS.1999.782635","DOI":"10.1109\/LICS.1999.782635"},{"key":"954_CR10","unstructured":"Knuth DE, Bendix PB (1970) Simple word problems in universal algebra. In: Leech J (ed) Computational problems in abstract algebra. Pergamon Press, pp 263\u2013297"},{"key":"954_CR11","doi-asserted-by":"crossref","unstructured":"Lakatos I (1976) Proofs and refutations: The logic of mathematical discovery, Cambridge University Press","DOI":"10.1017\/CBO9781139171472"},{"key":"954_CR12","volume-title":"Knowledge-based systems in Artificial Intelligence","author":"DB Lenat","year":"1982","unstructured":"Lenat DB (1982) AM: An artificial intelligence approach to discovery in mathematics as heuristic search. In: Knowledge-based systems in Artificial Intelligence. Also available from Stanford as TechReport AIM 286. McGraw Hill, New York"},{"key":"954_CR13","doi-asserted-by":"crossref","first-page":"1357","DOI":"10.1216\/rmjm\/1181071721","volume":"28","author":"R McCasland","year":"1998","unstructured":"McCasland R, Moore M, Smith P (1998) An introduction to Zariski Spaces over Zariski Topologies. Rocky Mountain J Math 28:1357\u20131369","journal-title":"Rocky Mountain J Math"},{"key":"954_CR14","unstructured":"McCasland RL, Bundy A, Autexier S (2007) Automated discovery of inductive theorems. In: Matuszewski R, Zalewska A (eds) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric. http:\/\/mizar.org\/trybulec65\/ , vol 10(23). University of Bia\u0142ystok, pp 135\u2013149"},{"key":"954_CR15","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.entcs.2005.11.021","volume":"151","author":"RL McCasland","year":"2006","unstructured":"McCasland RL, Bundy A, Smith PF (2006) Ascertaining mathematical theorems. Electr Notes in Theor Comput Sci 151 :21\u201338","journal-title":"Electr Notes in Theor Comput Sci"},{"key":"954_CR16","unstructured":"McCune W (1990) The Otter user\u2019s guide. Tech. Rep. ANL\/90\/9 Argonne National Laboratory"},{"key":"954_CR17","unstructured":"McCune W (1994) A Davis-Putnam program and its application to finite first-order model search. Tech. Rep. ANL\/MCS-TM-194 Argonne National Laboratoriess"},{"key":"954_CR18","doi-asserted-by":"crossref","unstructured":"Montano-Rivas O, McCasland R, Dixon L, Bundy A Scheme-based synthesis of inductive theories. In: MICAI, LNCS, vol. 6437, pp. 348\u2013361 (2010). Received best paper award","DOI":"10.1007\/978-3-642-16761-4_31"},{"key":"954_CR19","doi-asserted-by":"crossref","unstructured":"Paulson LC (1994) Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828","DOI":"10.1007\/BFb0030541"},{"key":"954_CR20","unstructured":"Pease A (2007) A computational model of Lakatos-style reasoning. Ph.D. thesis, University of Edinburgh"},{"key":"954_CR21","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/3-540-48660-7_37","volume-title":"CADE-16: Proceedings Of the 16th international conference on automated deduction","author":"J Zhang","year":"1999","unstructured":"Zhang J (1999) Jian: System description: MCS: Model-based Conjecture Searching. In: CADE-16: Proceedings Of the 16th international conference on automated deduction. Springer-Verlag, London, UK, pp 393\u2013397"}],"container-title":["Applied Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-017-0954-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10489-017-0954-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10489-017-0954-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,26]],"date-time":"2019-09-26T12:32:56Z","timestamp":1569501176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10489-017-0954-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,23]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["954"],"URL":"https:\/\/doi.org\/10.1007\/s10489-017-0954-8","relation":{},"ISSN":["0924-669X","1573-7497"],"issn-type":[{"value":"0924-669X","type":"print"},{"value":"1573-7497","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6,23]]}}}