{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:54:22Z","timestamp":1725515662201},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_25","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"371-385","source":"Crossref","is-referenced-by-count":1,"title":["A Combinator Language for Theorem Discovery"],"prefix":"10.1007","author":[{"given":"Phil","family":"Scott","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"25_CR1","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1006\/ijhc.2000.0394","volume":"53","author":"S. Colton","year":"2000","unstructured":"Colton, S., Bundy, A., Walsh, T.: On the notion of interestingness in automated mathematical discovery. Int. J. Hum.-Comput. Stud.\u00a053(3), 351\u2013375 (2000)","journal-title":"Int. J. Hum.-Comput. Stud."},{"key":"25_CR2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction: Essays in Honour of Robin Milner","author":"M. Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 169\u2013185. MIT Press, Cambridge (2000)"},{"key":"25_CR3","unstructured":"Hales, T.: Introduction to the Flyspeck Project, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/432\/pdf\/05021.HalesThomas.Paper.432.pdf"},{"key":"25_CR4","first-page":"1370","volume":"55","author":"T. Hales","year":"2008","unstructured":"Hales, T.: Formal proof. Notices of the American Mathematical Society\u00a055, 1370\u20131381 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: a Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"McCasland, R.L., Bundy, A.: MATHsAiD: A Mathematical Theorem Discovery Tool. In: SYNASC, pp. 17\u201322 (2006)","DOI":"10.1109\/SYNASC.2006.51"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/10930755_21","volume-title":"Theorem Proving in Higher Order Logics","author":"L.I. Meikle","year":"2003","unstructured":"Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 319\u2013334. Springer, Heidelberg (2003)"},{"issue":"1522","key":"25_CR8","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1098\/rsta.1984.0067","volume":"312","author":"R. Milner","year":"1984","unstructured":"Milner, R., Bird, R.S.: The Use of Machines to Assist in Rigorous Proof [and Discussion]. Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences\u00a0312(1522), 411\u2013422 (1984)","journal-title":"Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., Macqueen, D.: The Definition of Standard ML - Revised. The MIT Press, rev. sub. edn. (May 1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1090\/S0002-9947-1902-1500592-8","volume":"3","author":"E.H. Moore","year":"1902","unstructured":"Moore, E.H.: On the Projective Axioms of Geometry. Transactions of the American Mathematical Society\u00a03, 142\u2013158 (1902)","journal-title":"Transactions of the American Mathematical Society"},{"key":"25_CR11","unstructured":"Scott, P.: Mechanising Hilbert\u2019s Foundations of Geometry in Isabelle. Master\u2019s thesis, University of Edinburgh (2008)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-22863-6_28","volume-title":"Interactive Theorem Proving","author":"P. Scott","year":"2011","unstructured":"Scott, P., Fleuriot, J.: Composable Discovery Engines for Interactive Theorem Proving. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 370\u2013375. Springer, Heidelberg (2011)"},{"issue":"3-4","key":"25_CR13","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1017\/S0956796809007321","volume":"19","author":"J.M. Spivey","year":"2009","unstructured":"Spivey, J.M.: Algebras for combinatorial search. Journal of Functional Programming\u00a019(3-4), 469\u2013487 (2009)","journal-title":"Journal of Functional Programming"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/10704973_4","volume-title":"Advanced Functional Programming","author":"S.D. Swierstra","year":"1999","unstructured":"Swierstra, S.D., Alcocer, P.R.A., Saraiva, J.: Designing and Implementing Combinator Languages. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol.\u00a01608, pp. 150\u2013206. Springer, Heidelberg (1999)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for Functional Programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925, pp. 24\u201352. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,26]],"date-time":"2024-04-26T01:54:58Z","timestamp":1714096498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}