{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:46Z","timestamp":1774837966097,"version":"3.50.1"},"publisher-location":"Cham","reference-count":8,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319431437","type":"print"},{"value":"9783319431444","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_28","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T04:24:16Z","timestamp":1470457456000},"page":"459-465","source":"Crossref","is-referenced-by-count":5,"title":["What\u2019s in a Theorem Name?"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","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":[[2016,8,7]]},"reference":[{"issue":"3","key":"28_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s11219-006-9219-1","volume":"14","author":"F Deissenboeck","year":"2006","unstructured":"Deissenboeck, F., Pizka, M.: Concise and consistent naming. Softw. Q. J. 14(3), 261\u2013282 (2006)","journal-title":"Softw. Q. J."},{"key":"28_CR2","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)"},{"issue":"3","key":"28_CR3","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015)","journal-title":"J. Autom. Reason."},{"key":"28_CR4","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. CoRR, 1501.02155 (2015)"},{"key":"28_CR5","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Efficient semantic features for automated reasoning over large theories. In: IJCAI 2015, pp. 3084\u20133090. AAAI Press (2015)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Kripke, S.A.: Naming and necessity. In: Semantics of Natural Language, pp. 253\u2013355. Springer, Netherlands, Dordrecht (1972)","DOI":"10.1007\/978-94-010-2557-7_9"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Lawrie, D., Morrell, C., Feild, H., Binkley, D.: What\u2019s in a name? A study of identifiers. In: ICPC 2006, pp. 3\u201312. IEEE (2006)","DOI":"10.1109\/ICPC.2006.51"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Urban, J.: Content-based encoding of mathematical and code libraries. In: MathWikis 2011, CEUR-WS, vol. 767, pp. 49\u201353 (2011)","DOI":"10.1111\/j.1469-8749.2011.04074_2.x"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T15:39:30Z","timestamp":1749051570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}