{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:55:31Z","timestamp":1725738931648},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642393198"},{"type":"electronic","value":"9783642393204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_12","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T07:22:52Z","timestamp":1372663372000},"page":"184-199","source":"Crossref","is-referenced-by-count":4,"title":["Capturing Hiproofs in HOL Light"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[]},{"given":"Mark","family":"Adams","sequence":"additional","affiliation":[]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"HOL light, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light","key":"12_CR1"},{"unstructured":"Proofscape, \n                    \n                      http:\/\/proofscape.org","key":"12_CR2"},{"unstructured":"Prooftree, \n                    \n                      http:\/\/askra.de\/software\/prooftree\/","key":"12_CR3"},{"unstructured":"Adams, M.: Tactician (2012), \n                    \n                      http:\/\/www.proof-technologies.com\/tactician","key":"12_CR4"},{"unstructured":"Adams, M., Aspinall, D.: Recording and refactoring HOL light tactic proofs. In: Workshop on Automated Theory eXploration (2012)","key":"12_CR5"},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s11786-010-0025-6","volume":"3","author":"D. Aspinall","year":"2010","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Tactics for hierarchical proof. Mathematics in Computer Science\u00a03(3), 309\u2013330 (2010)","journal-title":"Mathematics in Computer Science"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-28717-6_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Aspinall","year":"2012","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Querying proofs. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol.\u00a07180, pp. 92\u2013106. Springer, Heidelberg (2012)"},{"issue":"3","key":"12_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1080\/09528130701475401","volume":"19","author":"D. Barker-Plummer","year":"2007","unstructured":"Barker-Plummer, D., Etchemendy, J.: A computational architecture for heterogeneous reasoning. Journal of Experimental & Theoretical Artificial Intelligence\u00a019(3), 195\u2013225 (2007)","journal-title":"Journal of Experimental & Theoretical Artificial Intelligence"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-56979-0_3","volume-title":"Conceptual Graphs for Knowledge Representation","author":"J. Barwise","year":"1993","unstructured":"Barwise, J.: Heterogeneous reasoning. In: Mineau, G.W., Moulin, B., Sowa, J.F. (eds.) ICCS 1993. LNCS, vol.\u00a0699, pp. 64\u201374. Springer, Heidelberg (1993)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Intelligent Computer Mathematics","author":"T. Bourke","year":"2012","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 32\u201348. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. Electronic Notes in Theoretical Computer Science 155 (2006)","key":"12_CR11","DOI":"10.1016\/j.entcs.2005.11.063"},{"unstructured":"Griffin, T.: Notational definition and top-down refinement for interactive proof development systems. PhD thesis, Cornell University (1988)","key":"12_CR12"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-02444-3_13","volume-title":"Types for Proofs and Programs","author":"C. Kaliszyk","year":"2009","unstructured":"Kaliszyk, C., Wiedijk, F.: Merging procedural and declarative proof. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 203\u2013219. Springer, Heidelberg (2009)"},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(94)90192-9","volume":"133","author":"D. Kapur","year":"1994","unstructured":"Kapur, D., Nie, X., Musser, D.: An overview of the tecton proof system. Theoretical Computer Science\u00a0133(2), 307\u2013339 (1994)","journal-title":"Theoretical Computer Science"},{"unstructured":"Obua, S.: HipCam (2013), \n                    \n                      http:\/\/github.com\/phlegmaticprogrammer\/hipcam","key":"12_CR15"},{"key":"12_CR16","series-title":"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.\u00a04130, pp. 298\u2013302. Springer, Heidelberg (2006)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - A generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"},{"unstructured":"Whiteside, I.: Refactoring Proofs. PhD thesis, University of Edinburgh (2013)","key":"12_CR18"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-22673-1_18","volume-title":"Intelligent Computer Mathematics","author":"I. Whiteside","year":"2011","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 260\u2013275. Springer, Heidelberg (2011)"}],"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-39320-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T02:26:39Z","timestamp":1557887199000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}