{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,3]],"date-time":"2026-11-03T13:44:30Z","timestamp":1793713470202,"version":"4.6.1"},"publisher-location":"Cham","reference-count":95,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_9","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"138-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A Survey of Languages for Formalizing Mathematics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"9_CR1","unstructured":"Ausbrooks, R., et al.: Mathematical Markup Language (MathML) Version 3.0. Technical report, World Wide Web Consortium (2010). http:\/\/www.w3.org\/TR\/MathML3"},{"key":"9_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J Abrial","year":"1996","unstructured":"Abrial, J.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR3","unstructured":"Arthan, R.: ProofPower. http:\/\/www.lemma-one.com\/ProofPower\/"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-74464-1_2","volume-title":"Types for Proofs and Programs","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a proof assistant. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 18\u201332. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74464-1_2"},{"key":"9_CR5","unstructured":"Buswell, S., Caprotti, O., Carlisle, D., Dewar, M., Gaetano, M., Kohlhase, M.: The Open Math Standard, Version 2.0. Technical report, The Open Math Society (2004). http:\/\/www.openmath.org\/standard\/om20"},{"key":"9_CR6","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The $$\\lambda \\varPi $$-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"9_CR7","unstructured":"Brown, C., Kaliszyk, C., P\u0105k, K.: Higher-order Tarski Grothendieck as a foundation for formal proof. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) Interactive Theorem Proving. LIPIcs, vol. 141, pp. 9:1\u20139:16 (2019)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-23250-4_3","volume-title":"Intelligent Computer Mathematics","author":"K Ber\u010di\u010d","year":"2019","unstructured":"Ber\u010di\u010d, K., Kohlhase, M., Rabe, F.: Towards a unified mathematical data infrastructure: database and interface generation. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 28\u201343. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_3"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0 \u2013 the core of the TPTP language for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 491\u2013506. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_41"},{"key":"9_CR10","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R Constable","year":"1986","unstructured":"Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Upper Saddle River (1986)"},{"key":"9_CR11","volume-title":"Combinatory Logic","author":"H Curry","year":"1958","unstructured":"Curry, H., Feys, R.: Combinatory Logic. North-Holland, Amsterdam (1958)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-14418-9_11","volume-title":"Controlled Natural Language","author":"M Cramer","year":"2010","unstructured":"Cramer, M., Fisseni, B., Koepke, P., K\u00fchlwein, D., Schr\u00f6der, B., Veldman, J.: The Naproche project controlled natural language proof checking of mathematical texts. In: Fuchs, N.E. (ed.) CNL 2009. LNCS (LNAI), vol. 5972, pp. 170\u2013186. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14418-9_11"},{"issue":"2\/3","key":"9_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-22673-1_24","volume-title":"Intelligent Computer Mathematics","author":"M Codescu","year":"2011","unstructured":"Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project abstract: logic atlas and integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 289\u2013291. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_24"},{"issue":"1","key":"9_CR15","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(1), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9_CR16","unstructured":"Coq Development Team: The Coq proof assistant: reference manual. Technical report, INRIA (2015)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-662-48899-7_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Dunchev","year":"2015","unstructured":"Dunchev, C., Guidi, F., Sacerdoti Coen, C., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 460\u2013468. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-42547-4_9","volume-title":"Intelligent Computer Mathematics","author":"P-O Dehaye","year":"2016","unstructured":"Dehaye, P.-O., et al.: Interoperability in the OpenDreamKit project: the math-in-the-middle approach. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 117\u2013131. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42547-4_9"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"9_CR20","unstructured":"Common Logic editors: Common Logic (CL) \u2013 A framework for a family of logic-based languages. Technical Report 24707, ISO\/IEC (2007)"},{"issue":"2","key":"9_CR21","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W Farmer","year":"1993","unstructured":"Farmer, W., Guttman, J., Thayer, F.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213\u2013248 (1993)","journal-title":"J. Autom. Reason."},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-37012-0_2","volume-title":"The Language of Mathematics","author":"M Ganesalingam","year":"2013","unstructured":"Ganesalingam, M.: The language of mathematics. In: Ganesalingam, M. (ed.) The Language of Mathematics. LNCS, vol. 7805, pp. 17\u201338. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37012-0_2"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-319-08434-3_31","volume-title":"Intelligent Computer Mathematics","author":"D Ginev","year":"2014","unstructured":"Ginev, D., Corneli, J.: NNexus reloaded. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 423\u2013426. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_31"},{"key":"9_CR25","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. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-319-42432-3_58","volume-title":"Mathematical Software \u2013 ICMS 2016","author":"D Ginev","year":"2016","unstructured":"Ginev, D., et al.: The SMGloM project and system: towards a terminology and ontology for mathematics. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 451\u2013457. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42432-3_58"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-662-48899-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T Gauthier","year":"2015","unstructured":"Gauthier, T., Kaliszyk, C.: Sharing HOL4 and HOL light proof knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 372\u2013386. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_26"},{"key":"9_CR28","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.jsc.2018.04.005","volume":"90","author":"T Gauthier","year":"2019","unstructured":"Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symb. Comput. 90, 89\u2013123 (2019)","journal-title":"J. Symb. Comput."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Hales, T.: Dense Sphere Packings: A Blueprint for Formal Proofs. London Mathematical Society Lecture Note Series, vol. 400. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139193894"},{"key":"9_CR30","unstructured":"Hales, T.: Developments in formal proofs. S\u00e9minaire Bourbaki, 1086, 2013\u20132014. arxiv.org\/abs\/1408.6474"},{"key":"9_CR31","unstructured":"Hales, T.: The formal abstracts project (2017). https:\/\/formalabstracts.github.io\/"},{"key":"9_CR32","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. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"issue":"1","key":"9_CR33","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9_CR34","unstructured":"HOL4 development team. https:\/\/hol-theorem-prover.org\/"},{"key":"9_CR35","first-page":"479","volume-title":"Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism","author":"W Howard","year":"1980","unstructured":"Howard, W.: The formulas-as-types notion of construction. In: To, H.B. (ed.) Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479\u2013490. Academic Press, Cambridge (1980)"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-642-02614-0_38","volume-title":"Intelligent Computer Mathematics","author":"P Horn","year":"2009","unstructured":"Horn, P., Roozemond, D.: OpenMath in SCIEnce: SCSCP and POPCORN. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS (LNAI), vol. 5625, pp. 474\u2013479. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02614-0_38"},{"key":"9_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-319-20615-8_11","volume-title":"Intelligent Computer Mathematics","author":"F Horozal","year":"2015","unstructured":"Horozal, F., Rabe, F.: Formal logic definitions for interchange languages. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 171\u2013186. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-20615-8_11"},{"key":"9_CR38","unstructured":"Humayoun, M.: Developing system MathNat for automatic formalization of mathematical texts. Ph.D. thesis, Universit\u00e9 de Grenoble (2012)"},{"key":"9_CR39","unstructured":"Hurd, J.: OpenTheory: package management for higher order logic theories. In: Dos Reis, G., Th\u00e9ry, L. (eds.) Programming Languages for Mechanized Mathematics Systems, pp. 31\u201337. ACM (2009)"},{"key":"9_CR40","unstructured":"Iancu, M., Kohlhase, M., Rabe, F.: Translating the Mizar Mathematical Library into OMDoc format. Technical Report KWARC Report-01\/11, Jacobs University Bremen (2011)"},{"issue":"1","key":"9_CR41","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"9_CR42","unstructured":"Kaliszyk, C., Kohlhase, M., M\u00fcller, D., Rabe, F.: A standard for aligning mathematical concepts. In: Kohlhase, A., et al. (eds.) Work in Progress at CICM 2016, pp. 229\u2013244. CEUR-WS.org (2016)"},{"key":"9_CR43","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)"},{"key":"9_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-319-66107-0_21","volume-title":"Interactive Theorem Proving","author":"M Kohlhase","year":"2017","unstructured":"Kohlhase, M., M\u00fcller, D., Owre, S., Rabe, F.: Making PVS accessible to generic services by\u00a0interpretation in a universal format. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 319\u2013335. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_21"},{"key":"9_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-72453-9_14","volume-title":"Mathematical Aspects of Computer and Information Sciences","author":"M Kohlhase","year":"2017","unstructured":"Kohlhase, M., et al.: Knowledge-based interoperability for mathematical software systems. In: Bl\u00f6mer, J., Kotsireas, I.S., Kutsia, T., Simos, D.E. (eds.) MACIS 2017. LNCS, vol. 10693, pp. 195\u2013210. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72453-9_14"},{"key":"9_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-31374-5_26","volume-title":"Intelligent Computer Mathematics","author":"K Kofler","year":"2012","unstructured":"Kofler, K., Neumaier, A.: DynGenPar \u2013 a dynamic generalized parser for\u00a0common mathematical language. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 386\u2013401. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_26"},{"issue":"2","key":"9_CR47","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D Knuth","year":"1984","unstructured":"Knuth, D.: Literate programming. Comput. J. 27(2), 97\u2013111 (1984)","journal-title":"Comput. J."},{"key":"9_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol. 4180. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11826095"},{"key":"9_CR49","unstructured":"Kohlhase, M.: Using as a semantic markup format. Math. Comput. Sci. 2(2), 279\u2013304 (2008)"},{"issue":"3","key":"9_CR50","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1007\/s10817-018-9479-z","volume":"63","author":"C Kaliszyk","year":"2019","unstructured":"Kaliszyk, C., P\u0105k, K.: Semantics of Mizar as an Isabelle object logic. J. Autom. Reason. 63(3), 557\u2013595 (2019)","journal-title":"J. Autom. Reason."},{"key":"9_CR51","unstructured":"Kaliszyk, C., P\u0105k, K.: Declarative proof translation (short paper). In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). LIPIcs, vol. 141, pp. 35:1\u201335:7 (2019)"},{"key":"9_CR52","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1616-1","volume-title":"From Discourse to Logic. Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory, Studies in Linguistics and Philosophy","author":"H Kamp","year":"1993","unstructured":"Kamp, H., Reyle, U.: From Discourse to Logic. Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory, Studies in Linguistics and Philosophy, vol. 42. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-94-017-1616-1"},{"key":"9_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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 (LNAI), vol. 8543, pp. 357\u2013372. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_26"},{"issue":"1","key":"9_CR54","first-page":"201","volume":"9","author":"M Kohlhase","year":"2016","unstructured":"Kohlhase, M., Rabe, F.: QED reloaded: towards a pluralistic formal library of mathematical knowledge. J. Form. Reason. 9(1), 201\u2013234 (2016)","journal-title":"J. Form. Reason."},{"key":"9_CR55","unstructured":"Kohlhase, M., Rabe, F.: Experiences from Exporting Major Proof Assistant Libraries (2020). https:\/\/kwarc.info\/people\/frabe\/Research\/KR_oafexp_20.pdf"},{"key":"9_CR56","unstructured":"Kaliszyk, C., Rabe, F., Sutcliffe, G.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Workshop on Practical Aspects of Automated Reasoning, pp. 41\u201355 (2016)"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"Kohlhase, M., Rabe, F., Sacerdoti Coen, C., Schaefer, J.: Logic-independent proof search in logical frameworks (short paper). In: Peltier, N., Sofronie-Stokkermans, V. (ed.) Automated Reasoning, vol. 12166, pp. 395\u2013401. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_22"},{"key":"9_CR58","unstructured":"Kohlhase, M., Rabe, F., Wenzel, M.: Making Isabelle Content Accessible in Knowledge in Representation Formats (2020). https:\/\/kwarc.info\/people\/frabe\/Research\/KRW_isabelle_19.pdf"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Kohlhase, M., Schaefer, J.: GF + MMT = GLF - from language to semantics through LF. In: Miller, D., Scagnetto, I. (eds.) Logical Frameworks and Meta-Languages: Theory and Practice, pp. 24\u201339. Open Publishing Association (2019)","DOI":"10.4204\/EPTCS.307.4"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-319-66107-0_2","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2017","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Automating formalization by statistical and semantic parsing of mathematics. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 12\u201327. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_2"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Kamareddine, F., Wells, J.: Computerizing mathematical text with MathLang. In: Ayala-Rinc\u00f3n, M., Haeusler, E. (eds.) Logical and Semantic Frameworks, with Applications, pp. 5\u201330. ENTCS (2008)","DOI":"10.1016\/j.entcs.2008.03.063"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"Kamareddine, F., Wells, J., Zengler, C., Barendregt, H.: Computerising mathematical text. In: Siekmann, J. (ed.) Computational Logic. Elsevier (2014)","DOI":"10.1016\/B978-0-444-51624-4.50008-3"},{"issue":"7","key":"9_CR63","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"3","key":"9_CR64","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/1358190.1358201","volume":"41","author":"S Linton","year":"2007","unstructured":"Linton, S.: GAP: groups, algorithms, programming. ACM Commun. Comput. Algebr. 41(3), 108\u2013109 (2007)","journal-title":"ACM Commun. Comput. Algebr."},{"key":"9_CR65","volume-title":"Metamath: A Computer Language for Pure Mathematics","author":"N Megill","year":"2007","unstructured":"Megill, N.: Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville (2007)"},{"key":"9_CR66","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/942578.807067","volume":"7","author":"R Milner","year":"1972","unstructured":"Milner, R.: Logic for computable functions: descriptions of a machine implementation. ACM SIGPLAN Not. 7, 1\u20136 (1972)","journal-title":"ACM SIGPLAN Not."},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the \u201973 Logic Colloquium, pp. 73\u2013118. North-Holland (1974)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"9_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/3-540-16492-8_94","volume-title":"Third International Conference on Logic Programming","author":"DA Miller","year":"1986","unstructured":"Miller, D.A., Nadathur, G.: Higher-order logic programming. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 448\u2013462. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16492-8_94"},{"key":"9_CR69","doi-asserted-by":"crossref","unstructured":"M\u00fcller, D., Rabe, F.: Rapid prototyping formal systems in MMT: case studies. In: Miller, D., Scagnetto, I. (eds.) Logical Frameworks and Meta-languages: Theory and Practice, pp. 40\u201354 (2019)","DOI":"10.4204\/EPTCS.307.5"},{"key":"9_CR70","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-319-94205-6_38","volume-title":"Automated Reasoning","author":"D M\u00fcller","year":"2018","unstructured":"M\u00fcller, D., Rabe, F., Kohlhase, M.: Theories as types. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 575\u2013590. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_38"},{"key":"9_CR71","doi-asserted-by":"crossref","unstructured":"M\u00fcller, D., Rothgang, C., Liu, Y., Rabe, F.: Alignment-based translations across formal systems using interface theories. In: Dubois, C., Woltzenlogel Paleo, B. (eds.) Proof eXchange for Theorem Proving, pp. 77\u201393. Open Publishing Association (2017)","DOI":"10.4204\/EPTCS.262.7"},{"key":"9_CR72","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-030-23250-4_12","volume-title":"Intelligent Computer Mathematics","author":"D M\u00fcller","year":"2019","unstructured":"M\u00fcller, D., Rabe, F., Sacerdoti Coen, C.: The Coq library as a theory graph. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 171\u2013186. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_12"},{"key":"9_CR73","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-08434-3_37","volume-title":"Intelligent Computer Mathematics","author":"A Naumowicz","year":"2014","unstructured":"Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 449\u2013452. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_37"},{"key":"9_CR74","unstructured":"Norell, U.: The Agda WiKi (2005). http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"9_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"9_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"9_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541"},{"key":"9_CR78","unstructured":"Paulson, L., Coen, M.: Zermelo-Fraenkel Set Theory. Isabelle distribution, ZF\/ZF.thy (1993)"},{"key":"9_CR79","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction, pp. 202\u2013206 (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"issue":"5","key":"9_CR80","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1017\/S0960129512000424","volume":"23","author":"F Rabe","year":"2013","unstructured":"Rabe, F.: A logical framework combining model and proof theory. Math. Struct. Comput. Sci. 23(5), 945\u20131001 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"9_CR81","doi-asserted-by":"crossref","first-page":"1753","DOI":"10.1093\/logcom\/exu079","volume":"27","author":"F Rabe","year":"2017","unstructured":"Rabe, F.: How to identify, translate, and combine logics? J. Log. Comput. 27(6), 1753\u20131798 (2017)","journal-title":"J. Log. Comput."},{"issue":"4","key":"9_CR82","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3234693","volume":"19","author":"F Rabe","year":"2018","unstructured":"Rabe, F.: A Modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 1\u201343 (2018)","journal-title":"ACM Trans. Comput. Log."},{"key":"9_CR83","volume-title":"Grammatical Framework: Programming with Multilingual Grammars","author":"A Ranta","year":"2011","unstructured":"Ranta, A.: Grammatical Framework: Programming with Multilingual Grammars. CSLI Publications, Stanford (2011)"},{"issue":"1","key":"9_CR84","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"F Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1\u201354 (2013)","journal-title":"Inf. Comput."},{"key":"9_CR85","doi-asserted-by":"crossref","unstructured":"Rabe, F., Sch\u00fcrmann, C.: A practical module system for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40\u201348. ACM Press (2009)","DOI":"10.1145\/1577824.1577831"},{"key":"9_CR86","unstructured":"Stein, W., et al.: Sage Mathematics Software. The Sage Development Team (2013). http:\/\/www.sagemath.org"},{"key":"9_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32"},{"key":"9_CR88","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"9_CR89","unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: Joshi, A. (eds.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26\u201328. Morgan Kaufmann (1985)"},{"key":"9_CR90","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 244\u2013259. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_17"},{"key":"9_CR91","unstructured":"Wiedijk, F.: The QED manifesto revisited. In: From Insight to Proof, Festschrift in Honour of Andrzej Trybulec, pp. 121\u2013133 (2007)"},{"key":"9_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-662-44199-2_9","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"W Windsteiger","year":"2014","unstructured":"Windsteiger, W.: Theorema 2.0: a system for mathematical theory exploration. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 49\u201352. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44199-2_9"},{"key":"9_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-72453-9_17","volume-title":"Mathematical Aspects of Computer and Information Sciences","author":"T Wiesing","year":"2017","unstructured":"Wiesing, T., Kohlhase, M., Rabe, F.: Virtual theories \u2013 a uniform interface to mathematical knowledge bases. In: Bl\u00f6mer, J., Kotsireas, I.S., Kutsia, T., Simos, D.E. (eds.) MACIS 2017. LNCS, vol. 10693, pp. 243\u2013257. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72453-9_17"},{"key":"9_CR94","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-96812-4_22","volume-title":"Intelligent Computer Mathematics","author":"Q Wang","year":"2018","unstructured":"Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 255\u2013270. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22"},{"key":"9_CR95","unstructured":"Wolfram. Mathematica (2012)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T04:30:14Z","timestamp":1667449814000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":95,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}