{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:44Z","timestamp":1774837964090,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662488980","type":"print"},{"value":"9783662488997","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_26","type":"book-chapter","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T22:59:28Z","timestamp":1448060368000},"page":"372-386","source":"Crossref","is-referenced-by-count":10,"title":["Sharing HOL4 and HOL Light Proof Knowledge"],"prefix":"10.1007","author":[{"given":"Thibault","family":"Gauthier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"26_CR1","unstructured":"Adams, M.: The common HOL platform. In: Kaliszyk, C., Paskevich, A., (eds.) Fourth International Workshop on Proof Exchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2\u20133 August 2015. to appear in EPTCS (2015)"},{"issue":"2","key":"26_CR2","first-page":"91","volume":"7","author":"A Asperti","year":"2014","unstructured":"Asperti, A., Ricciotti, W., Coen, C.S.: Matita tutorial. J. Formaliz. Reason. 7(2), 91\u2013199 (2014)","journal-title":"J. Formaliz. Reason."},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-20615-8_10","volume-title":"Intelligent Computer Mathematics","author":"S Autexier","year":"2015","unstructured":"Autexier, S., Hutter, D.: Structure formation in large theories. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 155\u2013170. Springer, Heidelberg (2015)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-20615-8_1","volume-title":"Intelligent Computer Mathematics","author":"JC Blanchette","year":"2015","unstructured":"Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 3\u201317. Springer, Heidelberg (2015)"},{"key":"26_CR5","first-page":"1","volume":"13","author":"M Bortin","year":"2006","unstructured":"Bortin, M., Johnsen, E.B., L\u00fcth, C.: Structured formal development in Isabelle. Nordic J. Comput. 13, 1\u201320 (2006)","journal-title":"Nordic J. Comput."},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-319-08434-3_20","volume-title":"Intelligent Computer Mathematics","author":"T Gauthier","year":"2014","unstructured":"Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 267\u2013281. Springer, Heidelberg (2014)"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Gauthier, T., Kaliszyk, C.: Premise selection and external provers for HOL4. In: Leroy, X., Tiu, A., (eds.) Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pp. 49\u201357 (2015)","DOI":"10.1145\/2676724.2693173"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104. Springer, Heidelberg (1996)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Huet, G., Herbelin, H.: 30 years of research and development around Coq. In: Jagannathan, S., Sewell, P., (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 249\u2013250. ACM (2014)","DOI":"10.1145\/2535838.2537848"},{"key":"26_CR11","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C., (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), number NASA\/CP-2003-212448 in NASA Technical reports, pp. 56\u201368, September 2003"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-20398-5_14","volume-title":"NASA Formal Methods","author":"J Hurd","year":"2011","unstructured":"Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177\u2013191. Springer, Heidelberg (2011)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-39634-2_7","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Krauss, A.: Scalable LCF-Style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 51\u201366. Springer, Heidelberg (2013)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-319-08434-3_26","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL Light. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 357\u2013372. Springer, Heidelberg (2014)"},{"issue":"2","key":"26_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"26_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"26_CR17","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015 (2015). (to appear)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-14052-5_22","volume-title":"Interactive Theorem Proving","author":"C Keller","year":"2010","unstructured":"Keller, C., Werner, B.: Importing HOL Light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307\u2013322. Springer, Heidelberg (2010)"},{"key":"26_CR19","unstructured":"The Mizar Mathematical Library. \n                    http:\/\/mizar.org\/"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298\u2013302. Springer, Heidelberg (2006)"},{"key":"26_CR21","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL (2010). Invited talk"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-39320-4_25","volume-title":"Intelligent Computer Mathematics","author":"F Rabe","year":"2013","unstructured":"Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 339\u2013343. Springer, Heidelberg (2013)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:25:27Z","timestamp":1559316327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}