{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:22:50Z","timestamp":1759882970502,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_14","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:43:34Z","timestamp":1759844614000},"page":"240-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Global, Regional, and Local Contexts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,8]]},"reference":[{"key":"14_CR1","unstructured":"R.\u00a0Ausbrooks, S.\u00a0Buswell, D.\u00a0Carlisle, S.\u00a0Dalmas, S.\u00a0Devitt, A.\u00a0Diaz, M.\u00a0Froumentin, R.\u00a0Hunter, P.\u00a0Ion, M.\u00a0Kohlhase, R.\u00a0Miner, N.\u00a0Poppelier, B.\u00a0Smith, N.\u00a0Soiffer, R.\u00a0Sutor, and S.\u00a0Watt. Mathematical Markup Language (MathML) Version 2.0 (second edition), 2003. See http:\/\/www.w3.org\/TR\/MathML2."},{"key":"14_CR2","unstructured":"S.\u00a0Buswell, O.\u00a0Caprotti, D.\u00a0Carlisle, M.\u00a0Dewar, M.\u00a0Gaetano, and M.\u00a0Kohlhase. The Open Math Standard, Version 2.0. Technical report, The Open Math Society, 2004. See http:\/\/www.openmath.org\/standard\/om20."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"J.\u00a0Carette, W.\u00a0Farmer, and Y.\u00a0Sharoda. Leveraging the information contained in theory presentations. In C.\u00a0Benzm\u00fcller and B.\u00a0Miller, editors, Intelligent Computer Mathematics, volume 12236, pages 55\u201370. Springer, 2020.","DOI":"10.1007\/978-3-030-53518-6_4"},{"key":"14_CR4","unstructured":"J.\u00a0Carette and R.\u00a0O\u2019Connor. Theory Presentation Combinators. In J.\u00a0Jeuring, J.\u00a0Campbell, J.\u00a0Carette, G.\u00a0Dos Reis, P.\u00a0Sojka, M.\u00a0Wenzel, and V.\u00a0Sorge, editors, Intelligent Computer Mathematics, volume 7362, pages 202\u2013215. Springer, 2012."},{"key":"14_CR5","unstructured":"Coq Development Team. The Coq Proof Assistant: Reference Manual. Technical report, INRIA, 2015."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"W.\u00a0Farmer, J.\u00a0Guttman, and F.\u00a0Thayer. IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning, 11(2):213\u2013248, 1993.","DOI":"10.1007\/BF00881906"},{"key":"14_CR7","unstructured":"T.\u00a0Hardin et\u00a0al. The focalize essential, 2012. http:\/\/focalize.inria.fr\/."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"F.\u00a0Horozal, M.\u00a0Kohlhase, and F.\u00a0Rabe. Extending MKM Formats at the Statement Level. In J.\u00a0Campbell, J.\u00a0Carette, G.\u00a0Dos Reis, J.\u00a0Jeuring, P.\u00a0Sojka, V.\u00a0Sorge, and M.\u00a0Wenzel, editors, Intelligent Computer Mathematics, pages 64\u201379. Springer, 2012.","DOI":"10.1007\/978-3-642-31374-5_5"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"R.\u00a0Jenks and R.\u00a0Sutor. AXIOM: The Scientific Computation System. Springer, 1992.","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"14_CR10","unstructured":"M.\u00a0Kohlhase and S.\u00a0Kuschert. Dynamic lambda calculus. In Meeting on Mathematics of Language, pages 85\u201392, 1997. https:\/\/kwarc.info\/people\/mkohlhase\/papers\/dlc00.pdf."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kohlhase. OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). Number 4180 in Lecture Notes in Artificial Intelligence. Springer, 2006.","DOI":"10.1007\/11826095"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kohlhase. Using \n\n                    \n                    \n                      The image shows the word \"LaTeX\" styled in a distinctive font, commonly used to represent the typesetting system for mathematical and scientific documents.\n                    \n                   as a Semantic Markup Format. Mathematics in Computer Science, 2(2):279\u2013304, 2008.","DOI":"10.1007\/s11786-008-0055-5"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"F.\u00a0Kamm\u00fcller, M.\u00a0Wenzel, and L.\u00a0Paulson. Locales \u2013 a Sectioning Concept for Isabelle. In Y.\u00a0Bertot, G.\u00a0Dowek, A.\u00a0Hirschowitz, C.\u00a0Paulin, and L.\u00a0Thery, editors, Theorem Proving in Higher Order Logics, pages 149\u2013166. Springer, 1999.","DOI":"10.1007\/3-540-48256-3_11"},{"key":"14_CR14","unstructured":"P.\u00a0Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"D.\u00a0M\u00fcller, F.\u00a0Rabe, and M.\u00a0Kohlhase. Theories as Types. In D.\u00a0Galmiche, S.\u00a0Schulz, and R.\u00a0Sebastiani, editors, Automated Reasoning, pages 575\u2013590. Springer, 2018.","DOI":"10.1007\/978-3-319-94205-6_38"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"S.\u00a0Owre, J.\u00a0Rushby, and N.\u00a0Shankar. PVS: A Prototype Verification System. In D.\u00a0Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748\u2013752. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"L.\u00a0Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"F.\u00a0Rabe and M.\u00a0Kohlhase. A Scalable Module System. Information and Computation, 230(1):1\u201354, 2013.","DOI":"10.1016\/j.ic.2013.06.001"},{"key":"14_CR19","unstructured":"Rocq Consortium. The Rocq Prover: Reference Manual. Technical report, INRIA, 2025."},{"key":"14_CR20","unstructured":"W.\u00a0Stein et\u00a0al. Sage Mathematics Software. The Sage Development Team, 2013. http:\/\/www.sagemath.org."},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Sharoda and F.\u00a0Rabe. Diagram Operators in MMT. In C.\u00a0Kaliszyk, E.\u00a0Brady, A.\u00a0Kohlhase, and C.\u00a0Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 211\u2013226. Springer, 2019.","DOI":"10.1007\/978-3-030-23250-4_15"},{"key":"14_CR22","unstructured":"A.\u00a0Trybulec and H.\u00a0Blair. Computer Assisted Reasoning with MIZAR. In A.\u00a0Joshi, editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence, pages 26\u201328. Morgan Kaufmann, 1985."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"T.\u00a0Wiesing, M.\u00a0Kohlhase, and F.\u00a0Rabe. Virtual Theories \u2013 A Uniform Interface to Mathematical Knowledge Bases. In J.\u00a0Bl\u00f6mer, I.\u00a0Kotsireas, T.\u00a0Kutsia, and D.\u00a0Simos, editors, Mathematical Aspects of Computer and Information Sciences, pages 243\u2013257. Springer, 2017.","DOI":"10.1007\/978-3-319-72453-9_17"}],"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-032-07021-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:43:39Z","timestamp":1759844619000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,8]]},"ISBN":["9783032070203","9783032070210"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,8]]},"assertion":[{"value":"8 October 2025","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":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}