{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:55:30Z","timestamp":1725738930694},"publisher-location":"Berlin, Heidelberg","reference-count":33,"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_8","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T11:22:52Z","timestamp":1372677772000},"page":"120-135","source":"Crossref","is-referenced-by-count":6,"title":["Automated Reasoning Service for HOL Light"],"prefix":"10.1007","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J. Alama","year":"2011","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: Issues and solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding Monomorphic and Polymorphic Types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 493\u2013507. Springer, Heidelberg (2013), \n                    \n                      http:\/\/www21.in.tum.de\/~blanchet\/enc_types_paper.pdf"},{"key":"8_CR4","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism, \n                    \n                      http:\/\/www21.in.tum.de\/~blanchet\/tff1spec.pdf"},{"key":"8_CR5","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: The SNoW Learning Architecture. Technical Report UIUCDCS-R-99-2101, UIUC Computer Science Department, 5 (1999)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","year":"2006","unstructured":"Furbach, U., Shankar, N. (eds.): IJCAR 2006. LNCS (LNAI), vol.\u00a04130. Springer, Heidelberg (2006)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Van Gelder, A., Sutcliffe, G.: Extending the TPTP language to higher-order logic with automated parser generation. In: Furbach, Shankar (eds.) [7], pp. 156\u2013161","DOI":"10.1007\/11814771_15"},{"key":"8_CR9","series-title":"Dagstuhl Seminar Proceedings","volume-title":"Mathematics, Algorithms, Proofs","author":"T.C. Hales","year":"2005","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol.\u00a005021. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany (2005)"},{"key":"8_CR10","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":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","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.\u00a01104, pp. 313\u2013327. Springer, Heidelberg (1996)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. Accepted to ITP 2013, \n                    \n                      http:\/\/cl-informatik.uibk.ac.at\/~cek\/import.pdf","DOI":"10.1007\/978-3-642-39634-2_7"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-38574-2_18","volume-title":"Automated Deduction \u2013 CADE-24","author":"C. Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Urban, J.: PRocH: Proof reconstruction for HOL Light. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 267\u2013274. Springer, Heidelberg (2013), \n                    \n                      http:\/\/mws.cs.ru.nl\/~urban\/proofs.pdf"},{"key":"8_CR15","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. CoRR, abs\/1211.7012 (2012)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31365-3_30","volume-title":"Automated Reasoning","author":"D. K\u00fchlwein","year":"2012","unstructured":"K\u00fchlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 378\u2013392. Springer, Heidelberg (2012)"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR18","unstructured":"Paulson, L.C., Blanchette, J.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL (2010) (Invited talk)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"L.C. Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 232\u2013245. Springer, Heidelberg (2007)"},{"key":"8_CR20","unstructured":"Pitts, A.: The HOL logic. In: Gordon, M.J.C., Melham, T.F. (eds.) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)"},{"issue":"2-3","key":"8_CR21","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"2-3","key":"8_CR22","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - A Brainiac Theorem Prover. AI Commun.\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, Shankar (eds.) [7], pp. 67\u201381","DOI":"10.1007\/11814771_7"},{"key":"8_CR24","series-title":"LNAI","first-page":"152","volume-title":"CICM 2013","author":"C. Tankink","year":"2013","unstructured":"Tankink, C., Kaliszyk, C., Urban, J., Geuvers, H.: Formal mathematics on display: A wiki for Flyspeck. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 152\u2013167. Springer, Heidelberg (2013)"},{"issue":"1","key":"8_CR25","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"8_CR26","unstructured":"Urban, J.: An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper). In: H\u00f6fner, P., McIver, A., Struth, G. (eds.) ATE Workshop. CEUR Workshop Proceedings, vol.\u00a0760, pp. 3\u20138. CEUR-WS.org (2011)"},{"key":"8_CR27","unstructured":"Urban, J.: Parallelizing Mizar. CoRR, abs\/1206.0141 (2012)"},{"key":"8_CR28","unstructured":"Urban, J.: BliStr: The Blind Strategymaker. CoRR, abs\/1301.2683 (2013)"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J. Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning\u00a050, 229\u2013241 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-14128-7_12","volume-title":"Intelligent Computer Mathematics","author":"J. Urban","year":"2010","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC\/Calculemus\/MKM 2010. LNCS, vol.\u00a06167, pp. 132\u2013146. Springer, Heidelberg (2010)"},{"key":"8_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP Machine learning connection prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol.\u00a06793, pp. 263\u2013277. Springer, Heidelberg (2011)"},{"key":"8_CR33","unstructured":"Vinge, V.: A Fire Upon the Deep. Tor Books (1992)"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T06:27:44Z","timestamp":1557901664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}