Michael Kohlhase

2025

• Betzendahl J., Lohr D., Berges MP., Kohlhase M.:
  Efficient Exam Correction at Scale: Streamlining Paper-Based Assessments with the VoLl-KOrN System
  In: Mrohs, L., Franz, J., Herrmann, D., Lindner, K., Staake, T. (ed.): Digitales Lehren und Lernen an der Hochschule Strategien - Bedingungen - Umsetzung, Bielefeld: transcript, 2025
  ISBN: 978-3-8376-7120-9
  URL: https://www.transcript-verlag.de/978-3-8376-7120-9/digitales-lehren-und-lernen-an-der-hochschule/
• Lohr D., Berges MP., Chugh A., Kohlhase M., Müller D.:
  Leveraging Large Language Models to Generate Course-specific Semantically Annotated Learning Objects
  In: Journal of Computer Assisted Learning 41 (2025), p. e13101
  ISSN: 0266-4909
  DOI: 10.1111/jcal.13101
  URL: https://onlinelibrary.wiley.com/doi/10.1111/jcal.13101

2024

• Adrian A., Basaran OA., Dykes N., Evert S., Gritz M., Humml M., Kohlhase M., Lindner J., Maier A., Prettner S., Rapp M., Schröder L., Stürmer V.:
  DIREGA – Building Decision Support for German Register Law
  JURIX 2024 (Brno, December 11, 2024 - December 13, 2024)
  In: Jaromir Savelka, Jakub Harasta, Tereza Novotna, Jakub Misek (ed.): Frontiers in Artificial Intelligence and Applications 2024
  DOI: 10.3233/FAIA241269
  URL: https://ebooks.iospress.nl/volumearticle/71034
• Betzendahl J., Kohlhase M., Müller D.:
  Guided Tours in ALeA: Assembling Tailored Educational Dialogues from Semantically Annotated Learning Objects
  International Workshops of the 26th European Conference on Artificial Intelligence, ECAI 2023 (Kraków, POL, September 30, 2023 - October 4, 2023)
  In: Sławomir Nowaczyk, Przemysław Biecek, Neo Christopher Chung, Mauro Vallati, Paweł Skruch, Joanna Jaworek-Korjakowska, Simon Parkinson, Alexandros Nikitas, Martin Atzmüller, Tomáš Kliegr, Ute Schmid, Szymon Bobek, Nada Lavrac, Marieke Peeters, Roland van Dierendonck, Saskia Robben, Eunika Mercier-Laurent, Gülgün Kayakutlu, Mieczyslaw Lech Owoc, Karl Mason, Abdul Wahid, Pierangela Bruno, Francesco Calimeri, Francesco Cauteruccio, Giorgio Terracina, Diedrich Wolter, Jochen L. Leidner, Michael Kohlhase, Vania Dimitrova (ed.): Communications in Computer and Information Science 2024
  DOI: 10.1007/978-3-031-50485-3_39
• Kohlhase M., Berges MP., Grubert J., Henrich A., Landes D., Leidner JL., Mittag F., Nicklas D., Schmid U., Sedlmaier Y., Ulbrich-vom Ende A., Wolter D.:
  Project VoLL-KI: Learning from Learners
  In: Künstliche Intelligenz (2024)
  ISSN: 0933-1875
  DOI: 10.1007/s13218-024-00846-9
• Kohlhase M., Schütz M.:
  Reusing Learning Objects via Theory Morphisms
  17th International Conference on Intelligent Computer Mathematics, CICM 2024 (Montreal, QC, CAN, August 5, 2024 - August 9, 2024)
  In: Andrea Kohlhase, Laura Kovács (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2024
  DOI: 10.1007/978-3-031-66997-2_10
• Kruse-Kurbach T., Lohr D., Berges MP., Kohlhase M., Moghbeli Damaneh H., Schütz M.:
  Term Extraction for Domain Modeling
  22. Fachtagung Bildungstechnologien (DELFI) (Fulda, September 9, 2024 - September 11, 2024)
  In: Gesellschaft für Informatik e.V. (ed.): Proceedings of the 22. Fachtagung Bildungstechnologien (DELFI) 2024
  DOI: 10.18420/delfi2024_33
  URL: https://dl.gi.de/items/5f135f89-1d83-4a3f-ae8e-a2e2a09a413b

2023

• Berges MP., Betzendahl J., Chugh A., Kohlhase M., Lohr D., Müller D.:
  Learning Support Systems based on Mathematical Knowledge Management
  16th Conference on Intelligent Computer Mathematics (CICM 2023) (Cambridge, September 4, 2023 - September 8, 2023)
  In: Lecture Notes in Computer Science, Cham: 2023
• Kruse T., Berges MP., Betzendahl J., Kohlhase M., Lohr D., Müller D.:
  Learning with ALeA: Tailored experiences through annotated course material
  Workshop KI-Bildung (Berlin, September 28, 2023 - September 28, 2023)
  In: Maike Klein, Daniel Krupka, Cornelia Winter, Volker Wohlgemuth (ed.): INFORMATIK 2023. Designing Futures: Zukünfte gestalten, Bonn: 2023
  URL: https://nextcloud.gi.de/s/Y28MkNMjGnE2JY9
• Lohr D., Berges MP., Kohlhase M., Müller D., Rapp M.:
  The Y-Model - Formalization of Computer-Science Tasks in the Context of Adaptive Learning Systems
  IEEE German Education Conference (GeCon) (Berlin, August 2, 2023 - August 4, 2023)
  DOI: 10.1109/GECon58119.2023.10295148
• Lohr D., Berges MP., Kohlhase M., Rabe F.:
  The Potential of Answer Classes in Large-scale Written Computer-Science Exams
  Hochschuldidaktik Informatik (HDI) 2021 (Aachen, September 13, 2023 - September 14, 2023)
• Schaefer JF., Kohlhase M.:
  Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters
  Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023 (Cambridge, GBR, September 5, 2023 - September 8, 2023)
  In: Catherine Dubois, Manfred Kerber (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2023
  DOI: 10.1007/978-3-031-42753-4_13

2022

• Asakura T., Miyao Y., Aizawa A., Kohlhase M.:
  MioGatto: A Math Identifier-oriented Grounding Annotation Tool
  Joint of the 5th Workshop on Formal Mathematics for Mathematicians, FMM 2019, 2nd Workshop on Formal Verification of Physical Systems, FVPS 2021, 13th Workshop on Mathematical User Interaction, MathUI 2021, 2021 Workshop on Natural Formal Mathematics, NatFoM 2021, and 31st OpenMath Workshops, OM 2021 Doctoral Program and Work in Progress at the 14th Conference on Intelligent Computer Mathematics, CICM-WS 2021 (Virtual, Online, July 26, 2021 - July 31, 2021)
  In: Jasmin Blanchette, James Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Muller, Yasmine Sharoda, Claudio Sacerdoti Coen (ed.): Workshop Papers of the 14th Conference on Intelligent Computer Mathematics (CICM 2021) 2022
• Kohlhase A., Kohlhase M.:
  Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
  Joint of the 5th Workshop on Formal Mathematics for Mathematicians, FMM 2019, 2nd Workshop on Formal Verification of Physical Systems, FVPS 2021, 13th Workshop on Mathematical User Interaction, MathUI 2021, 2021 Workshop on Natural Formal Mathematics, NatFoM 2021, and 31st OpenMath Workshops, OM 2021 Doctoral Program and Work in Progress at the 14th Conference on Intelligent Computer Mathematics, CICM-WS 2021 (Virtual, Online, ROU, July 26, 2021 - July 31, 2021)
  In: Jasmin Blanchette, James Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Muller, Yasmine Sharoda, Claudio Sacerdoti Coen (ed.): CEUR Workshop Proceedings 2022
• Kohlhase M., Marcus R., Roux N., Schihada J.:
  Dynamic User Interfaces via Incremental Knowledge Management
  14th Conference on Intelligent Computer Mathematics (CICM 2021) (Virtual, Timisoara, July 26, 2021 - July 31, 2021)
  In: Jasmin Blanchette, James Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Muller, Yasmine Sharoda, Claudio Sacerdoti Coen (ed.): CICM-WS 2021: Workshop Papers of the 14th Conference on Intelligent Computer Mathematics (CICM 2021). Joint Proceedings of the FMM, FVPS, MathUI, NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021) 2022
  URL: https://ceur-ws.org/Vol-3377/mathui7.pdf
• Kohlhase M., Müller D.:
  System Description STEX3-A LATEX-Based Ecosystem for Semantic/Active Mathematical Documents
  15th International Conference on Intelligent Computer Mathematics (CICM) part of the Computational Logic Autumn Summit (CLAS) (Tbilisi)
  In: INTELLIGENT COMPUTER MATHEMATICS, CICM 2022, CHAM: 2022
  DOI: 10.1007/978-3-031-16681-5_13
• Müller D., Kohlhase M.:
  Injecting Formal Mathematics Into LATEX
  15th International Conference on Intelligent Computer Mathematics (CICM) part of the Computational Logic Autumn Summit (CLAS) (Tbilisi)
  In: INTELLIGENT COMPUTER MATHEMATICS, CICM 2022, CHAM: 2022
  DOI: 10.1007/978-3-031-16681-5_12

2021

• Adrian A., Kohlhase M., Rapp M.:
  A novel understanding of legal syllogism as a starting point for better legal symbolic AI systems
  In: Jusletter IT (2021), p. 169-178
  ISSN: 1664-848X
  DOI: 10.38023/1945d5d5-b8fe-40b6-b05c-00e55cfb8bad
• Aizawa A., Kohlhase M.:
  Mathematical Information Retrieval
  In: Tetsuya Sakai, Douglas W. Oard, Noriko Kando (ed.): Evaluating Information Retrieval and Access Tasks, Singapore: Springer Nature, 2021, p. 169-185 (Information Retrieval Series, Vol.43)
  ISBN: 978-981-15-5554-1
  DOI: 10.1007/978-981-15-5554-1_12
• Kohlhase M., Adrian A., Rapp M.:
  Context graphs for Ampliative analogical legal reasoning and argumentation
  In: Jusletter IT (2021), p. 231-240
  ISSN: 1664-848X
  DOI: 10.38023/eb626395-40e6-433f-b3b2-50523a4a0a9c
• Kohlhase M., Rabe F.:
  Experiences from Exporting Major Proof Assistant Libraries
  In: Journal of Automated Reasoning (2021)
  ISSN: 0168-7433
  DOI: 10.1007/s10817-021-09604-0

2020

• Bercic K., Kohlhase M., Rabe F.:
  (Deep) FAIR mathematics
  In: it - Information Technology (2020)
  ISSN: 1611-2776
  DOI: 10.1515/itit-2019-0028
• Bercic K., Kohlhase M., Rabe F.:
  Towards a heterogeneous query language for mathematical knowledge
  13th International Conference on Intelligent Computer Mathematics, CICM 2020 (Bertinoro, July 26, 2020 - July 31, 2020)
  In: Christoph Benzmüller, Bruce Miller (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
  DOI: 10.1007/978-3-030-53518-6_3
• Carette J., Farmer WM., Kohlhase M., Rabe F.:
  Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge
  In: Mathematical Intelligencer (2020)
  ISSN: 0343-6993
  DOI: 10.1007/s00283-020-10006-0
• Kohlhase M., Bösl B., Marcus R., Müller D., Rochau D., Roux N., Schihada J., Stamminger M.:
  FrameIT: Detangling Knowledge Management from Game Design in Serious Games
  The 13th Conference on Intelligent Computer Mathematics (CICM 2020) (Bertinoro, July 26, 2020 - July 31, 2020)
  In: Springer (ed.): Lecture Notes in Computer Science, vol 12236 2020
  DOI: 10.1007/978-3-030-53518-6_11
• Kohlhase M., Rabe F., Sacerdoti Coen C., Schaefer JF.:
  Logic-Independent Proof Search in Logical Frameworks: (Short Paper)
  10th International Joint Conference on Automated Reasoning, IJCAR 2020 (Virtual, Online, July 1, 2020 - July 4, 2020)
  In: Nicolas Peltier, Viorica Sofronie-Stokkermans (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
  DOI: 10.1007/978-3-030-51074-9_22
• Kohlhase M., Rabe F., Wenzel M.:
  Making Isabelle Content Accessible in Knowledge Representation Formats
  25th International Conference on Types for Proofs and Programs, TYPES 2019 (Oslo, June 11, 2019 - June 14, 2019)
  In: Marc Bezem, Assia Mahboubi, Assia Mahboubi (ed.): Leibniz International Proceedings in Informatics, LIPIcs 2020
  DOI: 10.4230/LIPIcs.TYPES.2019.1
• Marcus R., Kohlhase M., Rabe F.:
  Tgview3d: A system for 3-dimensional visualization of theory graphs
  13th International Conference on Intelligent Computer Mathematics, CICM 2020 (Bertinoro, July 26, 2020 - July 31, 2020)
  In: Christoph Benzmüller, Bruce Miller (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
  DOI: 10.1007/978-3-030-53518-6_20
• Müller D., Rabe F., Rothgang C., Kohlhase M.:
  Representing Structural Language Features in Formal Meta-languages
  The 13th Conference on Intelligent Computer Mathematics (CICM 2020) (Bertinoro, July 26, 2020 - July 31, 2020)
  In: Springer (ed.): Lecture Notes in Computer Science, vol 12236 2020
  DOI: 10.1007/978-3-030-53518-6_13
• Rapp M., Adrian A., Kohlhase M.:
  Context graphs for legal reasoning and argumentation
  3rd International Workshop on Systems and Algorithms for Formal Argumentation, SAFA 2020 (Virtual, Online, September 8, 2020)
  In: Sarah A. Gaggl, Matthias Thimm, Mauro Vallati (ed.): CEUR Workshop Proceedings 2020
• Schaefer JF., Amann K., Kohlhase M.:
  Prototyping Controlled Mathematical Languages in Jupyter Notebooks
  7th International Congress on Mathematical Software, ICMS 2020 (Braunschweig, DEU, July 13, 2020 - July 16, 2020)
  In: Anna Maria Bigatti, Jacques Carette, James H. Davenport, Michael Joswig, Timo de Wolff (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2020
  DOI: 10.1007/978-3-030-52200-1_40
• Schaefer JF., Kohlhase M.:
  GLIF: A Declarative Framework for Symbolic Natural Language Understanding
  6th Workshop on Formal and Cognitive Reasoning, FCR 2020 (, September 22, 2020)
  In: Christoph Beierle, Marco Ragni, Frieder Stolzenburg, Matthias Thimm (ed.): CEUR Workshop Proceedings 2020

2019

• Amann K., Kohlhase M., Rabe F., Wiesing T.:
  Integrating Semantic Mathematical Documents and Dynamic Notebooks
  12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
  In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
  DOI: 10.1007/978-3-030-23250-4_19
• Bercic K., Kohlhase M., Rabe F.:
  Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation
  12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
  In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
  DOI: 10.1007/978-3-030-23250-4_3
• Condoluci A., Kohlhase M., Müller D., Rabe F., Sacerdoti Coen C., Wenzel M.:
  Relational Data Across Mathematical Libraries
  12th International Conference on Intelligent Computer Mathematics, CICM 2019 (Prague, July 8, 2019 - July 12, 2019)
  In: Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (ed.): Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2019
  DOI: 10.1007/978-3-030-23250-4_5
• Kohlhase M., Schaefer JF.:
  GF + MMT = GLF from language to semantics through LF
  14th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2019 (Vancouver, BC, CAN, June 22, 2019)
  In: Dale Miller, Ivan Scagnetto (ed.): Electronic Proceedings in Theoretical Computer Science, EPTCS 2019
  DOI: 10.4204/EPTCS.307.4

2018

• Kohlhase A., Kohlhase M., Ouypornkochagorn T.:
  Discourse phenomena in mathematical documents
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_14
• Kohlhase M.:
  Towards context graphs for argumentation logics
  2018 Conference "Learning, Knowledge, Data, Analytics", LWDA 2018
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85053594694&origin=inward
• Kohlhase M., Betzendahl J.:
  Translating the IMPS theory library to MMT/OMDoc
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_2
• Kohlhase M., Betzendahl J.:
  Translating the IMPS theory library to MMT/OMDoc
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_2
• Kohlhase M., Kohlhase A., Ouypornkochagorn T.:
  Discourse phenomena in mathematical documents
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_14
• Kohlhase M., Wiesing T.:
  A proposal for an OpenMath JSON encoding
  Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060579045&origin=inward
• Müller D., Kohlhase M., Koprucki T., Tabelow K., Rabe F.:
  Model pathway diagrams for the representation of mathematical models
  In: Optical and Quantum Electronics 50 (2018), Article No.: ARTN 70
  ISSN: 0306-8919
  DOI: 10.1007/s11082-018-1321-7
• Müller D., Kohlhase M., Rabe F.:
  Automatically finding theory morphisms for knowledge management
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_18
• Müller D., Kohlhase M., Rabe F.:
  Theories as Types
  9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
  DOI: 10.1007/978-3-319-94205-6_38
• Pollinger T., Kohlhase M., Köstler H.:
  Knowledge amalgamation for computational science and engineering
  11th International Conference on Intelligent Computer Mathematics, CICM 2018
  DOI: 10.1007/978-3-319-96812-4_20
• Schaefer JF., Kohlhase M.:
  Syntactic/semantic analysis for high-precision math linguistics
  Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060658105&origin=inward
• Wiesing T., Kohlhase M.:
  A proposal for an openMath JSON encoding
  Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation, CME-EI 2018, Formal Mathematics for Mathematicians, FMM 2018, Computer Algebra in the Age of Types, CAAT 2018, Formal Verification of Physical Systems, FVPS 2018, Mathematical Models and Mathematical Software as Research Data 2018, M3SRD 2018 and 29th OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS 2018
  In: Proceedings of the Joint 2018 Computer Mathematics in Education - Enlightenment or Incantation 2018
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85060579045∨igin=inward

2017

• Kaliszyk C., Kohlhase M., Müller D., Rabe F.:
  A standard for aligning mathematical concepts
  2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973947&origin=inward
• Kohlhase M.:
  Math object identifiers - Towards research data in mathematics
  Lernen, Wissen, Daten, Analyse - 2017 Learning. Knowledge. Data. Analytics, LWDA 2017 (Rostock)
  In: Lernen, Wissen, Daten, Analyse - 2017 Learning. Knowledge. Data. Analytics, LWDA 2017 2017
  URL: https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85030126012&origin=inward
• Toloaca I., Kohlhase M.:
  Notation-based semantification
  MathUI 2016
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85018973557∨igin=inward
• Kohlhase M., Kohlhase A., Fürsich M.:
  Visual structure in mathematical expressions
  10th International Conference on Intelligent Computer Mathematics, CICM 2017
  DOI: 10.1007/978-3-319-62075-6_15
• Kohlhase M., Koprucki T., Müller D., Tabelow K.:
  Mathematical models as research data via flexiformal theory graphs
  In: 10th International Conference on Intelligent Computer Mathematics, CICM 2017 2017
  DOI: 10.1007/978-3-319-62075-6_16
• Kohlhase M., Müller D., Owre S., Rabe F.:
  Making PVS accessible to generic services by interpretation in a universal format
  8th International Conference on Interactive Theorem Proving, ITP 2017
  DOI: 10.1007/978-3-319-66107-0_21
• Kohlhase M., Müller D., Pfeiffer M., Rabe F., Thiery N., Vasilyev V., Wiesing T.:
  Knowledge-Based Interoperability for Mathematical Software Systems
  In: Johannes Blömer and Temur Kutsia and Dimitris Simos (ed.): MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences 2017
• Kohlhase M., Müller D., Rabe F., Kaliszyk C., Gauthier T.:
  Classification of alignments between concepts of formal mathematical systems
  10th International Conference on Intelligent Computer Mathematics, CICM 2017
  In: 10th International Conference on Intelligent Computer Mathematics, CICM 2017 2017
  DOI: 10.1007/978-3-319-62075-6_7
• Kohlhase M., Müller D., Rochau D.:
  FrameIT reloaded: Serious math games from modular math ontologies
  2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016
  In: 2016 Joint Formal Mathematics for Mathematicians, FM4M 2016, 11th Workshop on Mathematical User Interfaces, MathUI 2016, and 2016 Workshop on Theorem Proving Components for Educational Software, ThEdu 2016, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, CICM-WS-WIP 2016 2017
• Kohlhase M., Sperber W.:
  Software citations, information systems, and beyond
  10th International Conference on Intelligent Computer Mathematics, CICM 2017
  DOI: 10.1007/978-3-319-62075-6_8
• Kohlhase M., De Feo L., Müller D., Pfeiffer M., Rabe F., Thiéry N., Vasilyev V., Wiesing T.:
  Knowledge-based interoperability for mathematical software systems
  7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
  DOI: 10.1007/978-3-319-72453-9_14
• Koprucki T., Kohlhase M., Müller D., Tabelow K.:
  Mathematical models as research data in numerical simulation of opto-electronic devices
  17th International Conference on Numerical Simulation of Optoelectronic Devices, NUSOD 2017
  DOI: 10.1109/NUSOD.2017.8010073
• Müller D., Kohlhase M., Rupprecht M.:
  A Flexible, Interactive Theory-Graph Viewer
  CICM 2017
• Wiesing T., Kohlhase M., Rabe F.:
  Virtual theories – A uniform interface to mathematical knowledge bases
  7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
  DOI: 10.1007/978-3-319-72453-9_17
• Wiesing T., Kohlhase M., Rabe F.:
  Virtual theories – A uniform interface to mathematical knowledge bases
  7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
  DOI: 10.1007/978-3-319-72453-9_17
• Wiesing T., Kohlhase M., Rabe F., Kohlhase M.:
  Virtual Theories -- A Uniform Interface to Mathematical Knowledge Bases
  7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
  In: Johannes Blömer and Temur Kutsia and Dimitris Simos (ed.): MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences 2017
  DOI: 10.1007/978-3-319-72453-9_17

2016

• Ginev D., Iancu M., Jucovshi C., Kohlhase A., Kohlhase M., Oripov A., Schefter J., Sperber W., Teschke O., Wiesing T.:
  The SMGloM project and system: Towards a terminology and ontology for mathematics
  Springer Verlag, 2016
  ISBN: 9783319424316
  DOI: 10.1007/978-3-319-42432-3_58
• Hambasan R., Kohlhase M.:
  Faceted search for mathematics
  6th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2015
  DOI: 10.1007/978-3-319-32859-1_35
• Kohlhase M., Rabe F.:
  QED reloaded: Towards a pluralistic formal library of mathematical knowledge
  In: Journal of Formalized Reasoning 9 (2016), p. 201-234
  ISSN: 1972-5787
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84957079748&origin=inward
• Luzhnica E., Kohlhase M.:
  Formula semantification and automated relation finding in the on-line encyclopedia for integer sequences
  5th International Conference on Mathematical Software, ICMS 2016
  DOI: 10.1007/978-3-319-42432-3_60
• Müller D., Wiesing T., Thiery N., Dehaye P., Iancu M., Kohlhase M., Konovalov A., Lelièvre S., Pfeiffer M., Rabe F.:
  Interoperability in the OpenDreamKit project: The math-in-the-middle approach
  9th International Conference on Intelligent Computer Mathematics, CICM 2016
  DOI: 10.1007/978-3-319-42547-4_9

2015

• Hambasan R., Kohlhase M.:
  Faceted search for mathematics
  Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84944340107&origin=inward
• Iancu M., Kohlhase M.:
  A flexiformal model of knowledge dissemination and aggregation in mathematics
  International Conference on Intelligent Computer Mathematics, CICM 2015
  DOI: 10.1007/978-3-319-20615-8_9
• Iancu M., Kohlhase M.:
  Math literate knowledge management via induced material
  International Conference on Intelligent Computer Mathematics, CICM 2015
  DOI: 10.1007/978-3-319-20615-8_12
• Kohlhase A., Kohlhase M., Guseva A.:
  Context in spreadsheet comprehension
  2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84930355041&origin=inward
• Luzhnica E., Iancu M., Kohlhase M.:
  Importing the OEIS library into OMDoc
  Learning, Knowledge, Adaptation Workshops, LWA 2015: Knowledge Discovery, Data Mining and Machine Learning, KDML 2015, Knowledge Management, FGWM 2015, Information Retrieval, IR 2015 and Database Systems, FGDB 2015
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84944342791&origin=inward
• Toader A., Kohlhase M., Kohlhase A.:
  Assessment for spreadsheets
  2nd Workshop on Software Engineering Methods in Spreadsheets, SEMS 2015, Co-located with the 37th International Conference on Software Engineering, ICSE 2015
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84930336641&origin=inward

2014

• Acevedo C., Kohlhase M.:
  Open math map: Interaction
  Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891544&origin=inward
• Breitsprecher T., Codesci M., Jucovaschi C., Kohlhase M., Schröder L., Wartzack S.:
  Towards Ontological Support for Principle Solutions in Mechanical Engineering
  8th International Conference on Formal Ontology in Information Systems (Rio de Janeiro)
  In: 8th International Conference on Formal Ontology in Information Systems 2014
  DOI: 10.3233/978-1-61499-438-1-427
• Breitsprecher T., Codescu SM., Schröder L., Wartzack S., jucovschi C., Kohlhase M.:
  Semantic Support for Engineering Design Processes
  13th International Design Conference, DESIGN 2014 (Dubrovnik)
  In: In Proc. 13th International Design Conference, DESIGN 2014 2014
  URL: https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84924387161&origin=inward
• Carette J., Farmer W., Kohlhase M.:
  Realms: A structure for consolidating knowledge about mathematical theories
  2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
  DOI: 10.1007/978-3-319-08434-3_19
• Horozal F., Rabe F., Kohlhase M.:
  Flexary operators for formalized mathematics
  2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
  DOI: 10.1007/978-3-319-08434-3_23
• Iancu M., Jucovschi C., Kohlhase M., Wiesing T.:
  System description: MathHub.info
  2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
  DOI: 10.1007/978-3-319-08434-3_33
• Iancu M., Kohlhase M., Prodescu CC.:
  Representing, archiving, and searching the space of mathematical knowledge
  4th International Congress on Mathematical Software, ICMS 2014 (Seoul)
  DOI: 10.1007/978-3-662-44199-2_5
• Kohlhase L., Kohlhase M.:
  System description: A semantics-aware LATEX-to-office converter
  2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
  DOI: 10.1007/978-3-319-08434-3_35
• Kohlhase M.:
  A data model and encoding for a semantic, multilingual terminology of mathematics
  2014 International Conference on Intelligent Computer Mathematics, CICM 2014 (Coimbra)
  DOI: 10.1007/978-3-319-08434-3_13
• Kohlhase M.:
  Extension proposal: Records in pragmatic open math
  Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924891647&origin=inward
• Kohlhase M.:
  OpenMath language extensions
  Joint of the 9th Workshop on Mathematical User Interfaces, MathUI 2014, 26th OpenMath Workshop, OpenMath 2014, 2014 Workshop on Theorem Proving Components for Educational Software, ThEdu 2014 and the Work in Progress Section of Conference on Intelligent Computer Mathematics, CICM 2014
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924873356&origin=inward
• Kohlhase M., Iancu M.:
  Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
  4th International Congress on Mathematical Software, ICMS 2014 (Seoul)
  DOI: 10.1007/978-3-662-44199-2_7

2013

• Dörrie JW., Kohlhase M.:
  OpenMathMap: Accessing Math via Interactive Maps
  Joint Workshops of the 8th Workshop on Mathematical User Interfaces, MathUI 2013, 25th OpenMath Workshop, OpenMath 2013, 5th International Workshop on Programming Languages for Mechanised Mathematical Systems, PLMMS 2013 and the 2nd International Workshop on Theorem Proving Components for Educational Software, ThEdu 2013 and Work in Progress at Conference on Intelligent Computer Mathematics, CICM 2013
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84924872163&origin=inward
• Iancu M., Kohlhase M., Rabe F., Urban J.:
  The Mizar mathematical library in OMDoc: Translation and applications
  In: Journal of Automated Reasoning 50 (2013), p. 191-202
  ISSN: 0168-7433
  DOI: 10.1007/s10817-012-9271-4
• Kohlhase A., Kohlhase M., Jucovschi C., Toader A.:
  Full semantic transparency: Overcoming boundaries of applications
  14th IFIP TC 13 International Conference on Human-Computer Interaction, INTERACT 2013 (Cape Town)
  DOI: 10.1007/978-3-642-40477-1_25
• Kohlhase M., Mance F., Rabe F.:
  A universal machine for biform theory graphs
  Conference on Intelligent Computer Mathematics, CICM 2013, Co-located with the MKM 2013, Calculemus 2013, DML 2013, and Systems and Projects 2013 (Bath)
  DOI: 10.1007/978-3-642-39320-4_6
• Lange-Bever C., Kohlhase M.:
  Mashups using mathematical knowledge: Why formulas are different
  In: Brigitte Endres-Niggemeyer (ed.): Semantic Mashups: Intelligent Reuse of Web Resources, Springer Berlin Heidelberg, 2013, p. 171-204
  ISBN: 9783642364020
  DOI: 10.1007/978-3-642-36403-7_6
• Rabe F., Kohlhase M.:
  A scalable module system
  In: Information and Computation 230 (2013), p. 1-54
  ISSN: 0890-5401
  DOI: 10.1016/j.ic.2013.06.001

2012

• Codescu SM., Horozal F., Kohlhase M., Mossakowski T., Rabe F.:
  A proof theoretic interpretation of model theoretic hiding
  20th International Workshop on Algebraic Development Techniques, WADT 2010 (Etelsen)
  DOI: 10.1007/978-3-642-28412-0_9
• Codescu SM., Horozal F., Kohlhase M., Mossakowski T., Rabe F., Sojakova K.:
  Towards logical frameworks in the heterogeneous tool set hets
  20th International Workshop on Algebraic Development Techniques, WADT 2010 (Etelsen)
  DOI: 10.1007/978-3-642-28412-0_10
• David C., Jucovschi C., Kohlhase A., Kohlhase M.:
  Semantic alliance: A framework for semantic allies
  Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
  DOI: 10.1007/978-3-642-31374-5_4
• Horozal F., Kohlhase M., Rabe F.:
  Extending MKM formats at the statement level
  Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
  DOI: 10.1007/978-3-642-31374-5_5
• Kerber M., Kohlhase M.:
  Reasoning without believing: On the mechanisation of presuppositions and partiality
  In: Journal of Applied Non-Classical Logics 22 (2012), p. 295-317
  ISSN: 1166-3081
  DOI: 10.1080/11663081.2012.705962
• Kohlhase M.:
  The flexiformalist manifesto
  14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012 (Timisoara)
  DOI: 10.1109/SYNASC.2012.78
• Kohlhase M.:
  The Planetary project: Towards eMath3.0
  Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
  DOI: 10.1007/978-3-642-31374-5_34
• Kohlhase M., Matican B., Prodescu CC.:
  MathWebSearch 0.5: Scaling an open formula search engine
  Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC 2012, Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2012, DML 2012, Conf. on Mathematical Knowledge Management, MKM 2012, Part of CICM 2012 (Bremen)
  DOI: 10.1007/978-3-642-31374-5_23
• Kohlhase M., Rabe F.:
  Semantics of OpenMath and MathML3
  In: Mathematics in Computer Science 6 (2012), p. 235-260
  ISSN: 1661-8270
  DOI: 10.1007/s11786-012-0113-x
• Lange C., Ion P., Dimou A., Bratsas C., Sperber W., Kohlhase M., Antoniou I.:
  Bringing mathematics to the web of data: The case of the mathematics subject classification
  9th Extended Semantic Web Conference, ESWC 2012 (Heraklion, Crete)
  DOI: 10.1007/978-3-642-30284-8_58

2011

• Autexier S., David C., Dietrich D., Kohlhase M., Zholudev V.:
  Workflows for the management of change in science, technologies, engineering and mathematics
  18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
  DOI: 10.1007/978-3-642-22673-1_12
• Codescu SM., Horozal F., Kohlhase M., Mossakowski T., Rabe F.:
  Project abstract: Logic atlas and integrator (LATIN)
  18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
  DOI: 10.1007/978-3-642-22673-1_24
• David C., Ginev D., Kohlhase M., Matican B., Mirea S.:
  A framework for semantic publishing of modular content objects
  1st Workshop on Semantic Publishing 2011, SePublica 2011 - Co-located with the 8th Extended Semantic Web Conference, ESWC 2011 (Hersonissos, Crete)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84890730016&origin=inward
• Ginev D., Stamerjohanns H., Kohlhase M., Miller B.:
  The LaTeXML daemon: Editable math on the collaborative web
  Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011 (Magdeburg)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874005493&origin=inward
• Horozal F., Iacob A., Jucovschi C., Kohlhase M., Rabe F.:
  Combining source, content, presentation, narration, and relational representation
  18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
  DOI: 10.1007/978-3-642-22673-1_15
• Kohlhase A., Kohlhase M.:
  Maintaining islands of consistency via versioned links
  29th ACM International Conference on Design of Communication, SIGDOC'11 (Pisa)
  DOI: 10.1145/2038476.2038510
• Wolska M., Grigore M., Kohlhase M.:
  Using discourse context to interpret object-denoting mathematical expressions
  4th Workshop Towards a Digital Mathematics Library, DML 2011
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84870532306&origin=inward
• Kohlhase M., Corneli J., David C., Ginev D., Jucovschi C., Kohlhasea A., Lange C., Matican B., Mirea S., Zholudev V.:
  The planetary system: Web 3.0 & active documents for STEM
  11th International Conference on Computational Science, ICCS 2011 (Singapore)
  DOI: 10.1016/j.procs.2011.04.063
• Kohlhase M., Kohlhase A.:
  Towards a flexible notion of document context
  29th ACM International Conference on Design of Communication, SIGDOC'11 (Pisa)
  DOI: 10.1145/2038476.2038512
• Alama J., Kohlhase M., Mamane L., Naumowicz A., Rudnicki P., Urban J.:
  Licensing the Mizar mathematical library
  18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
  DOI: 10.1007/978-3-642-22673-1_11
• Lange C., Kohlhase M., David C., Ginev D., Kohlhase A., Matican B., Mirea S., Zholudev V.:
  The planetary system: Executable science, technology, engineering and math papers
  8th Extended Semantic Web Conference, ESWC 2011 (Heraklion, Crete)
  DOI: 10.1007/978-3-642-21064-8_37
• Prodescu CC., Kohlhase M.:
  Mathwebsearch 0.5 an open formula search engine
  Symposium on Learning, Knowledge, and Adaptivity 2011, LWA 2011 (Magdeburg)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874016713&origin=inward
• Rabe F., Kohlhase M., Sacerdoti Coen C.:
  A foundational view on integration problems
  18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 (Bertinoro)
  DOI: 10.1007/978-3-642-22673-1_8

2010

• David C., Kohlhase M., Lange C., Rabe F., Zhiltsov N., Zholudev V.:
  Publishing math lecture notes as linked data
  7th Extended Semantic Web Conference, ESWC 2010 (Heraklion, Crete)
  DOI: 10.1007/978-3-642-13489-0_26
• Jucovschi C., Kohlhase M.:
  STEXIDE: An integrated development environment for STEX collections
  10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
  DOI: 10.1007/978-3-642-14128-7_29
• Kohlhase A., Kohlhase M., Lange-Bever C.:
  Dimensions of formality: A case study for MKM in software engineering
  10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
  DOI: 10.1007/978-3-642-14128-7_31
• Kohlhase A., Kohlhase M., Lange C.:
  STEX+: A system for flexible formalization of linked data
  6th International Conference on Semantic Systems, I-SEMANTICS '10 (Graz)
  DOI: 10.1145/1839707.1839712
• Kohlhase M., Rabe F., Zholudev V.:
  Towards MKM in the large: Modular representation and scalable software architecture
  10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010 (Paris)
  DOI: 10.1007/978-3-642-14128-7_32
• Kohlhase M., Zholudev V.:
  Scripting documents with XQuery: Virtual documents in TNTBase
  Balisage: The Markup Conference 2010 (Montreal, QC)
  DOI: 10.4242/BalisageVol5.Zholudev01
• Dumitrache A., Lange C., Kohlhase M., Aschenbeck N.:
  Prototyping a browser for a listed buildings database* with semantic MediaWiki
  5th Workshop on Semantic Wikis - Linking Data and People, SemWiki 2010 - 7th Extended Semantic Web Conference, ESWC 2010 (Hersonissos, Heraklion, Crete)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84873471498&origin=inward
• Stamerjohanns H., Kohlhase M., Ginev D., David C., Miller B.:
  Transforming large collections of scientific publications to XML
  In: Mathematics in Computer Science 3 (2010), p. 299-307
  ISSN: 1661-8270
  DOI: 10.1007/s11786-010-0024-7

2009

• Davenport J., Kohlhase M.:
  Unifying math ontologies: A tale of two standards
  16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
  DOI: 10.1007/978-3-642-02614-0_23
• Ginev D., Jucovschi C., Anca S., Grigore M., David C., Kohlhase M.:
  An architecture for linguistic and semantic analysis on the ARXMLIV corpus
  39th Jahrestagung der Gesellschaft fur Informatik e.V. (GI): Im Focus das Leben, INFORMATIK 2009 39th Annual Meeting of the German Informatics Society (GI): Focus on Life, INFORMATIK 2009 (Lubeck)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874316647&origin=inward
• Kohlhase A., Kohlhase M.:
  Compensating the computational bias of spreadsheets with MKM techniques
  16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
  DOI: 10.1007/978-3-642-02614-0_29
• Kohlhase A., Kohlhase M.:
  Modeling task experience in user assistance systems
  27th ACM International Conference on Design of Communication, SIGDOC'09 (Bloomington, IN)
  DOI: 10.1145/1621995.1622021
• Kohlhase A., Kohlhase M.:
  Spreadsheet interaction with frames: Exploring a mathematical practice
  16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
  DOI: 10.1007/978-3-642-02614-0_28
• Kohlhase M., Brown C., Benzmüller C.:
  Cut-simulation and impredicativity
  In: Logical Methods in Computer Science 5 (2009), p. 1-21
  ISSN: 1860-5974
  DOI: 10.2168/LMCS-5(1:6)2009
• Kohlhase M., Kohlhase A.:
  Semantic transparency in user assistance systems
  27th ACM International Conference on Design of Communication, SIGDOC'09 (Bloomington, IN)
  DOI: 10.1145/1621995.1622013
• Kohlhase M., Kohlhase A.:
  What you understand is what you get: Assessment in spreadsheets
  LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity (Darmstadt)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874134110&origin=inward
• Kohlhase M., Lange-Bever C.:
  A mathematical approach to ontology authoring and documentation
  LWA 2009 - Workshop-Woche: Lernen-Wissen-Adaptivitat - Learning, Knowledge and Adaptivity (Darmstadt)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874182293&origin=inward
• Kohlhase M., Lemburg J., Schröder L., Schulz E.:
  Formal management of CAD/CAM processes
  2nd World Congress on Formal Methods, FM 2009 (Eindhoven)
  DOI: 10.1007/978-3-642-05089-3_15
• Kohlhase M., Zholudev V.:
  TNTBase: Versioned storage for XML
  Balisage: The Markup Conference 2009 (Montreal, QC)
  DOI: 10.4242/BalisageVol3.Zholudev01
• Lange-Bever C., Kohlhase M.:
  A mathematical approach to ontology authoring and documentation
  16th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2009 and 8th Int. Conf. on Mathematical Knowledge Management, MKM 2009. Held as part of the Confs. on Intelligent Computer Mathematics, CICM 2009 (Grand Bend, ON)
  DOI: 10.1007/978-3-642-02614-0_31
• Müller C., Kohlhase M.:
  Context-aware adaptation: A case study on mathematical notations
  In: Information Systems Management 26 (2009), p. 215-230
  ISSN: 1058-0530
  DOI: 10.1080/10580530903017583
• Stamerjohanns H., Ginev D., David C., Misev D., Zamdzhiev V., Kohlhase M.:
  MathML-aware article conversion from LATEX a comparison study
  2nd Workshop on Towards a Digital Mathematics Library, DML 2009 (Grand Bend, ON)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84896692132&origin=inward
• Tranh HM., Lange-Bever C., Chulkov G., Schönwälder J., Kohlhase M.:
  Applying semantic techniques to search and analyze bug tracking data
  In: Journal of Network and Systems Management 17 (2009), p. 285-308
  ISSN: 1064-7570
  DOI: 10.1007/s10922-009-9134-4

2008

• Kohlhase M.:
  Using LATEX as a semantic markup format
  In: Mathematics in Computer Science 2 (2008), p. 279-304
  ISSN: 1661-8270
  DOI: 10.1007/s11786-008-0055-5
• Kohlhase M., Kohlhase A.:
  Semantic knowledge management for education
  In: Proceedings of the IEEE 96 (2008), p. 970-989
  ISSN: 0018-9219
  DOI: 10.1109/JPROC.2008.921606
• Kohlhase M., Lange-Bever C.:
  SWiM: A semantic wiki for mathematical knowledge management
  In: 1st Workshop on Semantic Wikis 2008
  DOI: 10.4018/978-1-59904-877-2.ch004
• Kohlhase M., Müller C., Rabe F.:
  Notations for living mathematical documents
  9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008 (Birmingham)
  DOI: 10.1007/978-3-540-85110-3_41
• Müller C., Kohlhase M.:
  Towards a community of practice toolkit based on semantically marked up artifacts
  1st World Summit on the Knowledge Society, WSKS 2008 (Athens)
  DOI: 10.1007/978-3-540-87781-3_5
• Rabe F., Kohlhase M.:
  An exchange format for modular knowledge
  LPAR 2008 Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, KEAPPA 2008 and the 7th International Workshop on the Implementation of Logics, IWIL 2008 (Doha)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84885598893&origin=inward
• Stamerjohanns H., Kohlhase M.:
  Transforming the arχiv to XML
  9th Int. Conf. Artificial Intelligence and Symbolic Computation, AISC 2008 - 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008 - 7th Int. Conf. Mathematical Knowledge Management, MKM 2008 (Birmingham)
  DOI: 10.1007/978-3-540-85110-3_46

2007

• Freksa C., Kohlhase M., Schill K.:
  Lecture Notes in Comuter Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes: Preface
  29th Annual German Conference on Artificial Intelligence (KI 2006) (Bremen)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35448943067&origin=inward
• Kohlhase A., Kohlhase M.:
  Reexamining the MKM value proposition: From math web search to math web research
  14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007 (Hagenberg)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-38049042760&origin=inward
• Kohlhase M., Mahnke A., Müller C.:
  Managing variants in document content and narrative structures
  Workshop on Learning, Knowledge, and Adaptivity, LWA 2007 (Halle)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84869721576&origin=inward
• Kohlhase M., Müller C.:
  Panta rhei
  Workshop on Learning, Knowledge, and Adaptivity, LWA 2007 (Halle)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84874010902&origin=inward
• Normann I., Kohlhase M.:
  Extended formula normalization for e-retrieval and sharing of mathematical knowledge
  14th Symposium on Calculemus 2007 and 6th International Conference on Mathematical Knowledge Management, MKM 2007 (Hagenberg)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-38049028250&origin=inward

2006

• Hilf E., Kohlhase M., Stamerjohanns H.:
  Capturing the content of physics: Systems, observables, and experiments
  5th International Conference on Mathematical Knowledge Management, MKM 2006 (Wokingham)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749546748&origin=inward
• Kohlhase A., Kohlhase M.:
  An exploration in the space of mathematical knowledge
• Kohlhase A., Kohlhase M.:
  Communities of practice in MKM: An extensional model
  5th International Conference on Mathematical Knowledge Management, MKM 2006 (Wokingham)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749542803&origin=inward
• Kohlhase M.:
  OMDoc - An open markup format for mathematical documents [version 1.2]
  2006
• Benzmüller C., Brown C., Kohlhase M.:
  Cut-simulation in impredicative logics
  Third International Joint Conference on Automated Reasoning, IJCAR 2006 (Seattle, WA)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749556449&origin=inward
• Kohlhase M., Lange-Bever C.:
  A semantic wiki for mathematical knowledge management
  1st Workshop on Semantic Wikis - From Wiki to Semantics, SemWiki 2006 - Co-located with the ESWC 2006 (Budva)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84873470933&origin=inward
• Kohlhase M., Sucan I.:
  A search engine for mathematical formulae
  8th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2006 (Beijing)
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-33749635061&origin=inward

2004

• Kohlhase M., Benzmüller C., Brown C.:
  Higher-order semantics and extensionality
  In: Journal of Symbolic Logic 69 (2004), p. 1027-1088
  ISSN: 0022-4812
  DOI: 10.2178/jsl/1102022211
• Kohlhase M., Kohlhase A.:
  CPOINT: Dissolving the author's dilemma
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35048892955&origin=inward

2003

• Kohlhase M., Anghelache R.:
  Towards collaborative content management and version control for structured mathematical knowledge
• Kohlhase M., Koller A.:
  Resource-adaptive model generation as a performance model
  In: Logic Journal of the Igpl 11 (2003), p. 435-456
  ISSN: 1367-0751

2002

• Siekmann J., Benzmüller C., Brezhnev V., Cheikhrouhou L., Fiedler A., Franke A., Horacek H., Kohlhase M., Meier A., Melis E., Moschner M., Normann I., Pollet M., Sorge V., Ullrich C., Wirth C., Zimmer J.:
  Proof development with Ωmega
  18th International Conference on Automated Deduction, CADE 2002
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84948980176&origin=inward
• Zimmer J., Kohlhase M.:
  System description: The mathweb software bus for distributed mathematical reasoning
  18th International Conference on Automated Deduction, CADE 2002
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84948958841&origin=inward

2001

• Kohlhase M., Franke A.:
  MBase: Representing knowledge and context for the integration of mathematical software systems
  In: Journal of Symbolic Computation 32 (2001), p. 365-402
  ISSN: 0747-7171
  DOI: 10.1006/jsco.2000.0468
• Kohlhase M.:
  OMDoc: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge
  5th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2000
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84974687882&origin=inward
• Kohlhase M., Armando A., Ranise S.:
  Communication Protocols for mathematical services based on KQML and OMRS

2000

• Bos J., Kohlhase M. (ed.):
  ICoS-2 Inference in Computational Semantics. Workshop Proceedings
  2000
• Franke A., Kohlhase M.:
  System description: MBASE, an open mathematical knowledge base
  17th International Conference on Automated Deduction, CADE 2000
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84937429345&origin=inward
• Hutter D., Kohlhase M.:
  Managing structural information by higher-order colored unification
  In: Journal of Automated Reasoning 25 (2000), p. 123-164
  ISSN: 0168-7433
  DOI: 10.1023/A:1006282725324
• Kohlhase M.:
  Model generation for discourse representation theory
  In: Werner Horn (ed.): Proceedings of of the 14th European Conference on Artifical Intelligence 2000
• Pinkal M., Kohlhase M.:
  Feature logic for dotted types: A formalism for complex word meanings
  In: Proceedings of the 38th Annual Meeting of the Association for Computational Linguistics 2000

1999

• Franke A., Kohlhase M.:
  System description: MathWeb, an agent-based communication layer for distributed automated theorem proving
  16th International Conference on Automated Deduction, CADE 1999
  DOI: 10.1007/3-540-48660-7_17
• Franke A., Hess S., Jung C., Kohlhase M., Sorge V.:
  Agent-oriented integration of distributed mathematical services
  In: Journal of Universal Computer Science 5 (1999), p. 156-187
  ISSN: 0958-695X
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0001536634&origin=inward
• Siekmann J., Hess S., Benzmüller C., Cheikhrouhou L., Fiedler A., Horacek H., Kohlhase M., Konrad K., Meier A., Melis E., Pollet M., Sorge V.:
  ℒΩUI: ℒovely ΩMEGA User Interface
  In: Formal Aspects of Computing 11 (1999), p. 326-342
  ISSN: 0934-5043
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0345829693&origin=inward
• Kohlhase M., Franke A.:
  MBase: Representing mathematical knowledge in a relational data base
  In: Electronic Notes in Theoretical Computer Science 23 (1999), p. 451-468
  ISSN: 1571-0661
  DOI: 10.1016/S1571-0661(05)80615-2
• Kohlhase M., Scheja O.:
  Higher-order multi-valued resolution
  In: Journal of Applied Non-Classical Logics 9 (1999), p. 455-477
  ISSN: 1166-3081
  DOI: 10.1080/11663081.1999.10510980

1998

• Benzmüller C., Kohlhase M.:
  Extensional higher-order resolution
  15th International Conference on Automated Deduction, CADE 1998
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84858341103&origin=inward
• Kerber M., Kohlhase M., Sorge V.:
  Integrating Computer Algebra into Proof Planning
  In: Journal of Automated Reasoning 21 (1998), p. 327-355
  ISSN: 0168-7433
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-0032287894&origin=inward
• Kohlhase M., Benzmüller C.:
  System description: Leo— A higher-order theorem prover
  15th International Conference on Automated Deduction, CADE 1998
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84872799915&origin=inward

1997

• Benzmuller C, Cheikhrouhou L, Fehrer D, Fiedler A, Huang XR, Kerber M, Kohlhase M, Konrad K, Meier A, Melis E, Schaarschmidt W, Siekmann J, Sorge V:
  Omega MEGA: Towards a mathematical assistant
• Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X., Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W., Siekmann J., Sorge V.:
  ΩMEGA: Towards a mathematical assistant
  14th International Conference on Automated Deduction, CADE 1997
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84860987429&origin=inward
• Hutter D., Kohlhase M.:
  A colored version of the λ-calculus
  14th International Conference on Automated Deduction, CADE 1997
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-35048867096&origin=inward
• Kohlhase M., Gardent C.:
  Computing parallelism in discourse
  In: Martha E. Pollack (ed.): Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI) 1997

1996

• Gardent C., Kohlhase M., van Leusen N.:
  Corrections and higher-order unification
• Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
  The proof development environment Ω-MKRP
  In: Informatik - Forschung und Entwicklung 11 (1996), p. 20-26
  ISSN: 0178-3564
  DOI: 10.1007/s004500050036
• Kerber M., Kohlhase M., Sorge V.:
  Integrating computer algebra with proof planning
  4th International Symposium on Design and Implementation of Symbolic Computation Systems, DISCO 1996
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-21444434314&origin=inward

1995

• Kohlhase M.:
  Higher-order tableaux
  4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, TABLEAUX 1995
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84949190517&origin=inward

1994

• Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
  Keim: A toolkit for automated deduction
  12th International Conference on Automated Deduction, CADE-12 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84943317064&origin=inward
• Huang X., Kerber M., Kohlhase M., Melis E., Nesmith D., Richts J., Siekmann J.:
  Ω-MKRP: A proof development environment
  12th International Conference on Automated Deduction, CADE-12 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84961346097&origin=inward
• Huang X., Kerber M., Kohlhase M., Richts J.:
  Adapting methods to novel tasks in proof planning
  18th Annual German Conference on Artificial Intelligence, KI 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-2342658424&origin=inward
• Kerber M., Kohlhase M.:
  A mechanization of strong Kleene logic for partial functions
  12th International Conference on Automated Deduction, CADE-12 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84956993662&origin=inward
• Johann P., Kohlhase M.:
  Unification in an extensional lambda calculus with ordered function sorts and constant overloading
  12th International Conference on Automated Deduction, CADE-12 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-84945308194&origin=inward
• Kohlhase M.:
  Unification in a sorted λ-calculus with term declarations and function sorts
  18th Annual German Conference on Artificial Intelligence, KI 1994
  URL: https://www.scopus.com/record/display.uri?eid=2-s2.0-85028712606&origin=inward

1993

• Kohlhase M., Pfenning F.:
  UNIFICATION IN A LAMBDA-CALCULUS WITH INTERSECTION TYPES
  In: Proceedings of the International Logic Programming Symposion ILPS'93 1993

1992

• Kohlhase M.:
  Unification in order-sorted type theory
  International Conference on Logic Programming and Automated Reasoning, LPAR 1992
  DOI: 10.1007/BFb0013080