{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:53:32Z","timestamp":1725515612961},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_1","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"1-16","source":"Crossref","is-referenced-by-count":10,"title":["Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Alama","sequence":"first","affiliation":[]},{"given":"Lionel","family":"Mamane","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-15582-6_25","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"M. Adams","year":"2010","unstructured":"Adams, M.: Introducing HOL Zero. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol.\u00a06327, pp. 142\u2013143. Springer, Heidelberg (2010)"},{"key":"1_CR2","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. CoRR abs\/1108.3446 (2012), \n                    \n                      http:\/\/arxiv.org\/abs\/1108.3446"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-28717-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Alama","year":"2012","unstructured":"Alama, J., K\u00fchlwein, D., Urban, J.: Automated and Human Proofs in General Mathematics: An Initial Comparison. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 37\u201345. Springer, Heidelberg (2012)"},{"issue":"1-3","key":"1_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Padovani, L., Coen, C.S., Guidi, F., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell.\u00a038(1-3), 27\u201346 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"1_CR5","unstructured":"Bertot, Y., Pons, O., Pottier, L.: Dependency graphs for interactive theorem provers. Tech. rep., INRIA, report RR-4052 (2000)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"issue":"2","key":"1_CR7","first-page":"153","volume":"3","author":"A. Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: mizar in a nutshell. Journal of Formalized Reasoning\u00a03(2), 153\u2013245 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive Type Classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 160\u2013174. Springer, Heidelberg (2007)"},{"key":"1_CR9","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":"1_CR10","unstructured":"Mamane, L., Geuvers, H.: A document-oriented Coq plugin for TeXmacs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM 2007 - Work in Progress. RISC Report, vol. 07-06, pp. 47\u201360. University of Linz, Austria (2007)"},{"key":"1_CR11","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications\u00a04, 3\u201324 (2005)","journal-title":"Mechanized Mathematics and Its Applications"},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"1_CR13","unstructured":"Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: UITP 1998. Eindhoven University of Technology (1998)"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science\u00a021(4), 795\u2013825 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"1_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM\u2014fast 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":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15582-6_30","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"J. Urban","year":"2010","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol.\u00a06327, pp. 155\u2013166. Springer, Heidelberg (2010)"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-540-74591-4_28","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Wiedijk","year":"2007","unstructured":"Wiedijk, F.: Mizar\u2019s Soft Type System. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 383\u2013399. Springer, Heidelberg (2007)"}],"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-31374-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:21:52Z","timestamp":1556889712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}