{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:39Z","timestamp":1774837959323,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319084336","type":"print"},{"value":"9783319084343","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-08434-3_9","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T03:14:35Z","timestamp":1404184475000},"page":"108-122","source":"Crossref","is-referenced-by-count":23,"title":["Hipster: Integrating Theory Exploration in a Proof Assistant"],"prefix":"10.1007","author":[{"given":"Moa","family":"Johansson","sequence":"first","affiliation":[]},{"given":"Dan","family":"Ros\u00e9n","sequence":"additional","affiliation":[]},{"given":"Nicholas","family":"Smallbone","sequence":"additional","affiliation":[]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Blanchette, J.C.: Personal communication (2013)"},{"issue":"2","key":"9_CR2","first-page":"9","volume":"38","author":"B. Buchberger","year":"2000","unstructured":"Buchberger, B.: Theory exploration with Theorema. Analele Universitatii Din Timisoara, ser. Matematica-Informatica\u00a038(2), 9\u201332 (2000)","journal-title":"Analele Universitatii Din Timisoara, ser. Matematica-Informatica"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Creciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic\u00a04(4), 470\u2013504 (2006), Towards Computer Aided Mathematics","DOI":"10.1016\/j.jal.2005.10.006"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K. Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 392\u2013406. Springer, Heidelberg (2013)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-13977-2_3","volume-title":"Tests and Proofs","author":"K. Claessen","year":"2010","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: Guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 6\u201321. Springer, Heidelberg (2010)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.D.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 83\u201398. Springer, Heidelberg (2004)"},{"key":"9_CR8","unstructured":"Haftmann, F., Bulwahn, L.: Code generation from Isabelle\/HOL theories (2013), \n                    \n                      http:\/\/isabelle.in.tum.de\/doc\/codegen.pdf"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-45221-5_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Heras","year":"2013","unstructured":"Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol.\u00a08312, pp. 389\u2013406. Springer, Heidelberg (2013)"},{"key":"9_CR11","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA), number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning\u00a016, 79\u2013111 (1996)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M. Johansson","year":"2011","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning\u00a047(3), 251\u2013289 (2011)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D. K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: Machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 35\u201350. Springer, Heidelberg (2013)"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2005.11.021","volume":"151","author":"R.L. McCasland","year":"2006","unstructured":"McCasland, R.L., Bundy, A., Smith, P.F.: Ascertaining mathematical theorems. Electronic Notes in Theoretical Computer Science\u00a0151(1), 21\u201338 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"1637","DOI":"10.1016\/j.eswa.2011.06.055","volume":"39","author":"O. Montano-Rivas","year":"2012","unstructured":"Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Systems with Applications\u00a039(2), 1637\u20131646 (2012)","journal-title":"Expert Systems with Applications"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"9_CR18","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL 2010 (2010)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08434-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:26:09Z","timestamp":1558934769000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08434-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319084336","9783319084343"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08434-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}