KWARC Group: Selected Publications

This website represents the joint bibliography of the KWARC group and is generated automatically.
For more details, please see the Github Repository.
Please respect any copyrights when downloading
  1. Archival Literature
    1. Articles in Journals
    2. Articles in Collections
    3. Papers at International, Peer-Reviewed Conferences
    4. Monographs
    5. Conference Proceedings Edited
  2. Theses
  3. Gray Literature
    1. Worskhop Proceedings Edited
    2. Papers at Peer-Reviewed Workshops
    3. Technical Reports
  4. Unpublished
  5. Miscellaneous

Archival Literature

Articles in Journals

  1. [31] M. Kohlhase, M. Berges, J. Grubert, A. Henrich, D. Landes, J. L. Leidner, F. Mittag, D. Nicklas, U. Schmid, Y. Sedlmaier, A. U. Ende, and D. Wolter (2023) Project VoLL-KI – learning from learners. Künstliche Intellienz. Note: accepted Cited by: p1.
  2. [51] D. Müller (2023) An html/css schema for primitives – generating high-quality responsive html from generic . TeX users group conference (tug), pp. 275–286. External Links: Link Cited by: p1.
  3. [50] D. Müller and M. Kohlhase (2022) sTeX3 – a -based ecosystem for semantic/active mathematical documents. TeX users group conference (tug), pp. 197–201. External Links: Link Cited by: p1.
  4. [11] J. Carette, W. M. Farmer, M. Kohlhase, and F. Rabe (2021) Big math and the one-brain barrier – the tetrapod model of mathematical knowledge. Mathematical Intelligencer 43 (1). External Links: Document Cited by: p1.
  5. [39] M. Kohlhase and F. Rabe (2021) Experiences from exporting major proof assistant libraries. Journal of Automated Reasoning 65 (8), pp. 1265–1298. External Links: Document Cited by: p1.
  6. [8] K. Berčič and J. Vidali (2020/02/14) DiscreteZOO: a fingerprint database of discrete objects. Mathematics in Computer Science. External Links: Document, Link, ISSN 1661-8289 Cited by: p1.
  7. [6] K. Berčič, M. Kohlhase, and F. Rabe (2020) (Deep) fair mathematics. it – Information Technology 62 (1), pp. 7–17. External Links: Document, Link Cited by: p1.
  8. [45] T. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, and F. Rabe (2018) Model pathway diagrams for the representation of mathematical models. Journal of Optical and Quantum Electronics 50 (2), pp. 70. External Links: Document Cited by: p1.
  9. [12] G. Dowek, C. Dubois, B. Pientka, and F. Rabe (2017) Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports by Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik 6 (10), pp. 75–98. Note: see http://drops.dagstuhl.de/opus/volltexte/2017/6951/ Cited by: p1.
  10. [61] F. Rabe (2017) How to Identify, Translate, and Combine Logics?. Journal of Logic and Computation 27 (6), pp. 1753–1798. Cited by: p1.
  11. [62] F. Rabe (2017) Morphism Axioms. Theoretical Computer Science 691, pp. 55–80. Cited by: p1.
  12. [7] K. Berčič and P. Potočnik (2016) Two-arc-transitive two-valent digraphs of certain orders. Ars Mathematica Contemporanea 11 (1), pp. 127–146. External Links: Document Cited by: p1.
  13. [38] M. Kohlhase and F. Rabe (2016) QED reloaded: towards a pluralistic formal library of mathematical knowledge. Journal of Formalized Reasoning 9 (1), pp. 201–234. External Links: Link Cited by: p1.
  14. [2] E. Bender, P. Hubwieser, N. Schaper, M. Margaritis, M. Berges, L. Ohrndorf, J. Magenheim, and S. Schubert (2015) Towards a competency model for teaching computer science. Peabody Journal of Education 90 (4), pp. 519–532. External Links: ISSN 0161-956X, Document Cited by: p1.
  15. [59] F. Rabe (2015) Lax Theory Morphisms. ACM Transactions on Computational Logic 17 (1). Cited by: p1.
  16. [60] F. Rabe (2015) The Future of Logic: Foundation-Independence. Logica Universalis 10 (1), pp. 1–20. Note: Winner of the Contest “The Future of Logic” at the World Congress on Universal Logic External Links: Document, Link Cited by: p1.
  17. [44] M. Kohlhase (2014-06) Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. EMS Newsletter, pp. 22–27. External Links: Link Cited by: p1.
  18. [34] M. Kohlhase and M. Iancu (2014) Co-representing structure and meaning of mathematical documents. Sprache und Datenverarbeitung, International Journal for Language Data Processing 38 (2), pp. 49–80. Note: Special Issue “The language of mathematics – computational, linguistic and logical aspects” External Links: Link Cited by: p1.
  19. [36] M. Kohlhase, H. Mihaljevic-Brandt, W. Sperber, and O. Teschke (2013-09) Zentralblatt column: mathematical formula search. EMS Newsletter, pp. 56–57. External Links: Link Cited by: p1.
  20. [21] M. Iancu, M. Kohlhase, F. Rabe, and J. Urban (2013) The Mizar Mathematical Library in OMDoc: translation and applications. Journal of Automated Reasoning 50 (2), pp. 191–202. External Links: Link, Document Cited by: p1.
  21. [28] A. Kohlhase and M. Kohlhase (2013) Spreadsheets with a semantic layer. Electronic Communications of the EASST: Specification, Transformation, Navigation – Special Issue dedicated to Bernd Krieg-Brückner on the Occasion of his 60th Birthday 62, pp. 1–20. External Links: Link Cited by: p1.
  22. [48] C. Lange (2013) Ontologies and languages for representing mathematical knowledge on the semantic web. Semantic Web Journal 4 (2), pp. 119–158. External Links: Document, Link Cited by: p1.
  23. [53] F. Rabe and M. Kohlhase (2013) A scalable module system. Information & Computation 0 (230), pp. 1–54. External Links: Link Cited by: p1.
  24. [55] F. Rabe and K. Sojakova (2013) Logical Relations for a Logical Framework. ACM Transactions on Computational Logic. External Links: Link Cited by: p1.
  25. [58] F. Rabe (2013) A Logical Framework Combining Model and Proof Theory. Mathematical Structures in Computer Science 23 (5), pp. 945–1001. Cited by: p1.
  26. [5] K. Berčič and M. Ghasemi (2012) Tetravalent arc-transitive graphs of order twice a product of two primes. Discrete Mathematics 312 (24), pp. 3643–3648. External Links: Document Cited by: p1.
  27. [26] M. Kerber and M. Kohlhase (2012) Reasoning without believing: on the mechanization of presuppositions and partiality. Journal of Applied Non-Classical Logics 22 (4), pp. 295–317. External Links: Document Cited by: p1.
  28. [37] M. Kohlhase and F. Rabe (2012) Semantics of OpenMath and MathML3. Mathematics in Computer Science 6 (3), pp. 235–260. External Links: Link Cited by: p1.
  29. [46] C. Lange (2012) Desktop mit dolmetscher. freeX Magazin für Netzwerk/Virtualisierung/Sicherheit 2, pp. 90–94. Cited by: p1.
  30. [47] C. Lange (2012) Vokabelheft fürs web. freeX Magazin für Netzwerk/Virtualisierung/Sicherheit 1, pp. 42–45. External Links: Link Cited by: p1.
  31. [57] F. Rabe (2012) A logical framework combining model and proof theory. Mathematical Structures in Computer Science. External Links: Link Cited by: p1.
  32. [1] S. Awodey and F. Rabe (2011) Kripke Semantics for Martin-Löf’s Extensional Type Theory. Logical Methods in Computer Science 7 (3). Cited by: p1.
  33. [18] F. Horozal and F. Rabe (2011) Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science 412 (37), pp. 4919–4945. Cited by: p1.
  34. [22] M. Iancu and F. Rabe (2011) Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science 21 (4), pp. 883–911. External Links: Document, Link Cited by: p1.
  35. [32] M. Kohlhase, J. Corneli, C. David, D. Ginev, C. Jucovschi, A. Kohlhase, C. Lange, B. Matican, S. Mirea, and V. Zholudev (2011) The planetary system: web 3.0 & active documents for STEM. Procedia Computer Science 4, pp. 598–607. Note: Finalist at the Executable Paper Grand Challenge External Links: Link, Document Cited by: p1.
  36. [56] F. Rabe (2010) Review of “Reasoning in Simple Type Theory – Festschrift in Honor of Peter B. Andrews on his 70th Birthday”. Bulletin of Symbolic Logic 16 (3), pp. 409–411. Cited by: p1.
  37. [65] H. Stamerjohanns, D. Ginev, C. David, D. Misev, V. Zamdzhiev, and M. Kohlhase (2010) Conversion d’articles en vers XML avec MathML : une étude comparative. Cahiers GUTenberg 51, pp. 7–28. External Links: Link Cited by: p1.
  38. [66] H. Stamerjohanns, M. Kohlhase, D. Ginev, C. David, and B. Miller (2010) Transforming large collections of scientific publications to XML. Mathematics in Computer Science 3 (3), pp. 299–307. External Links: Link Cited by: p1.
  39. [67] H. M. Tran, C. Lange, G. Chulkov, J. Schönwälder, and M. Kohlhase (2009-05) Applying semantic techniques to search and analyze bug tracking data. Journal of Network and Systems Management 17 (3), pp. 285–308. External Links: Document Cited by: p1.
  40. [4] C. E. Benzmüller, C. E. Brown, and M. Kohlhase (2009) Cut-simulation and impredicativity. Logical Methods in Computer Science 5 (1), pp. 1–21. External Links: Link Cited by: p1.
  41. [49] C. Müller and M. Kohlhase (2009) Context-Aware Adaptation: A Case Study on Mathematical Notations. Information Systems Management 26 (3), pp. 215–230. External Links: ISSN 1934-8703 Cited by: p1.
  42. [27] A. Kohlhase and M. Kohlhase (2008-06) Semantic knowledge management for education. Proceedings of the IEEE; Special Issue on Educational Technology 96 (6), pp. 970–989. External Links: Link Cited by: p1.
  43. [17] J. Goguen, T. Mossakowski, V. de Paiva, F. Rabe, and L. Schröder (2008) An Institutional View on Categorical Logic. International Journal of Software and Informatics 1 (1), pp. 129–152. Cited by: p1.
  44. [29] A. Kohlhase and M. Reichel (2008) Embodied conceptualizations: social tagging and e-learning. International Journal of Web-Based Learning and Teaching Technologies (1), pp. 58–67. Cited by: p1.
  45. [43] M. Kohlhase (2008) Using as a semantic markup format. Mathematics in Computer Science 2 (2), pp. 279–304. External Links: Link Cited by: p1.
  46. [30] A. Kohlhase (2007) Learner and learning technology: the interaction process as a full partnership. ECTI Transactions Journal. External Links: Link Cited by: p1.
  47. [52] N. Müller (2007) Tagungsbericht – LWA 2006. KI – Zeitschrift Künstliche Intelligenz 1, pp. 61. Note: http://www.kuenstliche-intelligenz.de/index.php?id=7754 External Links: Link Cited by: p1.
  48. [54] F. Rabe, P. Pudlák, G. Sutcliffe, and W. Shen (2007) Solving the $100 Modal Logic Challenge. Journal of Applied Logic 1 (1). Cited by: p1.
  49. [3] C. Benzmüller, C. Brown, and M. Kohlhase (2004) Higher order semantics and extensionality. Journal of Symbolic Logic 69, pp. 1027–1088. External Links: Link Cited by: p1.
  50. [9] P. Blackburn and M. Kohlhase (2004) Inference and computational semantics. Journal of Logic, Language and Information 13 (2), pp. 117–120. External Links: Link Cited by: p1.
  51. [23] S. Jeschke, M. Kohlhase, and R. Seiler (2004) eLearning-, eTeaching- & eResearch-technologien – Chancen und Potentiale für die Mathematik. Mitteilungen der DMV 12 (2). External Links: Link Cited by: p1.
  52. [10] J. Bos and M. Kohlhase (2003) Editorial. Logic Journal of the IGPL 11 (4), pp. 381–384. Cited by: p1.
  53. [35] M. Kohlhase and A. Koller (2003) Resource-adaptive model generation as a performance model. Logic Journal of the IGPL 11 (4), pp. 435–456. External Links: Link Cited by: p1.
  54. [33] M. Kohlhase and A. Franke (2001) MBase: representing knowledge and context for the integration of mathematical software systems. Journal of Symbolic Computation; Special Issue on the Integration of Computer Algebra and Deduction Systems 32 (4), pp. 365–402. External Links: Document, Link Cited by: p1.
  55. [20] D. Hutter and M. Kohlhase (2000) Managing structural information by higher-order colored unification. Journal of Automated Reasoning 25 (2), pp. 123–164. External Links: Link Cited by: p1.
  56. [42] M. Kohlhase (2000) OMDoc: an infrastructure for OpenMath content dictionary information. Bulletin of the ACM Special Interest Group on Symbolic and Automated Mathematics (SIGSAM) 34 (2), pp. 43–48. External Links: Link Cited by: p1.
  57. [14] A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase, and V. Sorge (1999) Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science 5, pp. 156–187. External Links: Link Cited by: p1.
  58. [15] A. Franke and M. Kohlhase (1999) MBase: representing mathematical knowledge in a relational data base. Electronic Notes Theoretical Computer Science 23 (3). Cited by: p1.
  59. [16] C. Gardent, M. Kohlhase, and K. Konrad (1999) Higher-order colored unification: a linguistic application. Téchniqe et Sciences Informatiques, special issue for JFPLC-UNIF’97 18 (2), pp. 1–28. External Links: Link Cited by: p1.
  60. [40] M. Kohlhase and O. Scheja (1999) Higher-order multi-valued resolution. Journal of Applied Non-Classical Logics 9. External Links: Link Cited by: p1.
  61. [63] J. Siekmann, S. M. Hess, C. Benzmüller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, M. Pollet, and V. Sorge (1999) LΩUI: lovely Ωmega user interface. Formal Aspects of Computing 3 (11), pp. 326–342. External Links: Link Cited by: p1.
  62. [13] M. Egg, C. Gardent, and M. Kohlhase (1998) Steuerung der Inferenz in der Diskursverarbeitung. Kognitionswissenschaft 7 (3), pp. 106–110. External Links: Link Cited by: p1.
  63. [24] M. Kerber, M. Kohlhase, and V. Sorge (1998) Integrating computer algebra into proof planning. Journal of Automated Reasoning 21 (3), pp. 327–355. External Links: Link Cited by: p1.
  64. [64] J. Siekmann, M. Kohlhase, and E. Melis (1998) Ωmega, ein mathematisches Assistenzsystem. Kognitionswissenschaft 7 (3), pp. 101–105. External Links: Link Cited by: p1.
  65. [19] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann (1996) Die Beweisentwicklungsumgebung Ωmega. Informatik – Forschung und Entwicklung 11, pp. 20–26. Cited by: p1.
  66. [25] M. Kerber and M. Kohlhase (1996) A tableau calculus for partial functions. Collegium Logicum: Annals of the Kurt-Gödel-Society 2, pp. 21–49. External Links: Link Cited by: p1.
  67. [41] M. Kohlhase (1996) Sorten für das automatische Beweisen höherer Stufe. Künstliche Intelligenz. Cited by: p1.

Articles in Collections

  1. [22] M. Kohlhase (2022) Wann ist ein juristischer text strukturiert? die sicht der informatik und der künstlichen intelligenz. In Digitalisierung von zivilprozess und rechtsdurchsetzung, A. Adrian, S. Evert, M. K. Kohlhase, and M. Zwickel (Eds.), Schriften zum Prozessrecht, pp. 155–170. External Links: Link Cited by: p1.
  2. [2] A. Aizawa and M. Kohlhase (2020) Mathematical information retrieval. In Evaluating information retrieval and access tasks – NTCIR’s legacy of research impactEvaluating Information Retrieval and Access Tasks – NTCIR’s Legacy of Research Impact, T. Sakai, D. W. Oard, and N. Kando (Eds.), pp. 169–185. Cited by: p1.
  3. [4] E. Belyaeva, J. Berčič, K. Berčič, F. Fuart, A. Košmerlj, A. Muhič, A. Rehar, J. Rupnik, and M. Trampuš (2015) 3XL news: a cross-lingual news aggregator and reader. In The Semantic Web: ESWC 2015 Satellite Events, Lecture Notes in Computer Science, Vol. 9341, pp. 3–8. External Links: ISBN 978-3-319-25638-2, Document Cited by: p1.
  4. [25] C. Lange and M. Kohlhase (2013) Mashups using mathematical knowledge. In Semantic mashups, B. Endres-Niggemeyer and B. Endres-Niggemeyer (Eds.), pp. 171–204. External Links: Link Cited by: p1.
  5. [10] A. Kohlhase and M. Reichel (2010-01) Social tagging and learning: the fuzzy line between private and public space. In Novel Developments in Web-Based Learning Technologies: Tools for Modern Teaching, N. Karacapilidis (Ed.), Advances in Web-based Learning (AWBL). External Links: ISBN 978-1-60566-938-0 Cited by: p1.
  6. [8] A. Kohlhase and M. Kohlhase (2009) Compensating the computational bias of spreadsheets. In Festschrift in honour of Bernd Krieg-Brückner’s 60th birthdayFestschrift in Honour of Bernd Krieg-Brückner’s 60th Birthday, B. Hoffmann, B. Gersdorf, C. Lüth, T. Mossakowski, T. Röfer, L. Schröder, S. Hui, and M. Werner (Eds.), pp. 184–200. Cited by: p1.
  7. [11] M. Kohlhase, J. Lemburg, L. Schröder, and E. Schulz (2009) Formal management of CAD/CAM processes. In Festschrift in honour of Bernd Krieg-Brückner’s 60th birthdayFestschrift in Honour of Bernd Krieg-Brückner’s 60th Birthday, B. Hoffmann, B. Gersdorf, C. Lüth, T. Mossakowski, T. Röfer, L. Schröder, S. Hui, and M. Werner (Eds.), pp. 201–216. Cited by: p1.
  8. [9] A. Kohlhase and N. Müller (2008-04) Added-Value: Getting People into Semantic Work Environments. In Emerging technologies for semantic work environments: techniques, methods, and applicationsEmerging Technologies for Semantic Work Environments: Techniques, Methods, and Applications, J. Rech, B. Decker, and E. Ras (Eds.), pp. 185–205. Cited by: p1.
  9. [24] C. Lange and M. Kohlhase (2008-04) SWiM: a semantic wiki for mathematical knowledge management. In Emerging technologies for semantic work environments: techniques, methods, and applications, J. Rech, B. Decker, E. Ras, J. Rech, B. Decker, and E. Ras (Eds.), pp. 47–68. External Links: Link Cited by: p1.
  10. [5] C. Benzmüller, C. Brown, and M. Kohlhase (2008) Cut elimination with xi-functionality. In Festschrift in honour of Peter B. Andrews on his 70th birthday, C. Benzmüller, C. Brown, J. Siekmann, and R. Statman (Eds.), External Links: Link Cited by: p1.
  11. [21] M. Kohlhase (2008) Wissensrepräsentation für computerunterstützte Lehre. In Selbstorganisiertes Lernen im InternetSelbstorganisiertes Lernen im Internet, V. Hornung-Prähauser, M. Luckmann, and M. Kalz (Eds.), pp. 248–251. Cited by: p1.
  12. [3] G. Bancerek and M. Kohlhase (2007) Towards a Mizar Mathematical Library in OMDoc format. In From insight to proof: festschrift in honour of Andrzej TrybulecFrom Insight to Proof: Festschrift in Honour of Andrzej Trybulec, R. Matuszewski and A. Zalewska (Eds.), Studies in Logic, Grammar and Rhetoric, Vol. 10:23, pp. 265–275. External Links: Link Cited by: p1.
  13. [7] A. Franke and M. Kohlhase (2006-08) MBase, an open mathematical knowledge base. In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI. Cited by: p1.
  14. [17] M. Kohlhase (2006-08) Formal Proofs as Mathematical Objects. In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI, pp. 177–179. Cited by: p1.
  15. [18] M. Kohlhase (2006-08) Representing Proofs (Module PF). In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI, pp. 167–179. Cited by: p1.
  16. [19] M. Kohlhase (2006-08) Standardizing context in system interoperability. In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI. Cited by: p1.
  17. [20] M. Kohlhase (2006-08) S: a -based workflow for OMDoc. In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI. Cited by: p1.
  18. [23] C. Lange and M. Kohlhase (2006-08) SWiM – an OMDoc-based semantic wiki. In OMDoc – an open markup format for mathematical documents [version 1.2], LNAI. Cited by: p1.
  19. [26] N. Müller (2006-08) OMDoc as a Data Format for VeriFun. In OMDoc – an open markup format for mathematical documents [version 1.2]OMDoc – An open markup format for mathematical documents [Version 1.2], LNAI, pp. 329–332. Cited by: p1.
  20. [16] M. Kohlhase (2003) Artificial intelligence: automated reasoning. In Van Nostrand’s Scientific Encyclopedia, pp. 247–250. Cited by: p1.
  21. [6] P. Blackburn, J. Bos, M. Kohlhase, and H. de Nivelle (2001) Inference and computational semantics. In Computing meaning (volume 2)Computing Meaning (Volume 2), H. Bunt, L. Kievit, R. Muskens, and M. Verlinden (Eds.), pp. 11–28. Cited by: p1.
  22. [12] M. Kohlhase, E. Melis, and J. Siekmann (1999) ΩMEGA – a mathematical assistant. In Liber Amicorum for the Fiftieth Birthday of Johan van Benthem, J. Gerbrandy, M. Marx, M. de Rijke, and Y. Venema (Eds.), pp. 248–251. External Links: Link Cited by: p1.
  23. [1] (1998) M. Kohlhase, W. Bibel, and P. Schmitt (Eds.), Cited by: p1.
  24. [14] M. Kohlhase (1998) Automated theorem proving in mathematics. In Automated Deduction – A Basis for Applications, W. Bibel and P. Schmitt (Eds.), Vol. 3, pp. 3–7. Cited by: p1.
  25. [15] M. Kohlhase (1998) Higher-order automated theorem proving. In Automated Deduction – A Basis for Applications, W. Bibel and P. Schmitt (Eds.), Vol. 2, pp. 431–462. External Links: Link Cited by: p1.
  26. [13] M. Kohlhase (1992) Beweissysteme mit Logiken höherer Stufe. In Deduktionssysteme, Automatisierung des Logischen Denkens, K. H. Bläsius and H. Bürckert (Eds.), pp. 213–238. Cited by: p1.

Papers at International, Peer-Reviewed Conferences

  1. [14] M. Berges, J. Betzendahl, A. Chugh, M. Kohlhase, D. Lohr, and D. Müller (2023) Learning support systems based on mathematical knowledge managment. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2023, C. Dubois and M. Kerber (Eds.), LNAI. External Links: Link Cited by: p1.
  2. [142] T. Kruse, M. Berges, J. Betzendahl, M. Kohlhase, D. Lohr, and D. Müller (2023) Learning with alea: tailored experiences through annotated course material. In KI-bildung, Lecture Notes in Informatics. External Links: Link Cited by: p1.
  3. [155] D. Lohr, M. Berges, M. Kohlhase, D. Müller, and M. Rapp (2023) The Y-Model – formalization of computer-science tasks in the context of adaptive learning systems. In 2023 IEEE German Education Conference (GeCon), External Links: Link Cited by: p1.
  4. [156] D. Lohr, M. Berges, M. Kohlhase, and F. Rabe (2023) The potential of answer classes in large-scale written computer-science exams. In Proceedings of the 10th Symposium on Computer Science in Higher Education HDI23, Aachen, Germany, pp. . Note: Accepted External Links: Link Cited by: p1.
  5. [183] J. F. Schaefer and M. Kohlhase (2023) Towards an annotation standard for stem documents – datasets, benchmarks, and spotters. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2023, C. Dubois and M. Kerber (Eds.), LNAI. Cited by: p1.
  6. [50] M. Herchenbach, D. Müller, S. Scheele, and U. Schmid (2022) Explaining image classifications with near misses, near hits and prototypes: supporting domain experts in understanding decision boundaries. In Pattern Recognition and Artificial Intelligence: Third International Conference, ICPRAI 2022, External Links: Document, Link Cited by: p1.
  7. [122] M. Kohlhase and D. Müller (2022) System description: sTeX3 – a -based ecosystem for semantic/active mathematical documents. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2022, K. Buzzard and T. Kutsia (Eds.), LNAI, Vol. 13467, pp. 184–188. External Links: Link Cited by: p1.
  8. [167] D. Müller and M. Kohlhase (2022) Injecting formal mathematics into latex. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2022, K. Buzzard and T. Kutsia (Eds.), LNAI, Vol. 13467, pp. 168–183. External Links: Link Cited by: p1.
  9. [168] D. Müller, M. März, S. Scheele, and U. Schmid (2022) An interactive explanatory ai system for industrial quality control. In IAAI 2022, External Links: Document, Link Cited by: p1.
  10. [13] K. Berčič, M. Kohlhase, and F. Rabe (2020) Towards a heterogeneous query language for mathematical knowledge. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 39–54. External Links: Link Cited by: p1.
  11. [111] M. Kohlhase, B. Bösl, R. Marcus, D. Müller, D. Rochau, N. Roux, J. Schihada, and M. Stamminger (2020) FrameIT: detangling knowledge management from game design in serious games. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 173–189. External Links: Document, Link Cited by: p1.
  12. [125] M. Kohlhase, F. Rabe, C. S. Coen, and J. F. Schaefer (2020) Logic-independent proof search in logical frameworks (short paper). In 10th international joint conference on automated reasoning (IJCAR 2020)10th International Joint Conference on Automated Reasoning (IJCAR 2020), N. Peltier and V. Sofronie-Stokkermans (Eds.), pp. 395–401. Cited by: p1.
  13. [158] R. Marcus, M. Kohlhase, and F. Rabe (2020) TGView3D: a system for 3-dimensional visualization of theory graphs. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 290–296. External Links: Link Cited by: p1.
  14. [170] D. Müller, F. Rabe, C. Rothgang, and M. Kohlhase (2020) Representing structural language features in formal meta-languages. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 206–221. External Links: Link Cited by: p1.
  15. [181] J. F. Schaefer, K. Amann, and M. Kohlhase (2020) Prototyping controlled mathematical languages in jupyter notebooks. In Mathematical software – icms 2020. 7th international conferenceMathematical Software – ICMS 2020. 7th international conference, A. M. Bigatti, J. Carette, J. H. Davenport, M. Joswig, and T. de Wolff (Eds.), LNCS, Vol. 12097, pp. 406–415. External Links: Link Cited by: p1.
  16. [2] K. Amann, M. Kohlhase, F. Rabe, and T. Wiesing (2019) Integrating semantic mathematical documents and dynamic notebooks. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI, pp. 275–290. External Links: Link Cited by: p1.
  17. [12] K. Berčič, M. Kohlhase, and F. Rabe (2019) Towards a unified mathematical data infrastructure: database and interface generation. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI, pp. 28–43. External Links: Link Cited by: p1.
  18. [30] A. Condoluci, M. Kohlhase, D. Müller, F. Rabe, C. Sacerdoti Coen, and M. Wenzel (2019) Relational data across mathematical libraries. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI, pp. 61–76. External Links: Link Cited by: p1.
  19. [171] D. Müller, F. Rabe, and C. Sacerdoti Coen (2019) The Coq Library as a Theory Graph. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI. Cited by: p1.
  20. [175] F. Rabe and Y. Sharoda (2019) Diagram combinators in MMT. In Intelligent computer mathematicsIntelligent Computer Mathematics, C. Kaliszyck, E. Brady, A. Kohlhase, C. Sacerdoti Coen, C. Kaliszyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI, Cham, pp. 211–226. External Links: ISBN 978-3-030-23250-4, Link Cited by: p1.
  21. [19] J. Betzendahl and M. Kohlhase (2018) Translating the IMPS theory library to OMDoc/MMT. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  22. [83] A. Kohlhase, M. Kohlhase, and T. Ouypornkochagorn (2018) Discourse phenomena in math documents. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  23. [166] D. Müller, M. Kohlhase, and F. Rabe (2018) Automatically finding theory morphisms for knowledge management. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  24. [169] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  25. [174] T. Pollinger, M. Kohlhase, and H. Köstler (2018) Knowledge amalgamation for computational science and engineering. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  26. [182] J. F. Schaefer and M. Kohlhase (2018) Syntactic/semantic analysis for high-precision math linguistics. In Workshop papers at 11th conference on intelligent computer mathematics cicm 2018Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018, O. Hasan, A. Youssef, A. Naumowicz, W. Farmer, C. Kaliszyk, D. Gallois-Wong, F. Rabe, G. D. Reis, G. Passmore, J. Davenport, M. Pfeiffer, M. Kohlhase, S. Autexier, S. Tahar, T. Koprucki, U. Siddique, W. Neuper, W. Windsteiger, W. Schreiner, W. Sperber, and Z. Kovács (Eds.), Note: CICM Work in Progress Paper External Links: Link Cited by: p1.
  27. [62] P. Hubwieser, M. Berges, M. Striewe, and M. Goedicke (2017) Towards competency based testing and feedback: competency definition and measurement in the field of algorithms & data structures. In Proceedings of 2017 IEEE Global Engineering Education Conference (EDUCON), IEEE Conference Publications, pp. 517–526. External Links: ISBN 978-1-5090-5467-1, Document Cited by: p1.
  28. [79] A. Kohlhase, M. Kohlhase, and M. Fürsich (2017) Visual structure in math expressions. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  29. [114] M. Kohlhase, T. Koprucki, D. Müller, and K. Tabelow (2017) Mathematical models as research data via flexiformal theory graphs. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  30. [120] M. Kohlhase, D. Müller, S. Owre, and F. Rabe (2017) Making PVS accessible to generic services by interpretation in a universal format. In Interactive theorem proving 8th international conference, itp 2017Interactive Theorem Proving, M. Ayala-Rincón and C. A. Muñoz (Eds.), LNCS, Vol. 10499. External Links: Link Cited by: p1.
  31. [121] M. Kohlhase, D. Müller, M. Pfeiffer, F. Rabe, N. Thiéry, V. Vasilyev, and T. Wiesing (2017) Knowledge-based interoperability for mathematical software systems. In MACIS 2017MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences, J. Blömer, T. Kutsia, and D. Simos (Eds.), LNCS, pp. 195–210. External Links: Link Cited by: p1.
  32. [165] D. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, and F. Rabe (2017) Classification of alignments between concepts of formal mathematical systems. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  33. [184] P. Shah, M. Berges, and P. Hubwieser (2017) Qualitative content analysis of programming errors. In Proceedings of the 5th International Conference on Information and Education Technology, International Conference Proceedings Series, New York. External Links: ISBN 978-1-4503-4791-4, Document Cited by: p1.
  34. [187] W. Sperber and M. Kohlhase (2017) Software citations, information systems, and beyond. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  35. [190] T. Wiesing, M. Kohlhase, and F. Rabe (2017) Virtual theories – a uniform interface to mathematical knowledge bases. In MACIS 2017MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences, J. Blömer, T. Kutsia, and D. Simos (Eds.), LNCS, pp. 243–257. External Links: Link Cited by: p1.
  36. [17] M. Berges, M. Striewe, P. Shah, M. Goedicke, and P. Hubwieser (2016) Towards deriving programming competencies from student errors. In 4th International Conference on Learning and Teaching in Computing and Engineering (LaTiCE), Los Alamitos, pp. 19–23. Cited by: p1.
  37. [35] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Interoperability in the OpenDreamKit project: the math-in-the-middle approach. In Intelligent computer mathematicsIntelligent Computer Mathematics 2016, M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa (Eds.), LNAI. External Links: Link Cited by: p1.
  38. [45] D. Ginev, M. Iancu, C. Jucovshi, A. Kohlhase, M. Kohlhase, A. Oripov, J. Schefter, W. Sperber, O. Teschke, and T. Wiesing (2016) The SMGloM project and system. towards a terminology and ontology for mathematics. In Mathematical software - ICMS 2016 - 5th international congressMathematical Software - ICMS 2016 - 5th International Congress, G. Greuel, T. Koch, P. Paule, and A. Sommese (Eds.), LNCS, Vol. 9725. External Links: Link Cited by: p1.
  39. [49] R. Hambasan and M. Kohlhase (2016) Faceted search for mathematics. In MACIS 2015MACIS 2015: Sixth International Conference on Mathematical Aspects of Computer and Information Sciences, I. S. Kotsireas, S. M. Rump, and C. K. Yap (Eds.), LNCS. External Links: Link Cited by: p1.
  40. [154] G. Lisowski, D. McHugh, and M. Rapp (2016) Winning questions: inquisitive semantics and the lottery paradox. In 5th LSE Graduate Conference in Philosophy of Probability, External Links: Link Cited by: p1.
  41. [157] E. Luzhnica and M. Kohlhase (2016) Formula semantification and automated relation finding in the OEIS. In Mathematical software - ICMS 2016 - 5th international congressMathematical Software - ICMS 2016 - 5th International Congress, G. Greuel, T. Koch, P. Paule, and A. Sommese (Eds.), LNCS, Vol. 9725. External Links: Link Cited by: p1.
  42. [16] M. Berges and P. Hubwieser (2015) Evaluation of source code with item response theory. In Proceedings of the 20th SIGCSE Conference on Innovation and Technology in Computer Science Education, New York, pp. 51–56. Cited by: p1.
  43. [18] M. Berges (2015) Investigating novice programming abilities with the help of psychometric assessment. In Proceedings of Society for Information Technology & Teacher Education International Conference 2015, D. Slykhuis and G. Marks (Eds.), Las Vegas, NV, United States, pp. 90–95. Cited by: p1.
  44. [67] M. Iancu and M. Kohlhase (2015) A flexiformal model of knowledge dissemination and aggregation in mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2015, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), LNCS, pp. 137–152. External Links: Link Cited by: p1.
  45. [68] M. Iancu and M. Kohlhase (2015) Math literate knowledge management via induced material. In Intelligent computer mathematicsIntelligent Computer Mathematics 2015, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), LNCS, pp. 187–202. External Links: Link Cited by: p1.
  46. [128] M. Kohlhase and W. Sperber (2015) The SMGloM project or why we need a semantic glossary of mathematics. In European Conference on Data Analysis ECDA2015; Data Science: Foundations, Methods and Applications, External Links: Link Cited by: p1.
  47. [159] M. Margaritis, J. Magenheim, P. Hubwieser, M. Berges, L. Ohrndorf, and S. Schubert (2015) Development of a competency model for computer science teachers at secondary school level. In IEEE Global Engineering Education Conference, Los Alamitos, pp. 211–220. External Links: Document Cited by: p1.
  48. [180] A. Ruf, M. Berges, and P. Hubwieser (2015) Classification of programming tasks according to required skills and knowledge representation. In Informatics in Schools. Curricula, Competences, and Competitions, A. Brodnik and J. Vahrenhold (Eds.), Lecture Notes in Computer Science, Heidelberg, pp. 57–68. External Links: ISBN 978-3-319-25395-4 Cited by: p1.
  49. [21] T. Breitsprecher, M. Codescu, C. Jucovschi, M. Kohlhase, L. Schröder, and S. Wartzack (2014) Towards ontological support for principle solutions in mechanical engineering. In Formal ontology in information systems - proceedings of the eighth international conference, FOIS 2014Formal Ontology in Information Systems - Proceedings of the Eighth International Conference, FOIS 2014, P. Garbacz and O. Kutz (Eds.), Frontiers in Artificial Intelligence and Applications, Vol. 267, pp. 427–432. External Links: Document Cited by: p1.
  50. [23] M. B. Caminati, M. Kerber, C. Lange, and C. Rowat (2014) Set theory or higher order logic to represent auction concepts in Isabelle?. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 236–251. External Links: 1406.0774 Cited by: p1.
  51. [24] J. Carette, W. Farmer, and M. Kohlhase (2014) Realms: a structure for consolidating knowledge about mathematical theories. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 252–266. Note: MKM Best-Paper-Award External Links: Link Cited by: p1.
  52. [44] D. Ginev and J. Corneli (2014) NNexus reloaded. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 423–426. External Links: Link Cited by: p1.
  53. [46] D. Ginev, B. Miller, and S. Oprea (2014) E-books and graphics with ml. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 427–430. External Links: Link Cited by: p1.
  54. [57] F. Horozal, M. Kohlhase, and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  55. [65] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  56. [66] M. Iancu, M. Kohlhase, and C. Prodescu (2014) Representing, archiving, and searching the space of mathematical knowledge. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 26–30. External Links: Document, Link Cited by: p1.
  57. [73] C. Jucovschi (2014) Towards an interaction-based integration of MKM services into end-user applications. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 344–356. External Links: Link Cited by: p1.
  58. [74] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 357–372. External Links: Link Cited by: p1.
  59. [107] A. Kohlhase (2014) Math web search interfaces and the generation gap of mathematicians. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 586–593. External Links: Document Cited by: p1.
  60. [108] A. Kohlhase (2014) Search interfaces for mathematicians. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 153–168. External Links: Link Cited by: p1.
  61. [109] L. Kohlhase and M. Kohlhase (2014) System description: a semantics-aware -to-office converter. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 440–443. External Links: Link Cited by: p1.
  62. [112] M. Kohlhase and M. Iancu (2014) Discourse-level parallel markup and meaning adoption in flexiformal theory graphs. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 36–40. External Links: Document Cited by: p1.
  63. [141] M. Kohlhase (2014) A data model and encoding for a semantic, multilingual terminology of mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 169–183. External Links: Link Cited by: p1.
  64. [15] M. Berges and P. Hubwieser (2013) Concept specification maps: displaying content structures. In Proceedings of the 18th ACM conference on Innovation and technology in computer science education, New York, USA, pp. 291–296. External Links: ISBN 978-1-4503-2078-8, Document Cited by: p1.
  65. [47] D. Ginev and B. Miller (2013) ml 2012 - a year of ml. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 335–338. Cited by: p1.
  66. [61] P. Hubwieser, M. Berges, J. Magenheim, N. Schaper, K. Bröker, M. Margaritis, S. Schubert, and L. Ohrndorf (2013) Pedagogical content knowledge for computer science in german teacher education curricula. In Proceedings of the 8th Workshop in Primary and Secondary Computing Education, New York, pp. 95–103. External Links: Link, ISBN 978-1-4503-2455-7, Document Cited by: p1.
  67. [80] A. Kohlhase, M. Kohlhase, C. Jucovschi, and A. Toader (2013) Full semantic transparency: overcoming boundaries of applications. In Human-computer interaction – interact 2013Human-Computer Interaction – INTERACT 2013, P. Kotzé, G. Marsden, G. Lindgaard, J. Wesson, and M. Winckler (Eds.), LNCS, pp. 406–423. External Links: Link Cited by: p1.
  68. [106] A. Kohlhase (2013) Human-spreadsheet interaction. In Human-computer interaction – interact 2013Human-Computer Interaction – INTERACT 2013, P. Kotzé, G. Marsden, G. Lindgaard, J. Wesson, and M. Winckler (Eds.), LNCS, pp. 571–578. Cited by: p1.
  69. [117] M. Kohlhase, F. Mance, and F. Rabe (2013) A universal machine for biform theory graphs. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science. External Links: Link Cited by: p1.
  70. [124] M. Kohlhase, C. Prodescu, and C. Liguda (2013) XLSearch: a search engine for spreadsheets. In Symp. of the european spreadsheet risks interest group (EuSpRIG 2013)Symp. of the European Spreadsheet Risks Interest Group (EuSpRIG 2013), External Links: Link Cited by: p1.
  71. [139] M. Kohlhase (2013) Knowledge management for systematic engineering design in CAD systems. In Professionelles Wissenmanagement Management, Konferenzbeiträge der 7. KonferenzProfessionelles Wissenmanagement Management, Konferenzbeiträge der 7. Konferenz, F. Lehner, N. Amende, and N. Fteimi (Eds.), pp. 202–217. External Links: Link Cited by: p1.
  72. [140] M. Kohlhase (2013) The flexiformalist manifesto. In International workshop on symbolic and numeric algorithms for scientific computing (SYNASC 2012)14th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), A. Voronkov, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. M. Watt, and D. Zaharie (Eds.), pp. 30–36. External Links: Link Cited by: p1.
  73. [143] C. Lange, M. B. Caminati, M. Kerber, T. Mossakowski, C. Rowat, M. Wenzel, and W. Windsteiger (2013) A qualitative comparison of the suitability of four theorem provers for basic auction theory. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 200–215. External Links: 1303.4193 Cited by: p1.
  74. [146] C. Lange, M. Kerber, and C. Rowat (2013) Applying mechanised reasoning in economics – making reasoners applicable for domain experts. In INFORMATIK 2013: Informatik angepasst an Mensch, Organisation und Umwelt, M. Horbach (Ed.), Lecture Notes in Informatics, pp. 153–156. External Links: ISBN 978-3-88579-614-5 Cited by: p1.
  75. [151] C. Lange, C. Rowat, and M. Kerber (2013) The formare project – formal mathematical reasoning in economics. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 330–334. External Links: 1303.4194 Cited by: p1.
  76. [161] T. Mossakowski, O. Kutz, and C. Lange (2013) Semantics of the distributed ontology language: institutes and institutions. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, T. Mossakowski, N. Martí-Oliet, and M. Palomino Tarjuelo (Eds.), LNCS, pp. 212–230. Cited by: p1.
  77. [162] T. Mossakowski, O. Kutz, and C. Lange (2013) Three semantics for the core of the Distributed Ontology Language (extended abstract). In International Joint Conference on Artificial Intelligence, F. Rossi (Ed.), Cited by: p1, 160.
  78. [178] F. Rabe (2013) The MMT API: A Generic MKM System. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 339–343. Cited by: p1.
  79. [179] A. Ruf, M. Berges, and P. Hubwieser (2013) Types of assignments for novice programmers. In Proceedings of the 8th Workshop in Primary and Secondary Computing Education, New York, pp. 43–44. External Links: ISBN 978-1-4503-2455-7, Document Cited by: p1.
  80. [33] C. David, C. Jucovschi, A. Kohlhase, and M. Kohlhase (2012) Semantic Alliance: a framework for semantic allies. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 49–64. External Links: Link Cited by: p1.
  81. [56] F. Horozal, M. Kohlhase, and F. Rabe (2012) Extending MKM formats at the statement level. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 65–80. External Links: Link Cited by: p1.
  82. [69] M. Iancu and F. Rabe (2012) Management of Change in Declarative Languages. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 325–340. Cited by: p1.
  83. [72] C. Jucovschi (2012) Cost-effective integration of mkm semantic services into editing environments. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 96–110. External Links: Link Cited by: p1.
  84. [118] M. Kohlhase, B. A. Matican, and C. C. Prodescu (2012) MathWebSearch 0.5 – Scaling an Open Formula Search Engine. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 342–357. External Links: Link Cited by: p1.
  85. [138] M. Kohlhase (2012) The Planetary project: towards eMath3.0. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 448–452. External Links: 1206.5048 Cited by: p1.
  86. [144] C. Lange, P. Ion, A. Dimou, C. Bratsas, J. Corneli, W. Sperber, M. Kohlhase, and I. Antoniou (2012) Reimplementing the mathematics subject classification (MSC) as a linked open dataset. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 458–462. External Links: 1204.5086 Cited by: p1.
  87. [145] C. Lange, P. Ion, A. Dimou, C. Bratsas, W. Sperber, M. Kohlhase, and I. Antoniou (2012) Bringing mathematics to the web of data: the case of the mathematics subject classification. In The semantic webThe Semantic Web, E. Simperl, P. Cimiano, A. Polleres, O. Corcho, and V. Presutti (Eds.), LNCS, pp. 763–777. External Links: Link, Document Cited by: p1.
  88. [149] C. Lange, O. Kutz, T. Mossakowski, and M. Grüninger (2012) The distributed ontology language (DOL): ontology integration and interoperability applied to mathematical formalization. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 463–467. External Links: 1204.5093 Cited by: p1.
  89. [150] C. Lange, T. Mossakowski, O. Kutz, C. Galinski, M. Grüninger, and D. Couto Vale (2012) The Distributed Ontology Language (DOL): use cases, syntax, and extensibility. In Terminology and knowledge engineering conference (TKE)Terminology and Knowledge Engineering Conference (TKE), G. Aguado de Cea, M. C. Suárez-Figueroa, R. García-Castro, and E. Montiel-Ponsoda (Eds.), pp. 33–48. External Links: 1208.0293 Cited by: p1.
  90. [160] T. Mossakowski, O. Kutz, and C. Lange (2012) Three semantics for the core of the Distributed Ontology Language. In Formal Ontology in Information Systems, M. Donnelly and G. Guizzardi (Eds.), Frontiers in Artificial Intelligence and Applications, pp. 337–352. Note: Extended abstract published as [162] External Links: ISBN 978-1-61499-084-0, Link Cited by: p1.
  91. [177] F. Rabe (2012) A Query Language for Formal Mathematical Libraries. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 142–157. External Links: 1204.4685 Cited by: p1.
  92. [189] C. Tankink, C. Lange, and J. Urban (2012) Point-and-write — documenting formal mathematics by reference. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 169–185. External Links: 1204.5094 Cited by: p1.
  93. [1] J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, P. Rudnicki, and J. Urban (2011) Licensing the Mizar Mathematical Library. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 149–163. Cited by: p1.
  94. [5] S. Autexier, C. David, D. Dietrich, M. Kohlhase, and V. Zholudev (2011) Workflows for the management of change in science, technologies, engineering and mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 164–179. External Links: Link Cited by: p1.
  95. [25] M. Cîrlănaru, D. Ginev, and C. Lange (2011) Authoring and publishing of units and quantities in semantic documents. In The semantic web: ESWC 2011 workshopsThe Semantic Web: ESWC 2011 Workshops, R. García Castro, D. Fensel, and G. Antoniou (Eds.), LNCS, pp. 202–216. External Links: Link Cited by: p1.
  96. [27] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, and F. Rabe (2011) A Proof Theoretic Interpretation of Model Theoretic Hiding. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  97. [28] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, F. Rabe, and K. Sojakova (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  98. [29] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, and F. Rabe (2011) Project abstract: logic atlas and integrator (LATIN). In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 289–291. External Links: Link, Document Cited by: p1.
  99. [48] D. Ginev, H. Stamerjohanns, and M. Kohlhase (2011) The ML daemon: editable math on the collaborative web. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 292–294. Cited by: p1.
  100. [54] F. Horozal, A. Iacob, C. Jucovschi, M. Kohlhase, and F. Rabe (2011) Combining source, content, presentation, narration, and relational representation. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 212–227. External Links: Link Cited by: p1.
  101. [55] F. Horozal, M. Kohlhase, and F. Rabe (2011) Extending OpenMath with Sequences. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
  102. [93] A. Kohlhase and M. Kohlhase (2011) Maintaining islands of consistency via versioned links. In Proceedings of the 29th annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29th annual ACM international conference on Design of communication (SIGDOC), pp. 167–174. External Links: Link Cited by: p1.
  103. [94] A. Kohlhase and M. Kohlhase (2011) Maintaining islands of consistency via versioned links. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), External Links: Link Cited by: p1.
  104. [95] A. Kohlhase and M. Kohlhase (2011) Towards a flexible notion of document context. In Proceedings of the 29th annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29th annual ACM international conference on Design of communication (SIGDOC), pp. 181–188. External Links: Link Cited by: p1.
  105. [126] M. Kohlhase, F. Rabe, and C. Sacerdoti Coen (2011) A foundational view on integration problems. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 107–122. Note: https://kwarc.info/kohlhase/papers/cicm11-integration.pdf External Links: Link Cited by: p1.
  106. [147] C. Lange, M. Kohlhase, C. David, D. Ginev, A. Kohlhase, B. Matican, S. Mirea, and V. Zholudev (2011) The planetary system: executable science, technology, engineering and math papers. In The semantic web: research and applications (part II)ESWC (Part II), G. Antoniou, M. Grobelnik, E. Paslaru Bontas Simperl, B. Parsia, D. Plexousakis, P. D. Leenheer, and J. Z. Pan (Eds.), LNCS, pp. 471–475. External Links: 1103.1482 Cited by: p1.
  107. [153] C. Lange (2011) Krextor – an extensible framework for contributing content math to the web of data. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 304–306. External Links: Link Cited by: p1.
  108. [6] S. Autexier and N. Müller (2010) Semantics-based change impact analysis for heterogeneous collections of documents. In Proceedings of the 10th ACM symposium on document engineeringProceedings of the 10th ACM symposium on Document engineering, M. Gormish and R. Ingold (Eds.), DocEng ’10, pp. 97–106. External Links: Link, Document Cited by: p1.
  109. [32] C. David, C. Lange, and F. Rabe (2010) Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and Wolfram—Alpha. In CALCULEMUS (Emerging Trends), D. Delahaye and R. Rioboo (Eds.), Technical Reports of CEDRIC (CNAM/ENSIIE), pp. 13–30. Cited by: p1.
  110. [34] C. David, M. Kohlhase, C. Lange, F. Rabe, N. Zhiltsov, and V. Zholudev (2010) Publishing math lecture notes as linked data. In The semantic web: research and applications (part II)The Semantic Web: Research and Applications (Part II), L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, and T. Tudorache (Eds.), LNCS, pp. 370–375. External Links: 1004.3390v1 Cited by: p1.
  111. [71] C. Jucovschi and M. Kohlhase (2010) sTeXIDE: an integrated development environment for sTeX collections. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton (Eds.), LNAI, pp. 336–344. External Links: Link Cited by: p1.
  112. [81] A. Kohlhase, M. Kohlhase, and C. Lange (2010) Dimensions of formality: a case study for MKM in software engineering. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton (Eds.), LNAI, pp. 355–369. External Links: 1004.5071v1 Cited by: p1.
  113. [82] A. Kohlhase, M. Kohlhase, and C. Lange (2010) sTeX – a system for flexible formalization of linked data. In 6th international conference on semantic systems (I-Semantics) and the 5th international conference on pragmatic webProceedings of the 6th International Conference on Semantic Systems (I-Semantics) and the 5th International Conference on Pragmatic Web, A. Paschke, N. Henze, T. Pellegrini, and H. Weigand (Eds.), External Links: 1006.4474v1, Document Cited by: p1.
  114. [92] A. Kohlhase and M. Kohlhase (2010) What we understand is what we get: assessment in spreadsheets. In Symp. of the european spreadsheet risks interest group (EuSpRIG 2010)Symp. of the European Spreadsheet Risks Interest Group (EuSpRIG 2010), S. Thorne (Ed.), pp. 111–121. External Links: Link Cited by: p1.
  115. [105] A. Kohlhase (2010) Towards user assistance for documents via interactional semantic technology. In Proceedings of the 33.rd annual german conference on artificial intelligence ki’10KI 2010: Advances in Artificial Intelligence, R. Dillmann, J. Beyerer, U. D. Hanebeck, and T. Schultz (Eds.), LNAI, pp. 107–115. Cited by: p1.
  116. [127] M. Kohlhase, F. Rabe, and V. Zholudev (2010) Towards MKM in the large: modular representation and scalable software architecture. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton (Eds.), LNAI, pp. 370–384. External Links: 1005.5232v2 Cited by: p1.
  117. [191] V. Zholudev, M. Kohlhase, and F. Rabe (2010) A [insert xml format] database for [insert cool application]. In Proceedings of XML Prague 2010Proceedings of XML Prague 2010, External Links: Link Cited by: p1.
  118. [193] V. Zholudev and M. Kohlhase (2010) Scripting documents with xquery: virtual documents in TNTBase. In Proceedings of balisage: the markup conference 2010Proceedings of Balisage: The Markup Conference 2010, Balisage Series on Markup Technologies. Note: available at http://www.balisage.net/Proceedings/vol3/html/Zholudev01/BalisageVol3-Zholudev01.html External Links: Link Cited by: p1.
  119. [22] C. Calude and C. Müller (2009-07) Formal Proofs: Reconciling Correctness and Understanding. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI. Cited by: p1.
  120. [31] J. H. Davenport and M. Kohlhase (2009-07) Unifying Math Ontologies: A tale of two standards. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 263–278. External Links: Link Cited by: p1.
  121. [43] J. Gičeva, C. Lange, and F. Rabe (2009-07) Integrating web services into active mathematical documents. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 279–293. External Links: Link Cited by: p1.
  122. [88] A. Kohlhase and M. Kohlhase (2009-07) Compensating the computational bias of spreadsheets with MKM techniques. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 357–372. External Links: Link Cited by: p1.
  123. [91] A. Kohlhase and M. Kohlhase (2009-07) Spreadsheet interaction with frames: exploring a mathematical practice. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 341–356. External Links: Link Cited by: p1.
  124. [148] C. Lange and M. Kohlhase (2009-07) A mathematical approach to ontology authoring and documentation. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 389–404. External Links: Link Cited by: p1.
  125. [7] S. Awodey and F. Rabe (2009) Kripke Semantics for Martin-Löf’s Extensional Type Theory. In Typed Lambda Calculi and Applications (TLCA), P. Curien (Ed.), LNCS, Vol. 5608, pp. 249–263. Cited by: p1.
  126. [89] A. Kohlhase and M. Kohlhase (2009) Modeling task experience in user assistance systems. In Proceedings of the 27th annual ACM international conference on design of communication (SIGDOC)Proceedings of the 27th annual ACM international conference on Design of communication (SIGDOC), B. Mehlenbacher, A. Protopsaltis, A. Williams, and S. Slatterey (Eds.), pp. 135–142. External Links: Link Cited by: p1.
  127. [90] A. Kohlhase and M. Kohlhase (2009) Semantic transparency in user assistance systems. In Proceedings of the 27th annual ACM international conference on design of communication (SIGDOC)Proceedings of the 27th annual ACM international conference on Design of communication (SIGDOC), B. Mehlenbacher, A. Protopsaltis, A. Williams, and S. Slatterey (Eds.), pp. 89–96. External Links: Link Cited by: p1.
  128. [116] M. Kohlhase, J. Lemburg, L. Schröder, and E. Schulz (2009) Formal management of CAD/CAM processes. In 16th international symposium on formal methods (FM 2009)16th International Symposium on Formal Methods (FM 2009), A. Cavalcanti and D. Dams (Eds.), LNCS, pp. 223–238. External Links: Link Cited by: p1.
  129. [186] K. Sojakova and F. Rabe (2009) Translating Dependently-Typed Logic to First-Order Logic. In Recent Trends in Algebraic Development Techniques, A. Corradini and U. Montanari (Eds.), LNCS, Vol. 5486, pp. 326–341. Cited by: p1.
  130. [192] V. Zholudev and M. Kohlhase (2009) TNTBase: a versioned storage for XML. In Proceedings of balisage: the markup conference 2009Proceedings of Balisage: The Markup Conference 2009, Balisage Series on Markup Technologies. Note: available at https://kwarc.info/vzholudev/pubs/balisage.pdf External Links: Link Cited by: p1.
  131. [104] A. Kohlhase (2008-06) MS PowerPoint use from a micro-perspective. In Proceedings of the world conference on educational multimedia, hypermedia & telecommunications 2008 (ED-MEDIA’08)Proceedings of the World Conference on Educational Multimedia, Hypermedia & Telecommunications 2008 (ED-MEDIA’08), pp. 1279–1286. External Links: Link Cited by: p1.
  132. [119] M. Kohlhase, C. Müller, and F. Rabe (2008) Notations for living mathematical documents. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk (Eds.), LNAI, pp. 504–519. External Links: Link Cited by: p1.
  133. [152] C. Lange (2008) SWiM – a semantic wiki for mathematical knowledge management. In The semantic web: research and applicationsThe Semantic Web: Research and Applications, S. Bechhofer, M. Hauswirth, J. Hoffmann, and M. Koubarakis (Eds.), LNCS, pp. 832–837. External Links: 1003.5196v1 Cited by: p1.
  134. [163] C. Müller and M. Kohlhase (2008) Towards a community of practice toolkit based on semantically marked up artifacts. In Proceedings of the 1st World Summit of the Knowledge Society: Emerging Technologies and Information Systems for the Knowledge Society, M. D. Lytras and others (Eds.), LNAI, pp. 41–50. Cited by: p1.
  135. [188] H. Stamerjohanns and M. Kohlhase (2008) Transforming the arXiv to XML. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk (Eds.), LNAI, pp. 574–582. External Links: Link Cited by: p1.
  136. [97] A. Kohlhase, H. Schelhowe, and M. Lund (2007-09) What can the hundred languages of children teach us?. In Mensch & Computer 2007: Interaktion im PluralInteraktion im Plural, T. Gross (Ed.), Konferenzreihe Mensch und Computer, pp. 189–198. Cited by: p1.
  137. [102] A. Kohlhase (2007-06) Semantic powerpoint: content and semantic technology for educational added-value services in MS PowerPoint. In Proceedings of the world conference on educational multimedia, hypermedia & telecommunications 2007 (ED-MEDIA’07)Proceedings of the World Conference on Educational Multimedia, Hypermedia & Telecommunications 2007 (ED-MEDIA’07), C. Montgomerie and J. Seale (Eds.), pp. 3576–3583. External Links: Link Cited by: p1.
  138. [53] F. F. Horozal and C. E. Brown (2007) Formal representation of mathematics in a dependently typed set theory. In MKM/CalculemusTowards Mechanized Mathematical Assistants. MKM/Calculemus, M. Kauers, M. Kerber, R. Miner, and W. Windsteiger (Eds.), LNAI, pp. 265–279. Cited by: p1.
  139. [87] A. Kohlhase and M. Kohlhase (2007) Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch. In MKM/CalculemusTowards Mechanized Mathematical Assistants. MKM/Calculemus, M. Kauers, M. Kerber, R. Miner, and W. Windsteiger (Eds.), LNAI, pp. 266–279. External Links: Link Cited by: p1.
  140. [101] A. Kohlhase (2007) Semantic Perspectives on Knowledge Management and E-Learning. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, A. Hinneburg (Ed.), pp. 281–288. Cited by: p1.
  141. [103] A. Kohlhase (2007) The music is not in the piano: engaging vs. enabling MS PowerPoint. In Proceedings of Society for Information Technology and Teacher Education International Conference 2007 (SITE’07), R. Carlsen, K. McFerrin, J. Price, R. Weber, and D. A. Willis (Eds.), pp. 2026–2028. Note: St. Antonio, TX (USA), 2007-03-24/28 Cited by: p1.
  142. [164] C. Müller (2007) Presentation on Modeling Scientific Communities of Practice based on Semantic Markup of Scientific Documents and Web2.0. Technologies. In 7. konferenz für interaktive und kooperative medienMensch und Computer 2007, T. Gross (Ed.), Cited by: p1.
  143. [172] I. Normann and M. Kohlhase (2007) Extended formula normalization for ϵ-retrieval and sharing of mathematical knowledge. In MKM/CalculemusTowards Mechanized Mathematical Assistants. MKM/Calculemus, M. Kauers, M. Kerber, R. Miner, and W. Windsteiger (Eds.), LNAI, pp. 266–279. Cited by: p1.
  144. [99] A. Kohlhase (2006-03) Media or Medea Society? Learner and Learning Technology as Full Partners. In ICDML2006, B. Thipakorn (Ed.), Vol. 1, pp. 6–12. Note: Bangkok (Thailand), 2006-03-13/14 Cited by: p1.
  145. [9] C. E. Benzmüller, C. E. Brown, and M. Kohlhase (2006) Cut-simulation in impredicative logics. In Automated reasoning — third international joint conference, ijcar 2006Automated Reasoning — Third International Joint Conference, IJCAR 2006, U. Furbach and N. Shankar (Eds.), LNAI, pp. 220–234. External Links: Link Cited by: p1.
  146. [52] E. Hilf, M. Kohlhase, and H. Stamerjohanns (2006) Capturing the content of physics: systems, observables, and experiments. In MKM 2006Mathematical Knowledge Management (MKM), J. Borwein and W. M. Farmer (Eds.), LNAI, pp. 165–178. External Links: Link Cited by: p1.
  147. [85] A. Kohlhase and M. Kohlhase (2006) An exploration in the space of mathematical knowledge. In Mathematical knowledge management, MKM’05Mathematical Knowledge Management, MKM’05, M. Kohlhase (Ed.), LNAI, pp. 17–32. External Links: Link Cited by: p1.
  148. [86] A. Kohlhase and M. Kohlhase (2006) Communities of Practice in MKM: An Extensional Model. In MKM 2006Mathematical Knowledge Management (MKM), J. Borwein and W. M. Farmer (Eds.), LNAI, pp. 179–193. External Links: Link Cited by: p1.
  149. [96] A. Kohlhase and M. Reichel (2006) Embodied constructionist learning: social tagging and folksonomies in e-learning environments. In Current Developments in Technology-Assisted Education (mICTE06), Vol. 3, Badajoz, Spain. Cited by: p1.
  150. [100] A. Kohlhase (2006) What if PowerPoint became emPowerPoint (through CPoint)?. In Society for Information Technology and Teacher Education, 17th International Conference SITE 2006, C. M. Crawford (Ed.), pp. 2934–2939. Note: Orlando (USA), 2006-03-20/24 Cited by: p1.
  151. [129] M. Kohlhase and I. Şucan (2006) A search engine for mathematical formulae. In Proceedings of artificial intelligence and symbolic computation, AISC’2006Proceedings of Artificial Intelligence and Symbolic Computation, AISC’2006, T. Ida, J. Calmet, and D. Wang (Eds.), LNAI, pp. 241–253. External Links: Link Cited by: p1.
  152. [176] F. Rabe (2006) First-Order Logic with Dependent Types. In Automated reasoning — third international joint conference, ijcar 2006Automated Reasoning — Third International Joint Conference, IJCAR 2006, U. Furbach and N. Shankar (Eds.), LNAI, pp. 377–391. Cited by: p1.
  153. [98] A. Kohlhase (2005-11) Overcoming Proprietary Hurdles: CPoint as Invasive Editor. In Open source for education in europe: research and practiseOpen Source for Education in Europe: Research and Practise, F. de Vries, G. Attwell, R. Elferink, and A. Tödt (Eds.), pp. 51–56. Cited by: p1.
  154. [137] M. Kohlhase (2005-11) OMDoc: Open Mathematical Documents. In Open source for education in europe: research and practiseOpen Source for Education in Europe: Research and Practise, F. de Vries, G. Attwell, R. Elferink, and A. Tödt (Eds.), pp. 137–143. Cited by: p1.
  155. [84] A. Kohlhase and M. Kohlhase (2004) CPoint: dissolving the author’s dilemma. In Mathematical knowledge management, MKM’04Mathematical Knowledge Management, MKM’04, A. Asperti, G. Bancerek, and A. Trybulec (Eds.), LNAI, pp. 175–189. External Links: Link Cited by: p1.
  156. [26] E. Clarke, M. Kohlhase, J. Ouaknine, and K. Sutner (2003-09) System description: analytica 2. In 11th symposium on the integration of symbolic computation and mechanized reasoning (Calculemus 2003)Proceedings of the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2003), T. Hardin and R. Rioboo (Eds.), pp. 69–74. External Links: Link Cited by: p1.
  157. [110] M. Kohlhase and R. Anghelache (2003) Towards collaborative content management and version control for structured mathematical knowledge. In Mathematical knowledge management, MKM’03Mathematical Knowledge Management, MKM’03, A. Asperti, B. Buchberger, and J. H. Davenport (Eds.), LNCS, pp. 147–161. External Links: Link Cited by: p1.
  158. [4] A. Asperti and M. Kohlhase (2002) MathML in the MoWGLI project. In Second international conference on mathml and technologies for math on the webSecond International Conference on MathML and Technologies for Math on the Web, External Links: Link Cited by: p1.
  159. [130] M. Kohlhase, K. Sutner, P. Jansen, A. Kohlhase, P. Lee, D. Scott, and M. Szudzik (2002) Acquisition of math content in an academic setting. In Second international conference on mathml and technologies for math on the webSecond International Conference on MathML and Technologies for Math on the Web, External Links: Link Cited by: p1.
  160. [185] J. Siekmann, C. Benzmüller, V. Brezhnev, L. Cheikhrouhou, A. Fiedler, A. Franke, H. Horacek, M. Kohlhase, A. Meier, E. Melis, M. Moschner, I. Normann, M. Pollet, V. Sorge, C. Ullrich, C. Wirth, and J. Zimmer (2002) Proof development with Ωmega. In Automated deduction — cade-18Automated Deduction — CADE-18, A. Voronkov (Ed.), LNAI, pp. 144–149. Cited by: p1.
  161. [194] J. Zimmer and M. Kohlhase (2002) System Description: The MathWeb software bus for distributed mathematical reasoning. In Automated deduction — cade-18Automated Deduction — CADE-18, A. Voronkov (Ed.), LNAI, pp. 247–252. External Links: Link Cited by: p1.
  162. [135] M. Kohlhase (2001) Formal representation issues in an open mathematical knowledge base. In Electronic proceedings of the first international workshop on mathematical knowledge management: MKM’2001Electronic Proceedings of the First International Workshop on Mathematical Knowledge Management: MKM’2001, B. Buchberger and O. Caprotti (Eds.), External Links: Link Cited by: p1.
  163. [136] M. Kohlhase (2001) OMDoc: towards an internet standard for the administration, distribution and teaching of mathematical knowledge. In Proceedings of Artificial Intelligence and Symbolic Computation, AISC’2000Proceedings of Artificial Intelligence and Symbolic Computation, AISC’2000, E. R. Lozano (Ed.), LNAI, pp. 32–52. External Links: Link Cited by: p1.
  164. [3] A. Armando, M. Kohlhase, and S. Ranise (2000) Communication protocols for mathematical services based on KQML and OMRS. In CALCULEMUS-2000, systems for integrated computation and deductionProceedings of the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus-2000), M. Kerber and M. Kohlhase (Eds.), pp. 34–48. External Links: Link Cited by: p1.
  165. [38] A. Franke and M. Kohlhase (2000) System description: MBase, an open mathematical knowledge base. In Automated Deduction – cade-17Automated Deduction – CADE-17, D. McAllester (Ed.), LNAI, pp. 455–459. External Links: Link Cited by: p1.
  166. [113] M. Kohlhase and A. Koller (2000) Towards a tableaux machine for language understanding. In ICoS-2. inference in computational semantics. workshop proceedingsProceedings of Inference in Computational Semantics ICoS-2, J. Bos and M. Kohlhase (Eds.), pp. 57–88. Cited by: p1.
  167. [134] M. Kohlhase (2000) Model generation for discourse representation theory. In Proceedings of of the 14th european conference on artifical intelligenceProceedings of of the 14th European Conference on Artifical Intelligence, W. Horn (Ed.), pp. 441–445. External Links: Link Cited by: p1.
  168. [173] M. Pinkal and M. Kohlhase (2000) Feature logic for dotted types: a formalism for complex word meanings. In Proceedings of the 38th Annual Meeting of the Association for Computational Linguistics, Hongkong, pp. 521–528. External Links: Link Cited by: p1.
  169. [20] P. Blackburn, J. Bos, M. Kohlhase, and H. de Nivelle (1999) Inference and computational semantics. In Proceedings of IWCS III (third international workshop on computational semantics)Proceedings of IWCS III (Third International Workshop on Computational Semantics), H. Bunt, L. Kievit, R. Muskens, and M. Verlinden (Eds.), pp. 5–19. Cited by: p1.
  170. [37] A. Franke and M. Kohlhase (1999) System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Automated deduction — CADE-16Automated Deduction — CADE-16, H. Ganzinger (Ed.), LNAI, pp. 217–221. External Links: Link Cited by: p1.
  171. [51] S. Hess, C. Jung, M. Kohlhase, and V. Sorge (1998-07) An implementation of distributed mathematical services. In 6th calculemus and types workshop6th CALCULEMUS and TYPES Workshop, A. Cohen and H. Barendregt (Eds.), Cited by: p1.
  172. [10] C. Benzmüller and M. Kohlhase (1998) Extensional higher order resolution. In Proceedings of the 15th Conference on Automated DeductionProceedings of the 15th Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 56–72. External Links: Link Cited by: p1.
  173. [11] C. Benzmüller and M. Kohlhase (1998) LEO – a higher order theorem prover. In Proceedings of the 15th Conference on Automated DeductionProceedings of the 15th Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 139–144. External Links: Link Cited by: p1.
  174. [8] C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge (1997) Ωmega: towards a mathematical assistant. In Proceedings of the 14th Conference on Automated DeductionProceedings of the 14th Conference on Automated Deduction, W. McCune (Ed.), LNAI, pp. 252–255. External Links: Link Cited by: p1.
  175. [36] M. Egg and M. Kohlhase (1997) Dynamic control of quantifier scope. In Proceedings of the 11th Amsterdam Colloquium, P. Dekker (Ed.), Amsterdam, The Netherlands, pp. 109–114. Cited by: p1.
  176. [42] C. Gardent and M. Kohlhase (1997) Computing parallelism in discourse. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI)Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI), M. E. Pollack (Ed.), pp. 1016–1021. External Links: Link Cited by: p1.
  177. [64] D. Hutter and M. Kohlhase (1997) A coloured version of the λ-calculus. In Proceedings of the 14th Conference on Automated DeductionProceedings of the 14th Conference on Automated Deduction, W. McCune (Ed.), LNAI, pp. 291–305. Cited by: p1.
  178. [78] M. Kerber and M. Kohlhase (1997) Mechanising partiality without re-implementation. In Proceedings of the 18.th annual german conference on artificial intelligence ki’97Proceedings of the 18.th Annual German Conference on Artificial Intelligence KI’97, G. Brewka, C. Habel, and B. Nebel (Eds.), LNAI, pp. 123–134. External Links: Link Cited by: p1.
  179. [115] M. Kohlhase and S. Kuschert (1997) Dynamic lambda calculus. In Proceedings of the 5th Meeting on Mathematics of Language – MOL5, pp. 85–92. Cited by: p1.
  180. [77] M. Kerber and M. Kohlhase (1996-08) A resolution calculus for presuppositions. In Proceedings of the 12th european conference on artificial intelligenceProceedings of the 12th European Conference on Artificial Intelligence, W. Wahlster (Ed.), pp. 375–379. External Links: Link Cited by: p1.
  181. [39] C. Gardent, M. Kohlhase, and N. van Leusen (1996) Corrections and higher-order unification. In Proceedings of KONVENS’96, Bielefeld, Germany, pp. 268–279. External Links: Link Cited by: p1.
  182. [40] C. Gardent and M. Kohlhase (1996) Focus and higher–order unification. In Proceedings of the 16th International Conference on Computational Linguistics, Copenhagen, pp. 268–279. External Links: Link Cited by: p1.
  183. [41] C. Gardent and M. Kohlhase (1996) Higher–order coloured unification and natural language semantics. In Proceedings of the 34th Annual Meeting of the Association for Computational Linguistics, Santa Cruz, pp. 1–9. External Links: Link Cited by: p1.
  184. [75] M. Kerber, M. Kohlhase, and V. Sorge (1996) Integrating computer algebra with proof planning. In Design and implementation of symbolic computation systems, disco’96Design and Implementation of Symbolic Computation Systems, DISCO’96, J. Calmet and C. Limogelli (Eds.), LNCS, pp. 204–215. Cited by: p1.
  185. [133] M. Kohlhase (1995) Higher-order tableaux. In Proceedings of the Tableau Workshop, Koblenz, Germany, pp. 294–309. External Links: Link Cited by: p1.
  186. [58] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann (1994) KEIM: a toolkit for automated deduction. In Proceedings of the 12th Conference on Automated DeductionProceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 807–810. External Links: Link Cited by: p1.
  187. [59] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann (1994) Ω-MKRP a proof development environment. In Proceedings of the 12th Conference on Automated DeductionProceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 788–792. External Links: Link Cited by: p1.
  188. [60] X. Huang, M. Kerber, M. Kohlhase, and J. Richts (1994) Adapting methods to novel tasks in proof planning. In 18th annual german conference on aritificial intelligence18th Annual German Conference on Aritificial Intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 379–390. External Links: Link Cited by: p1.
  189. [63] D. Hutter and M. Kohlhase (1994) A colored version of the λ calculus. In Proceedings of the 12th Conference on Automated DeductionProceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 291–305. Cited by: p1.
  190. [70] P. Johann and M. Kohlhase (1994) Unification in an extensional lambda calculus with ordered function sorts and constant overloading. In Proceedings of the 12th Conference on Automated DeductionProceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 620–634. External Links: Link Cited by: p1.
  191. [76] M. Kerber and M. Kohlhase (1994) A mechanization of strong Kleene logic for partial functions. In Proceedings of the 12th Conference on Automated DeductionProceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 371–385. External Links: Link Cited by: p1.
  192. [132] M. Kohlhase (1994) Unification in a λ-calculus with term declarations and function sorts. In 18th annual german conference on aritificial intelligence18th Annual German Conference on Aritificial Intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 331–342. External Links: Link Cited by: p1.
  193. [123] M. Kohlhase and F. Pfenning (1993) Unification in a λ-calculus with intersection types. In Proceedings of the International Logic Programming Symposion ILPS’93, D. Miller (Ed.), pp. 488–505. External Links: Link Cited by: p1.
  194. [131] M. Kohlhase (1992) Unification in order-sorted type theory. In Proceedings of the international conference on logic programming and automated reasoning lpar’92Proceedings of the International Conference on Logic Programming and Automated Reasoning LPAR’92, A. Voronkov (Ed.), LNAI, pp. 421–432. Cited by: p1.

Monographs

  1. [4] C. Lange (2011) Enabling collaboration on semiformal mathematical knowledge by semantic web integration. Studies on the Semantic Web, AKA Verlag and IOS Press, Heidelberg and Amsterdam. External Links: ISBN 978-1-60750-840-3, Link Cited by: p1.
  2. [3] C. Lange (Ed.) (2006-09) Wikis und blogs – Planen, Einrichten, Verwalten. C&L Computer- und Literaturverlag. External Links: ISBN 3-936546-44-4 Cited by: p1.
  3. [1] M. Kohlhase (2006-08) OMDoc – an open markup format for mathematical documents [version 1.2]. LNAI, Springer Verlag. External Links: Link Cited by: p1.
  4. [2] C. Lange (Ed.) (2005-09) Wiki – Planen, Einrichten, Verwalten. C&L Computer- und Literaturverlag. External Links: ISBN 3-936546-28-2 Cited by: p1.

Conference Proceedings Edited

  1. [1] A. Adrian, S. Evert, M. K. Kohlhase, and M. Zwickel (Eds.) (2022) Digitalisierung von zivilprozess und rechtsdurchsetzung. Schriften zum Prozessrecht, Duncker & Humblot, Berlin. Cited by: p1.
  2. [7] J. Blanchette, J. Davenport, P. Koepke, A. Kohlhase, M. Kohlhase, A. Naumowicz, D. Müller, Y. Sharoda, and C. S. Coen (Eds.) (2021) Workshop papers at 14th conference on intelligent computer mathematics cicm 2021. External Links: Link Cited by: p1.
  3. [10] C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.) (2019) Intelligent computer mathematics. LNAI, Springer. External Links: Document Cited by: p1.
  4. [6] O. Hasan, A. Youssef, A. Naumowicz, W. Farmer, C. Kaliszyk, D. Gallois-Wong, F. Rabe, G. D. Reis, G. Passmore, J. Davenport, M. Pfeiffer, M. Kohlhase, S. Autexier, S. Tahar, T. Koprucki, U. Siddique, W. Neuper, W. Windsteiger, W. Schreiner, W. Sperber, and Z. Kovács (Eds.) (2018) Workshop papers at 11th conference on intelligent computer mathematics cicm 2018. External Links: Link Cited by: p1.
  5. [14] F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.) (2018) Intelligent computer mathematics. LNAI, Springer. External Links: Document, ISBN 978-3-319-96811-7 Cited by: p1.
  6. [9] H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.) (2017) Intelligent computer mathematics. LNAI, Springer. External Links: Document, ISBN 978-3-319-62074-9 Cited by: p1.
  7. [12] M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa (Eds.) (2016) Intelligent computer mathematics. LNAI, Springer. External Links: ISBN 978-3-319-08434-3 Cited by: p1.
  8. [4] J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.) (2013) Intelligent computer mathematics. Lecture Notes in Computer Science, Springer. External Links: Document, ISBN 978-3-642-39319-8 Cited by: p1.
  9. [5] J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.) (2011) Intelligent computer mathematics. LNAI, Springer Verlag. External Links: ISBN 978-3-642-22672-4 Cited by: p1.
  10. [8] C. Freksa, M. Kohlhase, and K. Schill (Eds.) (2006) Proceedings of the 29.th annual german conference on artificial intelligence KI’06. LNAI, Bremen, Germany. Cited by: p1.
  11. [13] M. Kohlhase (Ed.) (2006) Mathematical knowledge management, MKM’05. LNAI, Springer Verlag. Cited by: p1.
  12. [3] J. Bos and M. Kohlhase (Eds.) (2003) Logic journal of the igpl. Vol. 11(3), Oxford University Press. Note: Special Issue for ICOS-2 Cited by: p1.
  13. [2] J. Bos and M. Kohlhase (Eds.) (2000) ICoS-2. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
  14. [11] M. Kerber and M. Kohlhase (Eds.) (2000) CALCULEMUS-2000, systems for integrated computation and deduction. AKPeters, St. Andrews, Scotland. Cited by: p1.

Theses

  1. [89] T. W. Schöner (2023-04-23) User-fact interaction in the UFrameIT framework. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  2. [34] P. Hutterer (2023-04-12) Integrating automated semantic annotation using machine learning into authoring workflows for flexiformal documents. M.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  3. [3] J. Albert (2023) A multi-system narrative search for mathematical libraries – narrative harvesting of math archives. MSc Thesis, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  4. [16] A. Christoph (2023) Hybride künstliche intelligenz in der industriellen produktion am beispiel der sichtprüfung von räumlichen montagebaugruppen. MSc Thesis, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  5. [25] T. Friedrich (2023) Towards digitized register courts ”= a symbolic pipeline for information extraction. MSc Thesis, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  6. [29] M. Helmke (2023) Formalization and annotation of company register processes via logic. MSc Thesis, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  7. [67] J. Peters (2023) MathWebSearch 2.0: scalable formula indexing with perfect sharing. MSc Thesis, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  8. [93] M. Tintemann (2022-10-12) LoViWo extended. facilitating further content additions for an existing knowledge based physics simulation prototype. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  9. [21] M. N. Dreier (2022-10-11) Projektarbeit: erweiterung der mmt-wissensbasis für volumenbasierte mathematik-aufgaben in uframeit. M.Sc. Project Report, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  10. [79] N. Roux (2022-03-23) A framework for defining structure-preserving diagram operators. M.Sc. Thesis, FAU Erlangen-Nürnberg. Note: linked PDF is an old outdated one External Links: Link Cited by: p1.
  11. [2] J. Albert (2022) Towards a multi-system narrative search for mathematical libraries – narrative harvesting. Master Project Report, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  12. [6] M. Banken (2022) Theory intersection. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  13. [19] I. de Souza Bueno Júnior (2022) Interfacing mathematical human-computer interactions by using the grammatical logical inference framework. Bachelor’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  14. [96] S. Weber (2022) The problem-creator-menu – a game content IDE for unity based UFrameIT games. Bachelor Project Report, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  15. [100] M. Zimmer (2022) From proof-of-concept to proto-game: first steps. Bachelor Project Report, Computer Science, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  16. [17] A. Dalga (2021-03) Semantik-extraktion für mengen-phrasen in naturwissenschaftlichen papieren durch sequence-to-sequence modelle. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  17. [88] J. Schihada (2021) Knowledge-based physics simulation. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  18. [94] M. Wagner (2021) Tetrapodal harvesting of the oeis – fair, semantic extraction and organization. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  19. [15] C. Cerny (2020-12-04) Generating expressions in mmt. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  20. [20] M. N. Dreier (2020-12-04) Syntax und semantik von funktionalen konzepten in der mathematik. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  21. [80] N. Roux (2020-07-17) Structure-preserving diagram operators. Master Project Report, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  22. [12] B. Bösl (2020-03) Designing a framework for beneficial serious math games using the FrameIt method. M.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  23. [83] J. F. Schaefer (2020) Implementing ForTheL in GLIF – a case study. Master Project Report. External Links: Link Cited by: p1.
  24. [84] J. F. Schaefer (2020) Prototyping NLU pipelines – a type-theoretical framework. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  25. [85] A. Schärtl (2020) Ulo-storage – indexing and querying organizational data in mathematical libraries. Master Project Report. External Links: Link Cited by: p1.
  26. [87] J. Schihada (2020) FrameIT. Master Project Report. External Links: Link Cited by: p1.
  27. [4] C. Alt (2019-12) Diagram chasing done meta – formula search for nLab. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  28. [61] D. Müller (2019-12) Mathematical knowledge management across formal libraries. Ph.D. Thesis, Informatics, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  29. [78] N. Roux (2019-07-01) Refactoring of theory graphs in knowledge representation systems. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  30. [81] M. Rupprecht (2019-05) Visualization of theory graphs. M.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  31. [58] R. Marcus (2019-04) 3D-visualization of theory graphs. M.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  32. [27] D. Gorolenkov (2018-09) Meaning extraction in stem-documents by machine-learning methods. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  33. [54] P. Lohnert (2018-09) Automatisches ableiten von steuerungsabläufen durch semantische modellierung von funktionen und methoden der künstlichen intelligenz. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  34. [11] J. Betzendahl (2018-04) Translating the IMPS theory library to MMT / OMDoc. Master’s Thesis, Informatik, Universität Bielefeld. External Links: Link Cited by: p1.
  35. [68] M. Plivelic (2018-02) Using machine learning to support annotating of keywords in mathematical texts. B.Sc. Thesis, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  36. [75] M. Rapp (2018) Hybrid logics for arguments, beliefs, and their dynamics. Master’s Thesis, University of Amsterdam. External Links: Link Cited by: p1.
  37. [98] T. Wiesing (2017-08) Enabling cross-system communication using virtual theories and QMT. Master’s Thesis, Jacobs University Bremen, Bremen, Germany. External Links: Link Cited by: p1.
  38. [38] M. Iancu (2017) Towards flexiformal mathematics. Ph.D. Thesis, Jacobs University, Bremen, Germany. External Links: Link Cited by: p1.
  39. [69] T. Pollinger (2017) Knowledge representation for modeling and simulation – bridging the gap between informal PDE theory and simulations practice. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  40. [72] U. Rabenstein (2017) Meaning extraction and semantic services in STEM-documents – a case study on quantity expressions and units. Master’s Thesis, Informatik, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  41. [55] E. Luzhnica (2016) Formula semantification and automated relation finding in the OEIS. B. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  42. [76] M. Rapp (2016) Is there an ergodic axiom in economics?. Master’s Thesis, London School of Economics and Political Science. Cited by: p1.
  43. [77] D. Rochau (2016) FrameIT reloaded: serious math games from logic. B.Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  44. [82] J. F. Schaefer (2016) Declaration spotting in mathematical documents. B. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  45. [9] K. Berčič (2015-05) Constructions and catalogisation of symmetric graphs : phd thesis (in slovenian). Ph.D. Thesis, Faculty of Mathematics and Physics, University of Ljubljana. Cited by: p1.
  46. [97] T. Wiesing (2015) Semantic search for quantity expressions. B. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  47. [33] F. Horozal (2014-11) A framework for defining declarative languages. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  48. [10] J. Betzendahl (2014-08) Implementation of inverse coupled rewrite systems – a case study. Bachelor’s Thesis, Informatik, Universität Bielefeld. External Links: Link Cited by: p1.
  49. [70] C. C. Prodescu (2014) Text and formula search on ArXiv documents. M. Sc. Thesis, Jacobs University Bremen. Cited by: p1.
  50. [39] A. Jakubauskas (2013) Reflecting declarative rule implementations. M.Sc. Thesis, Jacobs University. External Links: Link Cited by: p1.
  51. [57] F. Mance (2013) A Practical OpenMath Machine. Master’s Thesis, Jacobs University Bremen. Note: Bachelor’s thesis Cited by: p1.
  52. [73] D. Rachev (2013) FrameIT: an user interface for applying mathematical theories to real world problems. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link, Document Cited by: p1.
  53. [74] M. Rapp (2013) Braucht die Ökonomie einen Paradigmenwechsel? Methodische Vorschläge nach Elinor Ostrom. Bachelor’s Thesis, Munich School of Philosophy. Cited by: p1.
  54. [18] C. David (2012) Semantic Alliance Framework: integrating documents and semantic services. M. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  55. [22] S. Dumbrava (2012) A Type Theory based on Reflection. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
  56. [32] F. F. Horozal (2012) Management of Change in the Web Ontology Language. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
  57. [37] M. Iancu (2012) Management of change in declarative languages. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
  58. [65] S. Oprea (2012) Modeling semantic similarity between scientific documents. B.Sc. Thesis, Jacobs University Bremen. Cited by: p1.
  59. [99] V. Zholudev (2012) Enhancing xml preservation and workflows. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  60. [26] D. Ginev (2011-08) The structure of mathematical expressions. Master’s Thesis, Jacobs University Bremen, Bremen, Germany. Note: https://kwarc.info/people/dginev/publications/DeyanGinev_MScThesis.pdf External Links: Link Cited by: p1.
  61. [36] A. Iacob (2011-08) Towards Project-Based Workflows in Twelf. Master’s Thesis, Jacobs University Bremen, Bremen, Germany. External Links: Link Cited by: p1.
  62. [35] A. Iacob (2011) Towards Project-Based Workflows in Twelf. Master’s Thesis, Jacobs University Bremen. Cited by: p1.
  63. [50] C. Lange (2011) Enabling collaboration on semiformal mathematical knowledge by semantic web integration. Ph.D. Thesis, Jacobs University Bremen. Note: Also available as a book [51] Cited by: p1.
  64. [51] C. Lange (2011) Enabling collaboration on semiformal mathematical knowledge by semantic web integration. Studies on the Semantic Web, AKA Verlag and IOS Press, Heidelberg and Amsterdam. External Links: ISBN 978-1-60750-840-3, Link Cited by: 50.
  65. [28] M. Grigore (2010) Knowledge-poor interpretation of mathematical expressions in context. M.Sc. Thesis, Jacobs University. External Links: Link Cited by: p1.
  66. [40] C. Jucovschi (2010) Editing knowledge in large mathematical corpora. a case study with semantic (sTeX). M.Sc. Thesis, Jacobs University. External Links: Link Cited by: p1.
  67. [60] C. Müller (2010) Adaptation of Mathematical Documents. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  68. [63] N. Müller (2010) Change management on semi-structured documents. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  69. [90] K. Sojakova (2010) Mechanically Verifying Logic Translations. Master’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  70. [5] Ş. Anca (2009) Natural language and mathematics processing for applicable theorem search. Master’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  71. [56] M. Makaveeva (2009) Management of change in common criteria it security documentation. M.Sc. Thesis, Jacobs University. External Links: Link Cited by: p1.
  72. [44] A. Kohlhase (2008-04) Semantic interaction design: composing knowledge with CPoint. Ph.D. Thesis, Computer Science, Universität Bremen. External Links: Link Cited by: p1.
  73. [1] A. Aiordachioaie (2008) Improving Panta Rhei. Master’s Thesis. External Links: Link Cited by: p1.
  74. [64] I. Normann (2008) Automated theory interpretation. Ph.D. Thesis, Jacobs University, Bremen, Germany. External Links: Link Cited by: p1.
  75. [71] F. Rabe (2008) Representing Logics and Logic Translations. Ph.D. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  76. [53] B. Laubner (2007-08) Using theory graphs to map mathematics: a case study and a prototype.. Master’s Thesis, Jacobs University, Bremen. External Links: Link Cited by: p1.
  77. [31] F. F. Horozal (2007) Towards a Natural Representation of Mathematics in Proof Assistants. Master’s Thesis, Saarland University, Saarbrücken, Germany. Cited by: p1.
  78. [66] D. Pesikan (2007) Coping with content representations of mathematics in editor environments: nOMDoc mode. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. Cited by: p1.
  79. [52] C. Lange (2006-08) A Semantic Wiki for Mathematical Knowledge Management. Diploma thesis, Universität Trier. External Links: Link Cited by: p1.
  80. [62] N. Müller (2005) OMDoc-Repräsentation von Programmen und Beweisen in VeriFun. Master’s Thesis, Programmiermethodik, Technische Universität Darmstadt. Note: https://kwarc.info/nmueller/papers/dt.pdf External Links: Link Cited by: p1.
  81. [23] S. Eisenhardt (2004) Model generation for negations in natural language. Master’s Thesis, Carnegie Mellon University. Cited by: p1.
  82. [92] W. Tayson (2004) Treating quantifier scope by model generation. Master’s Thesis, Carnegie Mellon University. Cited by: p1.
  83. [24] A. Franke (2003) MBase, a mathematical knowledge base. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  84. [14] A. Burkard (2001) Resource-adaptive model generation for natural language understanding. Master’s Thesis, Computational Linguistics, Saarland University. Cited by: p1.
  85. [95] S. Walther (2001) Model generation and dynamic semantics. Master’s Thesis, Computational Linguistics, Saarland University. Cited by: p1.
  86. [47] K. Konrad (2000) Model generation for natural language interpretation and analysis. Ph.D. Thesis, Universität des Saarlandes. External Links: Document Cited by: p1.
  87. [7] J. Baur (1999) Syntax and semantics of mathematical texts – a prototype. Master’s Thesis, Computational Linguistics, Saarland University. Cited by: p1.
  88. [8] C. Benzmüller (1999) Equality and extensionality in higher-order theorem proving. Ph.D. Thesis, Universität des Saarlandes. External Links: Link Cited by: p1.
  89. [30] S. Hess (1999) Human computer interaction in a proof development environment. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  90. [49] S. Kuschert (1999) Dynamic meaning and accommodation. Ph.D. Thesis, Saarland University. Cited by: p1.
  91. [42] L. Klein (1997) Intexing techniques for higher-order logic. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  92. [59] A. Meier (1997) Proof transformation, universtät des saarlandes. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  93. [91] V. Sorge (1996) Integrating a computer algebra system into a logical proof development environement. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  94. [41] G. Klein (1995) Unification for a lambda-calculus with term declarations and intersection sorts. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  95. [48] S. Kuschert (1995) An extension of the lambda-calculus by discourse representation structures. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  96. [46] M. Kohlhase (1994) A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. Thesis, Universität des Saarlandes. External Links: Link Cited by: p1.
  97. [43] A. Kohlhase (1990) The geometry of second order lagrangians in the plane. Master’s Thesis, TU Berlin. Cited by: p1.
  98. [13] A. Bozkurt (199) Strategies for resolution theorem provers in higher-order logic. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  99. [86] O. Scheja (199) Resolution for higher-order multi-valued logics. Master’s Thesis, Computer Science, Saarland University. Cited by: p1.
  100. [45] M. Kohlhase (1989) Eine hinreichende Bedingung für die starke, homologische Minimalität von kompakten, ℱ-extremalen Hyperflächen in glatten Mannigfaltigkeiten. Master’s Thesis, Universität Bonn. External Links: Link Cited by: p1.

Gray Literature

Worskhop Proceedings Edited

  1. [26] A. Kohlhase (Ed.) (2023) MathUI 2023: the 14th workshop on mathematical user interfaces. Cited by: p1.
  2. [25] A. Kohlhase (Ed.) (2022) MathUI 2021: the 13th workshop on mathematical user interfaces. Cited by: p1.
  3. [20] A. Kohlhase and E. Kübler (Eds.) (2017-10) Wissens- und erfahrungsmanagement (knowledge and experience management), FGWM. Note: Workshop at LWDA 2017 External Links: Link Cited by: p1.
  4. [23] A. Kohlhase and M. Pollanen (Eds.) (2017) MathUI 2017: the 12th workshop on mathematical user interfaces. External Links: Link Cited by: p1.
  5. [22] A. Kohlhase and P. Libbrecht (Eds.) (2016-07) Mathematical user interfaces workshop at CICM. External Links: Link Cited by: p1.
  6. [8] M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.) (2016) Intelligent computer mathematics – work in progress papers. External Links: Link Cited by: p1.
  7. [21] A. Kohlhase and P. Libbrecht (Eds.) (2015-07) Mathematical user interfaces workshop at CICM. External Links: Link Cited by: p1.
  8. [11] M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.) (2014) Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  9. [19] A. Henrich and H. Sperker (Eds.) (2013-10) Wissens- und erfahrungsmanagement LWA (lernen, wissensentdeckung und adaptivität) conference proceedings. Universität Bamberg. Cited by: 24.
  10. [24] A. Kohlhase and B. Rieger (Eds.) (2013-10) Wissens- und erfahrungsmanagement (knowledge and experience management), FGWM. Note: Workshop at LWA 2013, published as part of [19] Cited by: p1.
  11. [13] A. García Castro, C. Lange, P. Lord, and R. Stevens (Eds.) (2013) Proceedings of the 3rd workshop on semantic publishing, Extended Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  12. [27] C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger (Eds.) (2013) Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2013. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  13. [31] C. Lange, C. Rowat, and M. Kerber (Eds.) (2013) Enabling domain experts to use formalised reasoning. Society for the Study of Artificial Intelligence and Simulation of Behaviour (AISB). External Links: Link, ISBN 978-1-908187-32-1 Cited by: p1.
  14. [17] B. Good, F. van Harmelen, A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.) (2012) Proceedings of the 2nd workshop on semantic publishing, Extended Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  15. [37] P. Sojka and M. Kohlhase (Eds.) (2012) DML and MIR 2012. Masaryk University, Brno. External Links: ISBN 978-80-210-5542-1 Cited by: p1.
  16. [1] A. Asperti, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.) (2011) Intelligent Computer Mathematics, Work-in-Progress Proceedings. Technical Reports of University of Bologna, Vol. UBLCS-2011-04, University of Bologna. Cited by: p1.
  17. [7] J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.) (2011) Intelligent computer mathematics – work in progress papers. Cited by: p1.
  18. [12] A. García Castro, K. Baclawski, J. Bateman, K. Viljanen, and C. Lange (Eds.) (2011) Proceedings of the workshop ontologies come of age in the semantic web, International Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  19. [14] A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.) (2011) Proceedings of the 1st workshop on semantic publication, Extended Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  20. [15] H. Geuvers, G. Nadathur, F. Rabe, and C. Schürmann (Eds.) (2011) LFMTP 2011 - MLPA 2011 Informal Proceedings. Note: see http://kwarc.info/frabe/events/mlpa-11/index.html Cited by: p1.
  21. [34] C. Lange and J. Urban (Eds.) (2011) Proceedings of the itp 2011 workshop on mathematical wikis (mathwikis). CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  22. [16] A. Giurca, B. Endres-Niggemeyer, C. Lange, L. Maicher, and P. Hitzler (Eds.) (2010-06) AI Mashup Challenge. External Links: Link Cited by: p1.
  23. [9] M. d’Aquin, A. García Castro, C. Lange, and K. Viljanen (Eds.) (2010) Proceedings of the 1st workshop on ontology repositories and editors, Extended Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  24. [28] C. Lange, J. Reutelshöfer, S. Schaffert, and H. Skaf-Molli (Eds.) (2010) Proceedings of the 5th workshop on semantic wikis, Extended Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  25. [36] F. Rabe and C. Schürmann (Eds.) (2010) MLPA ’10: Proceedings of the 2nd Workshop on Modules and Libraries for Proof Assistants. Note: see http://kwarc.info/frabe/events/mlpa-10.html Cited by: p1.
  26. [18] M. Hartmann and F. Janssen (2009-09) LWA 2009; Workshop-Woche: Lernen – Wissen – Adaptivität. Technical report Vol. TUD-KE-2009-04, Universität Darmstadt. Cited by: 29.
  27. [29] C. Lange and J. Reutelshöfer (Eds.) (2009-09) Wissens- und erfahrungsmanagement (knowledge and experience management), FGWM. Note: Workshop at LWA 2009, published as part of [18] Cited by: p1.
  28. [30] C. Lange and J. Reutelshöfer (Eds.) (2009-09) Wissens- und erfahrungsmanagement (knowledge and experience management), FGWM. Vol. TUD-KE-2009-04, Universität Darmstadt. Cited by: p1.
  29. [33] C. Lange, S. Schaffert, H. Skaf-Molli, and M. Völkel (Eds.) (2009) Proceedings of the 4th workshop on semantic wikis, European Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  30. [35] F. Rabe and C. Schürmann (Eds.) (2009) MLPA ’09: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants. ACM International Conference Proceeding Series, Vol. 429, ACM. Cited by: p1.
  31. [6] O. Caprotti, S. Xambó, M. Huertas, M. Kohlhase, and M. Seppälä (Eds.) (2008) 3rd JEM workshop – joining educational mathematics. External Links: Link Cited by: p1.
  32. [32] C. Lange, S. Schaffert, H. Skaf-Molli, and M. Völkel (Eds.) (2008) Proceedings of the 3rd workshop on semantic wikis, European Semantic Web Conference. CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  33. [5] O. Caprotti, M. Kohlhase, and P. Libbrecht (Eds.) (2007-06) OpenMath/JEM workshop 2007. Note: online at http://www.openmath.org/meetings/linz2007/ External Links: Link Cited by: p1.
  34. [2] P. Baumgartner, P. A. Cairns, M. Kohlhase, and E. Melis (Eds.) (2003) Proceedings of the IJCAI 03 workshop on knowledge representation and automated reasoning for e-learning systems. Acapulco, Mexico. Cited by: p1.
  35. [4] P. Blackburn and M. Kohlhase (Eds.) (2001) ICoS-3. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
  36. [3] P. Baumgartner, U. Furbach, M. Kohlhase, W. McCune, W. Reif, M. Stickel, and T. Uribe (Eds.) (1998) CADE-15 workshop “problem-solving methodologies with automated deduction”. Cited by: p1.
  37. [10] J. Denzinger, M. Kohlhase, and B. Spencer (Eds.) (1998) CADE-15 workshop “using AI methods in deduction”. Cited by: p1.

Papers at Peer-Reviewed Workshops

  1. [16] A. Chugh, M. Kohlhase, and D. Müller (2023) Presentation of active documents in ALeA. In MathUI 2023: the 14th workshop on mathematical user interfacesMathUI 2023: The 14th Workshop on Mathematical User Interfaces, A. Kohlhase (Ed.), Note: submitted External Links: Link Cited by: p1.
  2. [80] A. Kohlhase and M. Kohlhase (2023) More interactions in ALeA – towards new added-value services based on semantic markup. In MathUI 2023: the 14th workshop on mathematical user interfacesMathUI 2023: The 14th Workshop on Mathematical User Interfaces, A. Kohlhase (Ed.), External Links: Link Cited by: p1.
  3. [174] L. Panzer and J. F. Schaefer (2023) AnnoTize: a flexible annotation tool for documents with mathematical formulae. In MathUI 2023: the 14th workshop on mathematical user interfacesMathUI 2023: The 14th Workshop on Mathematical User Interfaces, A. Kohlhase (Ed.), Note: accepted Cited by: p1.
  4. [205] J. F. Schaefer and M. Kohlhase (2023) Towards an annotation standard for stem documents – datasets, benchmarks, and spotters. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2023, C. Dubois and M. Kerber (Eds.), LNAI. Cited by: p1.
  5. [6] M. K. Andrea Kohlhase (2022) A conceptual design for an eye-tracking experiment on formula linebreaking. In MathUI 2021: the 13th workshop on mathematical user interfacesMathUI 2021: The 13th Workshop on Mathematical User Interfaces, A. Kohlhase (Ed.), Cited by: p1.
  6. [2] A. Adrian, M. Kohlhase, and M. Rapp (2021) A novel understanding of legal syllogism as a starting point for better legal symbolic ai systems. In 24. internationalen rechtsinformatik symposion (iris 2021)24. Internationalen Rechtsinformatik Symposion (IRIS 2021), E. S. und Walter Hötzendorfer und Franz Kummer und Ahti Saarenpää und Stefan Eder und Philip Hanke (Ed.), pp. 169ff.. External Links: Link Cited by: p1.
  7. [96] M. Kohlhase, A. Adrian, and M. Rapp (2021) Context graphs for ampliative analogical legal reasoning and argumentation. In 24. internationalen rechtsinformatik symposion (iris 2021)24. Internationalen Rechtsinformatik Symposion (IRIS 2021), E. S. und Walter Hötzendorfer und Franz Kummer und Ahti Saarenpää und Stefan Eder und Philip Hanke (Ed.), pp. 231ff.. External Links: Link Cited by: p1.
  8. [103] M. Kohlhase, R. Marcus, N. Roux, and J. Schihada (2021) Dynamic user interfaces via incremental knowledge management. In 13th MathUI Workshop 2021, Mathematical User Interaction, at the Conference on Intelligent Computer Mathematics, External Links: Link Cited by: p1.
  9. [167] D. Müller and C. Kaliszyk (2021) Disambiguating symbolic expressions in informal documents. In International Conference on Learning Representations, External Links: Link Cited by: p1.
  10. [177] F. Rabe (2021) A Language with Type-Dependent Equality. In Intelligent Computer Mathematics, F. Kamareddine and C. Sacerdoti Coen (Eds.), pp. 211–227. External Links: Document, Link Cited by: p1.
  11. [182] F. Rabe and N. Roux (2021) Systematic translation of formalizations of type theory from intrinsic to extrinsic style. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel and E. Tassi (Eds.), External Links: Link, Document Cited by: p1.
  12. [200] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: p1.
  13. [67] C. Kaliszyk and F. Rabe (2020) A survey of languages for formalizing mathematics. In Intelligent Computer Mathematics, C. Benzmüller and B. Miller (Eds.), Cham, pp. 138–156. External Links: ISBN 978-3-030-53518-6 Cited by: p1.
  14. [107] M. Kohlhase, F. Rabe, and M. Wenzel (2020) Making Isabelle content accessible in knowledge representation formats. In Proceedings of the 25th International Conference on Types for Proofs and Programs, TYPES 2019, M. Bezem and A. Mahboubi (Eds.), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 175. External Links: ISBN 978-3-95977-158-0, Link, Document Cited by: p1.
  15. [202] J. F. Schaefer, K. Amann, and M. Kohlhase (2020) Prototyping controlled mathematical languages in jupyter notebooks. In Mathematical software – icms 2020. 7th international conferenceMathematical Software – ICMS 2020. 7th international conference, A. M. Bigatti, J. Carette, J. H. Davenport, M. Joswig, and T. de Wolff (Eds.), LNCS, Vol. 12097, pp. 406–415. External Links: Link Cited by: p1.
  16. [204] J. F. Schaefer and M. Kohlhase (2020) GLIF: a declarative framework for symbolic natural language understanding. In Proceedings of the 6th Workshop on Formal and Cognitive Reasoning, C. Beierle, M. Ragni, F. Stolzenburg, and M. Thimm (Eds.), pp. 4–11. External Links: Link Cited by: p1.
  17. [10] K. Bercic (2019) Towards a census of relational data in mathematics. In Proceedings of the conference ”lernen, wissen, daten, analysen”, LWDAProceedings of the Conference ”Lernen, Wissen, Daten, Analysen”, LWDA, R. Jäschke and M. Weidlich (Eds.), CEUR Workshop Proceedings, Vol. 2454, pp. 207–217. External Links: Link Cited by: p1.
  18. [56] S. Hungerbühler, H. P. Jóhnsson, G. Lisowski, and M. Rapp (2019) Social choice and the problem of recommending essential readings. In At the Intersection of Language, Logic, and Information. ESSLLI 2018.At the Intersection of Language, Logic, and Information. ESSLLI 2018., J. Sikos and E. Pacuit (Eds.), Lecture Notes in Computer Science, Vol. 11667. Cited by: p1.
  19. [109] M. Kohlhase and M. Rapp (2019) Context graphs for argumentation logics. In Proceedings of the conference ”lernen, wissen, daten, analysen”, LWDAProceedings of the Conference ”Lernen, Wissen, Daten, Analysen”, LWDA, R. Jäschke and M. Weidlich (Eds.), CEUR Workshop Proceedings, Vol. 2454, pp. 265–279. External Links: Link Cited by: p1.
  20. [110] M. Kohlhase and J. F. Schaefer (2019) GF + MMT = GLF – from language to semantics through LF. In Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2019, D. Miller and I. Scagnetto (Eds.), Vol. 307, pp. 24–39. External Links: Document Cited by: p1.
  21. [169] D. Müller and F. Rabe (2019) Rapid prototyping formal systems in mmt: 5 case studies. In LFMTP 2019, External Links: Link Cited by: p1.
  22. [185] F. Rabe and Y. Sharoda (2019) Diagram combinators in MMT. In Intelligent computer mathematicsIntelligent Computer Mathematics, C. Kaliszyck, E. Brady, A. Kohlhase, C. Sacerdoti Coen, C. Kaliszyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI, Cham, pp. 211–226. External Links: ISBN 978-3-030-23250-4, Link Cited by: p1.
  23. [9] K. Berčič and J. Vidali (2018) DiscreteZOO: towards a fingerprint database of discrete objects. In Mathematical Software – ICMS 2018, pp. 36–44. External Links: Link, ISBN 978-3-319-96418-8 Cited by: p1.
  24. [94] A. Kohlhase (2018) Factors for reading mathematical expressions. In Proceedings of the conference ”lernen, wissen, daten, analysen”, LWDA, R. Gemulla, S. P. Ponzetto, C. Bizer, M. Keuper, and H. Stuckenschmidt (Eds.), CEUR Workshop Proceedings, Vol. 2191, pp. 195–202. External Links: Link Cited by: p1.
  25. [121] M. Kohlhase (2018) Towards context graphs for argumentation logics. In Proceedings of the conference ”lernen, wissen, daten, analysen”, LWDA, R. Gemulla, S. P. Ponzetto, C. Bizer, M. Keuper, and H. Stuckenschmidt (Eds.), CEUR Workshop Proceedings, Vol. 2191, pp. 203–214. External Links: Link Cited by: p1.
  26. [168] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  27. [181] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. In 24th International Workshop on Algebraic Development Techniques 2018, External Links: Link Cited by: p1.
  28. [203] J. F. Schaefer and M. Kohlhase (2018) Syntactic/semantic analysis for high-precision math linguistics. In Workshop papers at 11th conference on intelligent computer mathematics cicm 2018Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018, O. Hasan, A. Youssef, A. Naumowicz, W. Farmer, C. Kaliszyk, D. Gallois-Wong, F. Rabe, G. D. Reis, G. Passmore, J. Davenport, M. Pfeiffer, M. Kohlhase, S. Autexier, S. Tahar, T. Koprucki, U. Siddique, W. Neuper, W. Windsteiger, W. Schreiner, W. Sperber, and Z. Kovács (Eds.), Note: CICM Work in Progress Paper External Links: Link Cited by: p1.
  29. [120] M. Kohlhase (2017-10) Math object identifiers – towards research data in mathematics. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, A. Kohlhase and E. Kübler (Eds.), pp. 214–252. External Links: Link Cited by: p1.
  30. [214] G. Ucar and A. Kohlhase (2017-10) Irreführende mentale modelle beim smart-tv (misleading mental models for smart-tvs). In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, A. Kohlhase and E. Kübler (Eds.), pp. 200–212. External Links: Link Cited by: p1.
  31. [23] M. Codescu, T. Mossakowski, and F. Rabe (2017) Canonical Selection of Colimits. In Recent Trends in Algebraic Development Techniques, P. James and M. Roggenbach (Eds.), pp. 170–188. Cited by: p1.
  32. [93] A. Kohlhase (2017) Domain-dependant decoding of math expressions. In MathUI 2017: the 12th workshop on mathematical user interfacesMathUI 2017: The 12th Workshop on Mathematical User Interfaces, A. Kohlhase and M. Pollanen (Eds.), Cited by: p1.
  33. [152] G. Lisowski and M. Rapp (2017) Is the triviality of agm a serious possibility. In Logic in the Wild: 6th workshop in the ’Logic, Reasoning & Rationality’ series, External Links: Link Cited by: p1.
  34. [170] D. Müller, C. Rothgang, Y. Liu, and F. Rabe (2017) Alignment-based translations across formal systems using interface theories. In Fifth Workshop on Proof eXchange for Theorem Proving - PxTP 2017, External Links: Link Cited by: p1.
  35. [198] F. Rabe (2017) The MMT Perspective on Conservativity. In Logical and Semantic Frameworks, with Applications, S. Alves and R. Wassermann (Eds.), pp. 17–33. Cited by: p1.
  36. [201] M. Rupprecht, M. Kohlhase, and D. Müller (2017) A flexible, interactive theory-graph viewer. In MathUI 2017: the 12th workshop on mathematical user interfacesMathUI 2017: The 12th Workshop on Mathematical User Interfaces, A. Kohlhase and M. Pollanen (Eds.), External Links: Link Cited by: p1.
  37. [72] A. Kohlhase and M. Fürsich (2016-07) Understanding mathematical expressions: an eye-tracking study. In Mathematical user interfaces workshop at CICMMathematical User Interfaces Workshop, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  38. [213] I. Toloaca and M. Kohlhase (2016-07) Notation-based semantification. In Mathematical user interfaces workshop at CICMMathematical User Interfaces Workshop, A. Kohlhase and P. Libbrecht (Eds.), pp. 73–81. External Links: Link Cited by: p1.
  39. [4] A. Aizawa, M. Kohlhase, I. Ounis, and R. Zanibbi (2016) NTCIR-12 MathIR task overview. In Proceedings of the 12th ntcir conference on evaluation of information access technologiesProceedings of the 12th NTCIR Conference on Evaluation of Information Access Technologies, N. Kando, T. Sakai, and M. Sanderson (Eds.), pp. 299–308. External Links: Link Cited by: p1.
  40. [19] M. Codescu, T. Mossakowski, and F. Rabe (2016) Selecting Colimits for Parameterisation and Networks of Specifications. In Workshop on Algebraic Development Techniques, M. Roggenbach and P. James (Eds.), Cited by: p1.
  41. [64] C. Kaliszyk, F. Rabe, and G. Sutcliffe (2016) TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. In Workshop on Practical Aspects of Automated Reasoning, P. Fontaine, S. Schulz, and J. Urban (Eds.), pp. 41–55. Cited by: p1.
  42. [65] C. Kaliszyk, M. Kohlhase, D. Müller, and F. Rabe (2016) A standard for aligning mathematical concepts. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.), External Links: Link Cited by: p1.
  43. [92] A. Kohlhase (2016) Math web search interfaces and the generation gap of mathematicians. In Workshop Human-Computer Algebra Interaction, Kassel, Germany, External Links: Link Cited by: p1.
  44. [122] R. Kumar and F. Rabe (2016) Breakout session on A standard for system integration and proof interchange. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 94–94. Cited by: p1.
  45. [197] F. Rabe (2016) MMT: A UniFormal Approach to Knowledge Representation. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 88–88. Cited by: p1.
  46. [199] D. Rochau, M. Kohlhase, and D. Müller (2016) FrameIT reloaded: serious math games from modular math ontologies. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.), External Links: Link Cited by: p1.
  47. [44] R. Hambasan and M. Kohlhase (2015-10) Faceted search for mathematics. In Proceedings of the LWA 2015 workshops: KDML, FGWM, IR, and FGDBProceedings of the LWA 2015 Workshops: KDML, FGWM, IR, and FGDB, R. Bergmann, S. Görg, and G. Müller (Eds.), pp. 33–44. External Links: Link Cited by: p1.
  48. [153] E. Luzhnica, M. Iancu, and M. Kohlhase (2015-10) Importing the OEIS library into OMDoc. In Proceedings of the LWA 2015 workshops: KDML, FGWM, IR, and FGDBProceedings of the LWA 2015 Workshops: KDML, FGWM, IR, and FGDB, R. Bergmann, S. Görg, and G. Müller (Eds.), pp. 296–303. External Links: Link Cited by: p1.
  49. [40] D. Ginev, S. Lal, M. Kohlhase, and T. Wiesing (2015-07) KAT: an annotation tool for STEM documents. In Mathematical user interfaces workshop at CICMMathematical User Interfaces Workshop, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  50. [73] A. Kohlhase and A. Guseva (2015-07) Co-occurrences of context dimensions of spreadsheets. In Mathematical user interfaces workshop at CICMMathematical User Interfaces Workshop, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  51. [175] N. Pentrel and M. Kohlhase (2015-07) Relational presentations using semantic closeness spatial narrative for mathematical content. In Mathematical user interfaces workshop at CICMMathematical User Interfaces Workshop, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  52. [49] F. Horozal and F. Rabe (2015) Formal Logic Definitions for Interchange Languages. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 171–186. Cited by: p1.
  53. [75] A. Kohlhase, M. Kohlhase, and A. Guseva (2015) Context in spreadsheet comprehension. In Second workshop on software engineering methods in spreadsheetsSecond workshop on Software Engineering methods in Spreadsheets, External Links: Link Cited by: p1.
  54. [196] F. Rabe (2015) Generic Literals. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 102–117. Cited by: p1.
  55. [212] A. Toader, M. Kohlhase, and A. Kohlhase (2015) Assessment for spreadsheets. In Second workshop on software engineering methods in spreadsheetsSecond workshop on Software Engineering methods in Spreadsheets, External Links: Link Cited by: p1.
  56. [1] C. Acevedo and M. Kohlhase (2014) OpenMathMap: interaction. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  57. [3] A. Aizawa, M. Kohlhase, I. Ounis, and M. Schubotz (2014) NTCIR-11 Math-2 task overview. In NTCIR workshop 11 meetingNTCIR 11 Conference, N. Kando, H. Joho, and K. Kishida (Eds.), pp. 88–98. External Links: Link Cited by: p1.
  58. [15] J. Carette, W. Farmer, and M. Kohlhase (2014) Realms: a structure for consolidating knowledge about mathematical theories. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 252–266. Note: MKM Best-Paper-Award External Links: Link Cited by: p1.
  59. [41] D. Ginev, B. Miller, and S. Oprea (2014) E-books and graphics with ml. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 427–430. External Links: Link Cited by: p1.
  60. [43] R. Hambasan, M. Kohlhase, and C. Prodescu (2014) MathWebSearch at NTCIR-11. In NTCIR workshop 11 meetingNTCIR 11 Conference, N. Kando, H. Joho, and K. Kishida (Eds.), pp. 114–119. External Links: Link Cited by: p1.
  61. [52] F. Horozal, M. Kohlhase, and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  62. [57] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  63. [63] C. Jucovschi (2014) Towards an interaction-based integration of MKM services into end-user applications. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 344–356. External Links: Link Cited by: p1.
  64. [66] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 357–372. External Links: Link Cited by: p1.
  65. [82] A. Kohlhase and A. Toader (2014) FEncy: spreadsheet formulae exploration. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  66. [89] A. Kohlhase (2014) Design of search interfaces for mathematicians. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  67. [90] A. Kohlhase (2014) Math web search interfaces and the generation gap of mathematicians. In Mathematical software - ICMS 2014 - 4th international congressMathematical Software - ICMS 2014 - 4th International Congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 586–593. External Links: Document Cited by: p1.
  68. [91] A. Kohlhase (2014) Search interfaces for mathematicians. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 153–168. External Links: Link Cited by: p1.
  69. [95] L. Kohlhase and M. Kohlhase (2014) System description: a semantics-aware -to-office converter. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 440–443. External Links: Link Cited by: p1.
  70. [117] M. Kohlhase (2014) A data model and encoding for a semantic, multilingual terminology of mathematics. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 169–183. External Links: Link Cited by: p1.
  71. [118] M. Kohlhase (2014) Extension proposal: records in pragmatic OpenMath. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  72. [119] M. Kohlhase (2014) OpenMath language extensions. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2014MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, M. England, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. P. Sexton, P. Sojka, J. Urban, and S. M. Watt (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  73. [154] T. Mossakowski, M. Codescu, O. Kutz, C. Lange, and M. Grüninger (2014) Proof support for Common Logic. In Automated Reasoning in Quantified Non-Classical Logics (ARQNL), C. Benzmüller and J. Otten (Eds.), EasyChair Proceedings in Computing, pp. 42–58. External Links: Link Cited by: p1.
  74. [193] F. Rabe (2014) A Logic-Independent IDE. In Workshop on user interfaces for theorem proversWorkshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Link Cited by: p1.
  75. [194] F. Rabe (2014) A Logic-Independent IDE. In Workshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Document Cited by: p1.
  76. [195] F. Rabe (2014) MMT Objects. In Workshops and Work in Progress at CICM 2014: OpenMath Workshop, M. England, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. Sexton, P. Sojka, J. Urban, and S. Watt (Eds.), Cited by: p1.
  77. [47] A. Henrich and H. Sperker (Eds.) (2013-10) Wissens- und erfahrungsmanagement LWA (lernen, wissensentdeckung und adaptivität) conference proceedings. Universität Bamberg. Cited by: 81.
  78. [81] A. Kohlhase and A. Toader (2013-10) Exploration of spreadsheet formulae with fency. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, A. Kohlhase and B. Rieger (Eds.), External Links: Link Cited by: p1.
  79. [5] A. Aizawa, M. Kohlhase, and I. Ounis (2013) NTCIR-10 Math pilot task overview. In NTCIR workshop 10 meetingNTCIR Workshop 10 Meeting, N. Kando and K. Kishida (Eds.), pp. 1–8. External Links: Link Cited by: p1.
  80. [13] T. Breitsprecher, M. Codescu, C. Jucovschi, M. Kohlhase, L. Schröder, and S. Wartzack (2013) Semantic support for engineering design processes. In Proc. 13th International Design Conference, DESIGN 2014, External Links: Link Cited by: p1.
  81. [31] J. W. Dörrie, M. Kohlhase, and L. Linsen (2013) OpenMathMap: accessing math via interactive maps. In Contemporary Issues in Mathematical Publishing, JMM San Diego Special Session, K. Kaiser, S. Krantz, and B. Wegner (Eds.), pp. 81–98. External Links: Link Cited by: p1.
  82. [32] J. W. Dörrie and M. Kohlhase (2013) OpenMathMap: accessing math via interactive maps. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2013MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  83. [58] M. Iancu, F. Mance, and F. Rabe (2013) The Scala-REPL + MMT as a lightweight mathematical user interface. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2013MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  84. [71] M. Kerber, C. Lange, and C. Rowat (2013) Automated reasoning for economics. In 20th Automated Reasoning Workshop (ARW), A. Bolotov, S. Colton, D. Crocker, L. Dennis, C. Dixon, J. Fleuriot, U. Hustadt, M. Jamnik, K. Komendantskaya, A. Miller, R. Schmidt, V. Sorge, and J. Heras (Eds.), Note: Invited paper Cited by: p1.
  85. [88] A. Kohlhase (2013) Spreadsheets: from data interfaces to knowledge interfaces. In Joint proceedings of the MathUI, OpenMath, PLMMS, and ThEdu workshops and work in progress at the conference on intelligent computer mathematics 2013MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, C. Lange, D. Aspinall, J. Carette, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  86. [105] M. Kohlhase, C. Prodescu, and C. Liguda (2013) XLSearch: a search engine for spreadsheets. In Symp. of the european spreadsheet risks interest group (EuSpRIG 2013)Symp. of the European Spreadsheet Risks Interest Group (EuSpRIG 2013), External Links: Link Cited by: p1.
  87. [106] M. Kohlhase and C. Prodescu (2013) MathWebSearch at NTCIR-10. In NTCIR workshop 10 meetingNTCIR Workshop 10 Meeting, N. Kando and K. Kishida (Eds.), pp. 675–679. External Links: Link Cited by: p1.
  88. [115] M. Kohlhase (2013) Knowledge management for systematic engineering design in CAD systems. In Professionelles Wissenmanagement Management, Konferenzbeiträge der 7. KonferenzProfessionelles Wissenmanagement Management, Konferenzbeiträge der 7. Konferenz, F. Lehner, N. Amende, and N. Fteimi (Eds.), pp. 202–217. External Links: Link Cited by: p1.
  89. [116] M. Kohlhase (2013) The flexiformalist manifesto. In International workshop on symbolic and numeric algorithms for scientific computing (SYNASC 2012)14th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), A. Voronkov, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. M. Watt, and D. Zaharie (Eds.), pp. 30–36. External Links: Link Cited by: p1.
  90. [126] C. Lange, M. B. Caminati, M. Kerber, T. Mossakowski, C. Rowat, M. Wenzel, and W. Windsteiger (2013) A qualitative comparison of the suitability of four theorem provers for basic auction theory. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 200–215. External Links: 1303.4193 Cited by: p1.
  91. [139] C. Lange, C. Rowat, and M. Kerber (2013) The formare project – formal mathematical reasoning in economics. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.), Lecture Notes in Computer Science, pp. 330–334. External Links: 1303.4194 Cited by: p1.
  92. [140] C. Lange, C. Rowat, W. Windsteiger, and M. Kerber (2013) Developing an auction theory toolbox. In Enabling domain experts to use formalised reasoningEnabling Domain Experts to use Formalised Reasoning, C. Lange, C. Rowat, and M. Kerber (Eds.), Cited by: p1.
  93. [155] T. Mossakowski, O. Kutz, M. Codescu, and C. Lange (2013) The distributed ontology, modeling and specification language. In Modular Ontologies, C. Del Vescovo, T. Hahmann, D. Pearce, and D. Walther (Eds.), CEUR Workshop Proceedings, Aachen. Note: Invited paper External Links: ISSN 1613-0073, Link Cited by: p1.
  94. [157] T. Mossakowski, O. Kutz, and C. Lange (2013) Semantics of the distributed ontology language: institutes and institutions. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, T. Mossakowski, N. Martí-Oliet, and M. Palomino Tarjuelo (Eds.), LNCS, pp. 212–230. Cited by: p1.
  95. [87] A. Kohlhase (2012-06) Navigation in mathematical documents. In Mathematical user-interfaces workshop 2012 at CICMMathematical User Interfaces Workshop 2012, P. Libbrecht (Ed.), pp. 12–23. External Links: Link Cited by: p1.
  96. [20] M. Codescu, F. Horozal, I. Ignatov, and F. Rabe (2012) Representing CASL in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
  97. [22] M. Codescu, F. Horozal, T. Mossakowski, and F. Rabe (2012) Compiling Logics. In Workshop on Algebraic Development Techniques, Cited by: p1.
  98. [53] F. Horozal and F. Rabe (2012) Representing Categories of Theories in a Proof-Theoretical Logical Framework. In Workshop on Algebraic Development Techniques, Cited by: p1.
  99. [59] M. Iancu and F. Rabe (2012) (Work-in-Progress) An MMT-Based User-Interface. In Workshop on User Interfaces for Theorem Provers, C. Kaliszyk and C. Lüth (Eds.), Cited by: p1.
  100. [60] M. Iancu and F. Rabe (2012) Management of Change in Declarative Languages. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 325–340. Cited by: p1.
  101. [62] C. Jucovschi (2012) Cost-effective integration of mkm semantic services into editing environments. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 96–110. External Links: Link Cited by: p1.
  102. [70] M. Kerber, C. Lange, and C. Rowat (2012) Formal representation and proof for cooperative games. In Symposium on Mathematical Practice and Cognition II, A. Pease and B. Larvor (Eds.), pp. 15–18. External Links: Link, ISBN 978-1-908187-10-9 Cited by: p1.
  103. [98] M. Kohlhase and M. Iancu (2012) Searching the space of mathematical knowledge. In DML and MIR 2012DML and MIR 2012, P. Sojka and M. Kohlhase (Eds.), External Links: Link Cited by: p1.
  104. [123] O. Kutz, C. Lange, T. Mossakowski, C. M. Keet, F. Neuhaus, and M. Grüninger (2012) The Babel of the semantic web tongues – in search of the Rosetta stone of interoperability. In What will the Semantic Web look like 10 Years from now? Workshop at ISWC, F. van Harmelen, J. A. Hendler, P. Hitzler, K. Janowicz, and D. Vrandečić (Eds.), External Links: Link Cited by: p1.
  105. [134] C. Lange, O. Kutz, T. Mossakowski, and M. Grüninger (2012) The distributed ontology language (DOL): ontology integration and interoperability applied to mathematical formalization. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 463–467. External Links: 1204.5093 Cited by: p1.
  106. [137] C. Lange, T. Mossakowski, O. Kutz, C. Galinski, M. Grüninger, and D. Couto Vale (2012) The Distributed Ontology Language (DOL): use cases, syntax, and extensibility. In Terminology and knowledge engineering conference (TKE)Terminology and Knowledge Engineering Conference (TKE), G. Aguado de Cea, M. C. Suárez-Figueroa, R. García-Castro, and E. Montiel-Ponsoda (Eds.), pp. 33–48. External Links: 1208.0293 Cited by: p1.
  107. [138] C. Lange, T. Mossakowski, and O. Kutz (2012) LoLa: a modular ontology of logics, languages, and translations. In Modular Ontologies, T. Schneider and D. Walther (Eds.), CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  108. [156] T. Mossakowski, O. Kutz, and C. Lange (2012) cMap’s product classification mapping from an ontology interoperability perspective. In Mapping of classifications and other light-weight ontologies, A. Virgili and others (Eds.), Cited by: p1.
  109. [186] F. Rabe and K. Sojakova (2012) Mechanically Verifying Logic Translations. In Workshop on Algebraic Development Techniques, Cited by: p1.
  110. [192] F. Rabe (2012) A Query Language for Formal Mathematical Libraries. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 142–157. External Links: 1204.4685 Cited by: p1.
  111. [211] C. Tankink, C. Lange, and J. Urban (2012) Point-and-write — documenting formal mathematics by reference. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge (Eds.), LNAI, pp. 169–185. External Links: 1204.5094 Cited by: p1.
  112. [136] C. Lange, T. Mossakowski, C. Galinski, and O. Kutz (2011-11) Making heterogeneous ontologies interoperable through standardisation. In Accessibility Reaching Everywhere, pp. 185–196. External Links: Link Cited by: p1.
  113. [176] C. C. Prodescu and M. Kohlhase (2011-09) MathWebSearch 0.5 - open formula search engine. In Wissens- und erfahrungsmanagement LWA (lernen, wissensentdeckung und adaptivität) conference proceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, External Links: Link Cited by: p1.
  114. [124] O. Kutz, T. Mossakowski, C. Galinski, and C. Lange (2011-06) Towards a standard for heterogeneous ontology integration and interoperability. In First International Conference on Terminology, Language and Content Resources (LaRC), K. Choi and others (Eds.), pp. 101–110. External Links: Link Cited by: p1.
  115. [17] M. Cîrlănaru, D. Ginev, and C. Lange (2011) Authoring and publishing of units and quantities in semantic documents. In Proceedings of the 1st workshop on semantic publication, Extended Semantic Web Conference1st Workshop on Semantic Publication (SePublica), A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  116. [21] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, F. Rabe, and K. Sojakova (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development TechniquesRecent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  117. [27] C. David, D. Ginev, M. Kohlhase, B. Matican, and S. Mirea (2011) A framework for modular semantic publishing with separate compilation and dynamic linking. In Proceedings of the 1st workshop on semantic publication, Extended Semantic Web Conference1st Workshop on Semantic Publication (SePublica), A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  118. [35] A. Dumitrache and C. Lange (2011) BauDenkMalNetz – creating a semantically annotated web resource of historical buildings. In Proceedings of the 1st workshop on semantic publication, Extended Semantic Web Conference1st Workshop on Semantic Publication (SePublica), A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  119. [51] F. Horozal, M. Kohlhase, and F. Rabe (2011) Extending OpenMath with Sequences. In Intelligent computer mathematicsIntelligent Computer Mathematics, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
  120. [74] A. Kohlhase and C. Jucovschi (2011) planMP: collecting mathematical practices for mkm. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.), Cited by: p1.
  121. [79] A. Kohlhase and M. Kohlhase (2011) Towards a flexible notion of document context. In Proceedings of the 29th annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29th annual ACM international conference on Design of communication (SIGDOC), pp. 181–188. External Links: Link Cited by: p1.
  122. [217] M. Wolska, M. Grigore, and M. Kohlhase (2011) Using discourse context to interpret object-denoting mathematical expressions. In Towards digital mathematics library, dml workshopTowards Digital Mathematics Library, DML workshop, P. Sojka (Ed.), pp. 85–101. External Links: Link Cited by: p1.
  123. [151] C. Lange (2010-07) Towards OpenMath content dictionaries as linked data. In 23rd OpenMath workshop23rd OpenMath Workshop, M. Kohlhase and C. Lange (Eds.), External Links: 1006.4057v1 Cited by: p1.
  124. [29] C. David, M. Kohlhase, C. Lange, F. Rabe, and V. Zholudev (2010-06) JOBAD/MMT – interactive mathematics. In AI Mashup ChallengeAI Mashup Challenge at ESWC, A. Giurca, B. Endres-Niggemeyer, C. Lange, L. Maicher, and P. Hitzler (Eds.), External Links: Link Cited by: p1.
  125. [7] S. Autexier and N. Müller (2010) Semantics-based change impact analysis for heterogeneous collections of documents. In Proceedings of the 10th ACM symposium on document engineeringProceedings of the 10th ACM symposium on Document engineering, M. Gormish and R. Ingold (Eds.), DocEng ’10, pp. 97–106. External Links: Link, Document Cited by: p1.
  126. [26] C. David, D. Ginev, M. Kohlhase, and J. Corneli (2010) eMath 3.0: building blocks for a social and semantic web for online mathematics & ELearning. In 1st International Workshop on Mathematics and ICT: Education, Research and Applications1st International Workshop on Mathematics and ICT: Education, Research and Applications, I. Mierlus-Mazilu (Ed.), External Links: Link Cited by: p1.
  127. [28] C. David, M. Kohlhase, C. Lange, F. Rabe, N. Zhiltsov, and V. Zholudev (2010) Publishing math lecture notes as linked data. In The semantic web: research and applications (part II)The Semantic Web: Research and Applications (Part II), L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, and T. Tudorache (Eds.), LNCS, pp. 370–375. External Links: 1004.3390v1 Cited by: p1.
  128. [30] C. David, C. Lange, and F. Rabe (2010) Interactive documents as interfaces to computer algebra systems: JOBAD and Wolfram—Alpha. In CALCULEMUS (emerging trends)CALCULEMUS (Emerging Trends), D. Delahaye and R. Rioboo (Eds.), pp. 13–30. External Links: Link Cited by: p1.
  129. [34] A. Dumitrache, C. Lange, M. Kohlhase, and N. Aschenbeck (2010) Prototyping a browser for a listed buildings database with Semantic MediaWiki. In Proceedings of the 5th workshop on semantic wikis, Extended Semantic Web Conference5th Workshop on Semantic Wikis, C. Lange, J. Reutelshöfer, S. Schaffert, and H. Skaf-Molli (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  130. [37] I. Farhana Md Mahtar and N. Azan Mat Zin (2010) Mathematical knowledge representation for education semantic web based on learning style. In International Symposium in Information Technology (ITSim), pp. 1–4. External Links: Document Cited by: p1.
  131. [61] M. José Ibáñez, G. Vulcu, J. Ezpeleta, and S. Bhiri (2010) Semantically enabled business process discovery. In Symposium on Applied Computing, pp. 1396–1403. External Links: ISBN 978-1-60558-639-7 Cited by: p1.
  132. [76] A. Kohlhase, M. Kohlhase, and C. Lange (2010) Dimensions of formality: a case study for MKM in software engineering. In Intelligent computer mathematicsIntelligent Computer Mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton (Eds.), LNAI, pp. 355–369. External Links: 1004.5071v1 Cited by: p1.
  133. [141] C. Lange and V. Zholudev (2010) Previewing OWL changes and refactorings using a flexible XML database. In Proceedings of the 1st workshop on ontology repositories and editors, Extended Semantic Web Conference1st Workshop on Ontology Repositories and Editors, M. d’Aquin, A. García Castro, C. Lange, and K. Viljanen (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  134. [150] C. Lange (2010) Integrating mathematics into the web of data. In Linked Data in the Future Internet, S. Auer, S. Decker, and M. Hauswirth (Eds.), CEUR Workshop Proceedings, Aachen. External Links: ISSN 1613-0073, Link Cited by: p1.
  135. [191] F. Rabe (2010) Representing Isabelle in LF. In Logical Frameworks and Meta-languages: Theory and Practice, K. Crary and M. Miculan (Eds.), Electronic Proceedings in Theoretical Computer Science, Vol. 34, pp. 85–100. Cited by: p1.
  136. [215] D. Vrandečić, C. Lange, M. Hausenblas, J. Bao, and L. Ding (2010) Semantics of governmental statistics data. In Proceedings of WebSci’10: Extending the Frontiers of Society On-LineProceedings of WebSci’10: Extending the Frontiers of Society On-Line, External Links: Link Cited by: p1.
  137. [218] M. Wolska and M. Grigore (2010) Symbol declarations in mathematical writing: a corpus study. In Towards digital mathematics library, dml workshopTowards Digital Mathematics Library, DML workshop, P. Sojka (Ed.), pp. 119–127. External Links: Link Cited by: p1.
  138. [219] V. Zholudev, M. Kohlhase, and F. Rabe (2010) A [insert xml format] database for [insert cool application]. In Proceedings of XML Prague 2010Proceedings of XML Prague 2010, External Links: Link Cited by: p1.
  139. [42] M. Grigore, M. Wolska, and M. Kohlhase (2009-12-14) Towards context-based disambiguation of mathematical expressions. In The Joint Conference of ASCM 2009 and MACIS 2009: Asian Symposium on Computer Mathematics and Mathematical Aspects of Computer and Information Sciences, M. Suzuki, H. Hong, H. Anai, C. Yap, Y. Sato, and H. Yoshida (Eds.), COE Lecture Notes, Vol. 22, Fukuoka, Japan, pp. 262–271. External Links: ISSN 1881-4042, Link Cited by: p1.
  140. [46] M. Hartmann and F. Janssen (2009-09) LWA 2009; Workshop-Woche: Lernen – Wissen – Adaptivität. Technical report Vol. TUD-KE-2009-04, Universität Darmstadt. Cited by: 78, 132, 220.
  141. [78] A. Kohlhase and M. Kohlhase (2009-09) What you get is what you understand: assessment in SACHS. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, C. Lange and J. Reutelshöfer (Eds.), pp. 22–29. External Links: Link Cited by: p1.
  142. [97] M. Kohlhase, J. Gičeva, C. Lange, and V. Zholudev (2009-09) JOBAD – interactive mathematical documents. In AI Mashup ChallengeAI Mashup Challenge at KI Conference, B. Endres-Niggemeyer, V. Zacharias, and P. Hitzler (Eds.), External Links: Link Cited by: p1.
  143. [132] C. Lange and M. Kohlhase (2009-09) A mathematical approach to ontology authoring and documentation. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, C. Lange and J. Reutelshöfer (Eds.), Cited by: p1.
  144. [220] V. Zholudev (2009-09) The TNTBase System and Validation of XML Documents. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWMWissens- und Erfahrungsmanagement (Knowledge and Experience Management), FGWM, C. Lange and J. Reutelshöfer (Eds.), pp. 57–63. External Links: Link Cited by: p1.
  145. [14] C. Calude and C. Müller (2009-07) Formal Proofs: Reconciling Correctness and Understanding. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI. Cited by: p1.
  146. [24] J. H. Davenport and M. Kohlhase (2009-07) Quantifiers and big operators in OpenMath. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  147. [38] J. Gičeva, C. Lange, and F. Rabe (2009-07) Integrating web services into active mathematical documents. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 279–293. External Links: Link Cited by: p1.
  148. [108] M. Kohlhase and F. Rabe (2009-07) Semantics of OpenMath and MathML3. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  149. [131] C. Lange and M. Kohlhase (2009-07) A mathematical approach to ontology authoring and documentation. In MKM/Calculemus proceedingsMKM/Calculemus Proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt (Eds.), LNAI, pp. 389–404. External Links: Link Cited by: p1.
  150. [149] C. Lange (2009-07) wiki.openmath.org – how it works, how you can participate. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: 1003.5192v1 Cited by: p1.
  151. [180] F. Rabe and M. Kohlhase (2009-07) A better role system for OpenMath. In 22nd openmath workshop22nd OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  152. [133] C. Lange and M. Kohlhase (2009-06) Documenting ontologies the mathematical way. In Poster Proceedings of the 6th European Semantic Web Conference (ESWC), External Links: Link Cited by: p1.
  153. [148] C. Lange (2009-05) Krextor – an extensible XML→RDF extraction framework. In Scripting and development for the semantic web (SFSW)Scripting and Development for the Semantic Web (SFSW), C. Bizer, S. Auer, and G. A. Grimnes (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  154. [25] C. David, C. Brennan, O. Ormond, and M. Mullen (2009) Parallelised em wave propagation modelling for accurate network simulation. In 9th IT&T Conference, Dublin Institute of Technology, Cited by: p1.
  155. [33] S. Dumbrava, F. Horozal, and K. Sojakova (2009) A Case Study on Formalizing Algebra in a Module System. In Workshop on Modules and Libraries for Proof Assistants, F. Rabe and C. Schürmann (Eds.), ACM International Conference Proceeding Series, Vol. 429, pp. 11–18. Cited by: p1.
  156. [39] D. Ginev, C. Jucovschi, S. Anca, M. Grigore, C. David, and M. Kohlhase (2009) An architecture for linguistic and semantic analysis on the arXMLiv corpus. In Applications of Semantic Technologies (AST) Workshop at Informatik 2009, External Links: Link Cited by: p1.
  157. [48] F. Horozal and F. Rabe (2009) Representing Model Theory in a Type-Theoretical Logical Framework. In Fourth Workshop on Logical and Semantic Frameworks, with Applications, M. Ayala-Rincón and F. Kamareddine (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 256, pp. 49–65. Cited by: p1.
  158. [165] C. Müller (2009) Communities of Practice & Semantic Web: Stimulating Collaboration by Document Markup. In Proceedings of the United International Systems Conference (UNISCON) LNBIP 20, J. Yang and others (Eds.), pp. 432–437. External Links: Link Cited by: p1.
  159. [166] C. Müller (2009) Communities of Practice & Semantic Web: Stimulating Collaboration by Document Markup. In UNISCON 2009 Supplementary Proceedings: Doctoral Consortium Papers, pp. 1–8. External Links: Link Cited by: p1.
  160. [184] F. Rabe and C. Schürmann (2009) A Practical Module System for LF. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), J. Cheney and A. Felty (Eds.), ACM International Conference Proceeding Series, Vol. LFMTP’09, pp. 40–48. Cited by: p1.
  161. [190] F. Rabe (2009) Representing Logics and Logic Translations. In Ausgezeichnete Informatikdissertationen 2008, D. Wagner et al. (Ed.), Lecture Notes in Informatics, Vol. D-9, pp. 201–210. Note: English title: Outstanding Dissertations in Computer Science 2008 Cited by: p1.
  162. [210] H. Stamerjohanns, D. Ginev, C. David, D. Misev, V. Zamdzhiev, and M. Kohlhase (2009) MathML-aware article conversion from , a comparison study. In Towards digital mathematics library, dml 2009 workshopTowards Digital Mathematics Library, DML 2009 workshop, P. Sojka (Ed.), pp. 109–120. External Links: Link Cited by: p1.
  163. [77] A. Kohlhase and M. Kohlhase (2008-10) Compensating the semantic bias of spreadsheets. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference ProceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, J. Baumeister and M. Atzmüller (Eds.), Vol. 448. External Links: Link Cited by: p1.
  164. [128] C. Lange, T. Hastrup, and S. Corlosquet (2008-10) Arguing on issues with mathematical knowledge items in a semantic wiki. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference ProceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, J. Baumeister and M. Atzmüller (Eds.), Vol. 448. Cited by: p1.
  165. [163] C. Müller (2008-10) Towards CoPing with Information Overload. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference ProceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, J. Baumeister and M. Atzmüller (Eds.), Vol. 448. Cited by: p1.
  166. [164] C. Müller (2008-10) Towards the Adaptation of Scientific Course Material powered by Community of Practice. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference ProceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, J. Baumeister and M. Atzmüller (Eds.), Vol. 448. Cited by: p1.
  167. [171] N. Müller and M. Kohlhase (2008-10) Fine-Granular Version Control & Redundancy Resolution. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference ProceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) Conference Proceedings, J. Baumeister and M. Atzmüller (Eds.), Vol. 448. Note: http://www.kwarc.info/nmueller/papers/lwa08-fst.pdf External Links: Link Cited by: p1.
  168. [127] C. Lange and A. González Palomo (2008-07) Easily editing and browsing complex OpenMath markup with SWiM. In Mathematical user interfaces workshop at MKMMathematical User Interfaces Workshop, P. Libbrecht (Ed.), External Links: Link Cited by: p1.
  169. [129] C. Lange, T. Hastrup, and S. Corlosquet (2008-06) Improving mathematical knowledge items by acting on issue-based community feedback. In 2nd workshop on scientific communities of practice (SCooP-2008)Proceedings of the 2nd SCooP Workshop, C. Müller (Ed.), Cited by: p1.
  170. [160] C. Müller and M. Kohlhase (2008-06) Towards A Community of Practice Toolkit. In 2nd workshop on scientific communities of practice (SCooP-2008)Proceedings of the 2nd SCooP Workshop, C. Müller (Ed.), Cited by: p1.
  171. [145] C. Lange (2008-02) Editing OpenMath content dictionaries with SWiM. In 3rd JEM Workshop (Joining Educational Mathematics), External Links: Link Cited by: p1.
  172. [8] C. Benzmüller, F. Rabe, and G. Sutcliffe (2008) THF0 – The core of the TPTP Language for Higher-Order Logic. In 4th International Joint Conference on Automated Reasoning, A. Armando, P. Baumgartner, and G. Dowek (Eds.), LNCS, pp. 491–506. Cited by: p1.
  173. [125] C. Lange, U. Bojārs, T. Groza, J. Breslin, and S. Handschuh (2008) Expressing argumentative discussions in social media sites. In Social data on the web (SDoW), workshop at the 7th international semantic web conferenceSocial Data on the Web (SDoW), Workshop at the 7th International Semantic Web Conference, J. Breslin, U. Bojārs, A. Passant, and S. Fernández (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  174. [135] C. Lange, S. McLaughlin, and F. Rabe (2008) Flyspeck in a semantic wiki – collaborating on a large scale formalization of the Kepler conjecture. In Proceedings of the 3rd workshop on semantic wikis, European Semantic Web Conference3rd Workshop on Semantic Wikis, C. Lange, S. Schaffert, H. Skaf-Molli, and M. Völkel (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  175. [146] C. Lange (2008) Mathematical semantic markup in a wiki: the roles of symbols and notations. In Proceedings of the 3rd workshop on semantic wikis, European Semantic Web Conference3rd Workshop on Semantic Wikis, C. Lange, S. Schaffert, H. Skaf-Molli, and M. Völkel (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  176. [147] C. Lange (2008) SWiM – a semantic wiki for mathematical knowledge management. In The semantic web: research and applicationsThe Semantic Web: Research and Applications, S. Bechhofer, M. Hauswirth, J. Hoffmann, and M. Koubarakis (Eds.), LNCS, pp. 832–837. External Links: 1003.5196v1 Cited by: p1.
  177. [159] C. Müller and M. Kohlhase (2008) Communities of practice in mathematical elearning. In In proceedings of the Workshop in Mathematical and Scientific eContent, pp. 34–35. Cited by: p1.
  178. [178] F. Rabe and M. Kohlhase (2008) An exchange format for modular knowledge. In Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz (Eds.), CEUR Workshop Proceedings, Aachen, pp. 50–68. External Links: ISSN 1613-0073 Cited by: p1.
  179. [179] F. Rabe and M. Kohlhase (2008) An Exchange Format for Modular Knowledge. In Proceedings of the LPAR Workshops on Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz (Eds.), CEUR Workshop Proceedings, Vol. 418, pp. 50–68. Cited by: p1.
  180. [101] M. Kohlhase, C. Lange, and F. Rabe (2007-06) Presenting mathematical content with flexible elisions. In OpenMath/JEM workshop 2007OpenMath/JEM Workshop 2007, O. Caprotti, M. Kohlhase, and P. Libbrecht (Eds.), Cited by: p1.
  181. [104] M. Kohlhase, C. Müller, and N. Müller (2007-06) Documents with flexible notation contexts as interfaces to mathematical knowledge. In Mathematical user-interfaces workshop 2007 at MKMMathematical User Interfaces Workshop 2007, P. Libbrecht (Ed.), Cited by: p1.
  182. [142] C. Lange (2007-06) SWiM – a semantic wiki for mathematical knowledge management. In Mathematical user-interfaces workshop 2007 at MKMMathematical User Interfaces Workshop 2007, P. Libbrecht (Ed.), Cited by: p1.
  183. [144] C. Lange (2007-06) Towards scientific collaboration in a semantic wiki. In Bridging the Gap between Semantic Web and Web 2.0 (SemNet)Bridging the Gap between Semantic Web and Web 2.0 (SemNet), A. Hotho and B. Hoser (Eds.), Cited by: p1.
  184. [50] F. F. Horozal and C. E. Brown (2007) Formal representation of mathematics in a dependently typed set theory. In MKM/CalculemusTowards Mechanized Mathematical Assistants. MKM/Calculemus, M. Kauers, M. Kerber, R. Miner, and W. Windsteiger (Eds.), LNAI, pp. 265–279. Cited by: p1.
  185. [86] A. Kohlhase (2007) CPoint — ein invasiver, semantischer Editor für Content in MS PowerPoint. In EduMediaOffene Bildung im/mit dem Web 2.0!?!, V. Hornung-Prähauser (Ed.), pp. 116–118. Cited by: p1.
  186. [102] M. Kohlhase, A. Mahnke, and C. Müller (2007) Managing variants in document content and narrative structures. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, A. Hinneburg (Ed.), pp. 324–229. Cited by: p1.
  187. [143] C. Lange (2007) Towards a Semantic Wiki for Science. In Proceedings of the KWEPSY (Knowledge Web PhD Symposium)Proceedings of the KWEPSY (Knowledge Web PhD Symposium), E. Simperl, J. Diederich, and G. Schreiber (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  188. [158] C. Müller and M. Kohlhase (2007) Panta rhei. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, A. Hinneburg (Ed.), pp. 318–323. Cited by: p1.
  189. [161] C. Müller (2007) Presentation on Modeling Scientific Communities of Practice based on Semantic Markup of Scientific Documents and Web2.0. Technologies. In 7. konferenz für interaktive und kooperative medienMensch und Computer 2007, T. Gross (Ed.), Cited by: p1.
  190. [162] C. Müller (2007) Towards the Identification and Support of Scientific Communities of Practice. In 1st Workshop on Scientific COmmunities Of PracticeProceedings of the 1st SCooP Workshop, C. Müller (Ed.), Cited by: p1.
  191. [172] N. Müller and M. Wagner (2007) Towards Improving Interactive Mathematical Authoring by Ontology-driven Management of Change. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedingsWissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, A. Hinneburg (Ed.), pp. 289–295. Note: https://kwarc.info/nmueller/papers/lwa07.pdf External Links: Link Cited by: p1.
  192. [189] F. Rabe (2007) OMDoc Theory Graphs Revisited. In Proceedings of the OpenMath/JEM workshop, Cited by: p1.
  193. [216] M. Wagner and C. Müller (2007) Towards Community of Practice Support for Interactive Mathematical Authoring. In 1st Workshop on Scientific COmmunities Of PracticeProceedings of the 1st SCooP Workshop, C. Müller (Ed.), Cited by: p1.
  194. [84] A. Kohlhase (2006) CPoint – ein invasiver, semantischer Editor für wiederverwendaren Content in MS PowerPoint. In Proceedings der Pre-Conference Workshops der 4.e-Learning Fachtagung Informatik DeLFI 2006Proceedings der Pre-Conference Workshops der 4.e-Learning Fachtagung Informatik DeLFI 2006, C. Rensing (Ed.), pp. 35–42. Cited by: p1.
  195. [85] A. Kohlhase (2006) The User as Prisoner: How the Dilemma Might Dissolve. In 2nd Workshop on Learner Oriented Knowledge Management & KM Oriented e-Learning2nd Workshop on Learner Oriented Knowledge Management & KM Oriented e-Learning, M. Memmel, E. Ras, and S. Weibelzahl (Eds.), pp. 26–31. External Links: Link Cited by: p1.
  196. [130] C. Lange and M. Kohlhase (2006) A semantic wiki for mathematical knowledge management. In Proceedings of the 1st workshop on semantic wikis, European Semantic Web Conference1st Workshop on Semantic Wikis, M. Völkel, S. Schaffert, and S. Decker (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  197. [173] N. Müller (2006) An Ontology-Driven Management of Change. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, Universität Hildesheim, pp. 186–193. Note: https://kwarc.info/nmueller/papers/lwa06.pdf External Links: Link Cited by: p1.
  198. [187] F. Rabe (2006) First-Order Logic with Dependent Types. In Automated reasoning — third international joint conference, ijcar 2006Automated Reasoning — Third International Joint Conference, IJCAR 2006, U. Furbach and N. Shankar (Eds.), LNAI, pp. 377–391. Cited by: p1.
  199. [188] F. Rabe (2006) Towards Determining the Subset Relation between Propositional Modal Logics. In Proceedings of the FLoC 06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, G. Sutcliffe, R. Schmidt, and S. Schulz (Eds.), CEUR Workshop Proceedings, Aachen, pp. 126–140. External Links: ISSN 1613-0073 Cited by: p1.
  200. [183] F. Rabe, S. Schlager, and P. Schmitt (2005) A Sequent Calculus for a First-order Dynamic Logic with Trace Modalities for Promela+. In Short Paper Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, G. Sutcliffe and A. Voronkov (Eds.), pp. 21–27. Cited by: p1.
  201. [206] Y. Shirota (2005) Metadata for web-based mathematical learning materials. In Proceedings of the Data Engineering Workshop DEWS, External Links: Link Cited by: p1.
  202. [83] A. Kohlhase (2004) CPoint’s mathematical user interface. In Mathematical user interfaces workshop 2004Mathematical User Interfaces, P. Libbrecht (Ed.), External Links: Link Cited by: p1.
  203. [114] M. Kohlhase (2004) Semantic markup for /. In Mathematical user interfaces workshop 2004Mathematical User Interfaces, P. Libbrecht (Ed.), Cited by: p1.
  204. [18] E. Clarke, M. Kohlhase, J. Ouaknine, and K. Sutner (2003) Resurrecting the Analytica theorem prover. In First qpq workshop on deductive software componentsFirst QPQ Workshop on Deductive Software Components, Cited by: p1.
  205. [45] B. Han and M. Kohlhase (2003) A time calculus for natural language. In ICoS-4. inference in computational semantics. workshop proceedingsProceedings of Inference in Computational Semantics ICoS-4, P. Blackburn and J. Bos (Eds.), pp. 113–127. External Links: Link Cited by: p1.
  206. [113] M. Kohlhase (2003) Applying unification techniques to XML document management?. In 17th workshop on unification17th Workshop on Unification, Cited by: p1.
  207. [111] M. Kohlhase, K. Sutner, P. Jansen, A. Kohlhase, P. Lee, D. Scott, and M. Szudzik (2002) Acquisition of math content in an academic setting. In Second international conference on mathml and technologies for math on the webSecond International Conference on MathML and Technologies for Math on the Web, External Links: Link Cited by: p1.
  208. [221] J. Zimmer and M. Kohlhase (2002) System Description: The MathWeb software bus for distributed mathematical reasoning. In Automated deduction — cade-18Automated Deduction — CADE-18, A. Voronkov (Ed.), LNAI, pp. 247–252. External Links: Link Cited by: p1.
  209. [99] M. Kohlhase and A. Koller (2000) Towards a tableaux machine for language understanding. In ICoS-2. inference in computational semantics. workshop proceedingsProceedings of Inference in Computational Semantics ICoS-2, J. Bos and M. Kohlhase (Eds.), pp. 57–88. Cited by: p1.
  210. [207] J. Siekmann, C. BenzMüller, L. Cheikhrouhou, A. Fiedler, A. Franke, H. Horacek, M. Kohlhase, A. Meier, E. Melis, M. Pollet, V. Sorge, C. Ullrich, and J. Zimmer (2000) Adaptive course generation and presentation. In Proceedings of ITS-2000 workshop on Adaptive and Intelligent Web-Based Education Systems, P. Brusilovski and C. Peylo (Eds.), Montreal. Cited by: p1.
  211. [12] P. Blackburn, J. Bos, and M. Kohlhase (1999) Automated reasoning for computational semantics. In The Third International Tbilisi Symposium on Language, Logic and Computation, Batumi, Georgia. Cited by: p1.
  212. [11] P. Blackburn, J. Bos, M. Kohlhase, and H. de Nivelle (1998) Automated theorem proving for natural language understanding. In CADE-15 Workshop “Problem-solving Methodologies with Automated Deduction”CADE-15 workshop “problem-solving methodologies with automated deduction”, P. Baumgartner, U. Furbach, M. Kohlhase, W. McCune, W. Reif, M. Stickel, T. Uribe, P. Baumgartner, U. Furbach, M. Kohlhase, W. McCune, W. Reif, M. Stickel, and T. Uribe (Eds.), Cited by: p1.
  213. [208] J. Siekmann, S. Hess, C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, and V. Sorge (1998) A distributed graphical user interface for the interactive proof system OMEGA. In User interfaces for theorem proversUser Interfaces for Theorem Provers, R. C. Backhouse (Ed.), Computing Science Reports, pp. 130–138. Cited by: p1.
  214. [209] J. Siekmann, S. Hess, C. BenzMüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, and V. Sorge (1998) LOUI: a distributed graphical user interface for the interactive proof system OMEGA. In Proceedings of the International Workshop “User Interfaces for Theorem Provers 1998” (UITP’98), Eindhoven, Netherlands. External Links: Link Cited by: p1.
  215. [36] M. Egg and M. Kohlhase (1997) Underspecification of quantifier scope. In Proceedings der 6. Fachtagung der Sektion Computerlinguistik der DGfS, Heidelberg. External Links: Link Cited by: p1.
  216. [69] M. Kerber and M. Kohlhase (1996) Partiality without the cost. In Workshop on “Mechanization of Partial Functions” at CADE-13, Cited by: p1.
  217. [100] M. Kohlhase, S. Kuschert, and M. Pinkal (1996) A type-theoretic semantics for λ-DRT. In Proceedings of the 10th Amsterdam Colloquium, P. Dekker and M. Stokhof (Eds.), Amsterdam, pp. 479–498. External Links: Link Cited by: p1.
  218. [54] X. Huang, M. Kerber, M. Kohlhase, D. Nesmith, and J. Richts (1994) Guaranteeing correctness through the communication of checkable proofs (or: would you really trust an automated reasoning system?). In CADE-14 Workshop, Cited by: p1.
  219. [55] X. Huang, M. Kerber, M. Kohlhase, and W. Reif (1994) A test for evaluating the practical usefulness of deduction systems. In Informal Proc. of the 11th Annual Meeting of the “GI-Fachgruppe Deduktionssysteme”Informal Proc. of the 11th Annual Meeting of the “GI-Fachgruppe Deduktionssysteme”, C. W. Wolfgang Bibel (Ed.), Forschungsbericht, FB Informatik, TH Darmstadt, pp. 12–12. Cited by: p1.
  220. [68] M. Kerber and M. Kohlhase (1994) Formalizing mathematics with dependent sorts. In Proceedings des Deduktionstreffen, AIDA-Report. Cited by: p1.
  221. [112] M. Kohlhase (1993) Higher-order resolution with combinators. In Informal Proceedings fo the Annual Meeting of “GI-Fachgruppe ‘Deduktionssysteme’ ” in Kaiserslautern, 1993, J. Avenhaus and J. Denzinger (Eds.), SEKI-Report, pp. 15. Cited by: p1.

Technical Reports

  1. [56] M. Kohlhase (2024) Editorial notes for . Technical report Comprehensive Archive Network (CTAN). External Links: Link Cited by: p1.
  2. [57] M. Kohlhase (2024) Preparing dfg proposals and reports in with dfgproposal.cls. Technical report Comprehensive Archive Network (CTAN). External Links: Link Cited by: p1.
  3. [58] M. Kohlhase (2024) Preparing fp7 eu proposals and reports in with euproposal.cls. Technical report Comprehensive Archive Network (CTAN). External Links: Link Cited by: p1.
  4. [59] M. Kohlhase (2024) Preparing proposals in with proposal.cls. Technical report Comprehensive Archive Network (CTAN). External Links: Link Cited by: p1.
  5. [1] K. Amann, M. Kohlhase, and F. Rabe (2018) Notebook import into mathhub.info (interactive display). Deliverable Technical Report D4.11, OpenDreamKit. External Links: Link Cited by: p1.
  6. [11] J. Cremona, D. Müller, M. Kohlhase, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2018) Report on OpenDreamKit deliverable d6.5: gap/sage/lmfdb interface theories and alignment in omdoc/mmt for system interoperability. Deliverable Technical Report D6.5, OpenDreamKit. External Links: Link Cited by: p1.
  7. [12] J. Cremona, D. Müller, M. Kohlhase, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2018) Report on OpenDreamKit deliverable d6.8: curated math-in-the-middle ontology and alignments for gap/sage/lmfdb. Deliverable Technical Report D6.8, OpenDreamKit. External Links: Link Cited by: p1.
  8. [36] M. Kohlhase, T. Koprucki, D. Müller, and K. Tabelow (2017) Mathematical models as research data via flexiformal theory graphs. WIAS Preprint Technical Report 2385. External Links: Document Cited by: p1.
  9. [44] M. Kohlhase and T. Wiesing (2017) In-place computation in active documents (context/computation). Deliverable Technical Report D4.9, OpenDreamKit. External Links: Link Cited by: p1.
  10. [55] M. Kohlhase (2017) Distributed, collaborative, versioned editing of active documents in mathhub.info. Deliverable Technical Report D4.3, OpenDreamKit. External Links: Link Cited by: p1.
  11. [60] T. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, and F. Rabe (2017) Model pathway diagrams for the representation of mathematical models. WIAS Preprint Technical Report 2431. External Links: Document Cited by: p1.
  12. [64] S. L. Luca De Feo and T. Wiesing (2017) Support for the scscp interface protocol in all relevant components (sage, gap etc.) distribution. Deliverable Technical Report D3.3, OpenDreamKit. External Links: Link Cited by: p1.
  13. [13] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Report on OpenDreamKit deliverable d6.3: design of triform (D/K/S) theories (specification/rnc schema/examples) and implementation of triform theories in the MMT API. Deliverable Technical Report D6.2, OpenDreamKit. External Links: Link Cited by: p1.
  14. [14] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. Pfeiffer, F. Rabe, N. M. Thiéry, and T. Wiesing (2016) Report on OpenDreamKit deliverables d6.2: initial D/K/S base design (including base survey and requirements workshop report) and d6.3: design of triform (D/K/S) theories (specification/RNC schema/examples) and implementation of triform theories in the mmt api. Deliverable Technical Report D6.2, OpenDreamKit. External Links: Link Cited by: p1.
  15. [33] M. Kohlhase and A. Glontaru (2016) Full-text search (formulae + keywords) over latex-based documents. Deliverable Technical Report D6.1, OpenDreamKit. External Links: Link Cited by: p1.
  16. [54] M. Kohlhase (2016) Active/structured documents requirements and existing solutions. Deliverable Technical Report D4.2, OpenDreamKit. External Links: Link Cited by: p1.
  17. [53] M. Kohlhase (Ed.) (2015) Formats for topics and submissions for the math-3 task at ntcir-12. Technical report NTCIR. Cited by: p1.
  18. [30] M. Kerber, C. Lange, and C. Rowat (2014-01) A formal proof of Vickrey’s theorem by blast, simp, and rule. Working Paper Technical Report 14-01, University of Birmingham, Department of Economics. External Links: Link Cited by: p1.
  19. [52] M. Kohlhase (Ed.) (2014) Formats for topics and submissions for the math-2 task at ntcir-11. Technical report NTCIR. External Links: Link Cited by: p1.
  20. [31] A. Kohlhase (2013-03) Framings of information: readers’ perception of information sources in spreadsheets. Technical report Technical Report 30, Jacobs University. External Links: Link Cited by: p1.
  21. [66] T. Mossakowski, C. Maeder, M. Codescu, E. Kuksa, and C. Lange (2013-01-10) Hets for Common Logic users. DFKI GmbH, Bremen. External Links: Link Cited by: p1.
  22. [70] (2012-06-04) OntoIOp (ontology integration and interoperability) part 1: the distributed ontology language (DOL). International Standard (Working Draft) Technical Report 17347, ISO. External Links: Link Cited by: p1.
  23. [51] M. KohlhaseM. Kohlhase (Ed.) (2012) Topics for the NTCIR-10 math task; math retrieval subtask. Technical report NTCIR. External Links: Link Cited by: p1.
  24. [71] F. Rabe and M. Kohlhase (2012) An XML-based syntax for MMT. Technical report Cited by: p1.
  25. [24] M. Iancu, M. Kohlhase, and F. Rabe (2011) Translating the Mizar Mathematical Library into OMDoc format. Technical report Technical Report KWARC Report-01/11, Jacobs University Bremen. Cited by: p1.
  26. [25] M. Iancu, M. Kohlhase, and F. Rabe (2011) Translating the Mizar Mathematical Library into OMDoc format. KWARC Report Jacobs University Bremen. Note: http://uniformal.github.io/doc/applications/LATIN/docs/Mizar2OMDoc-Report.pdf External Links: Link Cited by: p1.
  27. [65] R. Ausbrooks, S. Buswell, D. Carlisle, G. Chavchanidze, S. Dalmas, S. Devitt, A. Diaz, S. Dooley, R. Hunter, P. Ion, M. Kohlhase, A. Lazrek, P. Libbrecht, B. Miller, R. Miner, M. Sargent, B. Smith, N. Soiffer, R. Sutor, and S. WattD. Carlisle, P. Ion, and R. Miner (Eds.) (2010) Mathematical Markup Language (MathML) version 3.0. W3C Recommendation World Wide Web Consortium (W3C). External Links: Link Cited by: p1.
  28. [73] V. Zholudev, M. Kohlhase, and F. Rabe (2010) A [insert xml format] database for [insert cool application] (extended version). Technical report Jacobs University Bremen. Note: https://kwarc.info/vzholudev/pubs/XMLPrague_long.pdf External Links: Link Cited by: p1.
  29. [9] C. Calude and C. Müller (2009-03) Formal Proofs: Reconciling Correctness and Understanding. Research Reports Centre for Discrete Mathematics and Theoretical Computer Science, University of Auckland. Note: http://www.cs.auckland.ac.nz/CDMTCS//researchreports/354cris.pdf External Links: Link Cited by: p1.
  30. [39] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2009-02) Notations for active mathematical documents. KWARC Report Technical Report 2009-1, Jacobs University Bremen. Note: https://kwarc.info/publications/papers/KLMMR_NfAD.pdf External Links: Link Cited by: p1.
  31. [32] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2009) Notations for Active Mathematical Documents. Technical report Technical Report 2009-1, Jacobs University Bremen. Cited by: p1.
  32. [72] H. Stamerjohanns, D. Ginev, C. David, D. Misev, V. Zamdzhiev, and M. Kohlhase (2009) A comparison study of MathML-aware converters. KWARC Report Jacobs University Bremen. Cited by: p1.
  33. [61] C. Lange and M. Kohlhase (2008-12) A mathematical approach to ontology authoring and documentation. KWARC Report Technical Report 2008-3, Jacobs University Bremen. External Links: Link Cited by: p1.
  34. [67] C. Müller and M. Kohlhase (2008-11) Communities of practice in mathematical e-learning. Research Report Centre for Discrete Mathematics and Theoretical Computer Science, University of Auckland. External Links: Link Cited by: p1.
  35. [68] C. Müller and M. Kohlhase (2008-11) Context Aware Adaptation: A Case Study on Mathematical Notations. Research Report Centre for Discrete Mathematics and Theoretical Computer Science, University of Auckland. External Links: Link Cited by: p1.
  36. [38] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2008-04) Adaptation of notations in living mathematical documents. KWARC Report Technical Report 2008-2, Jacobs University Bremen. External Links: Link Cited by: p1.
  37. [19] J. Gičeva (2008) Capturing rhetorical aspects in mathematical documents using OMDoc and SALT. Technical Report Jacobs University and DERI Galway. Cited by: p1.
  38. [69] C. Müller (2008) A Survey on Mathematical Notations. KWARC Report Technical Report 2008-1, Jacobs University Bremen. External Links: Link Cited by: p1.
  39. [62] C. Lange (2007-03) SWiM – a semantic wiki for mathematical knowledge management. Technical report Technical Report 5, Jacobs University Bremen. Note: Revised, updated and reviewed version of thesis [63] External Links: Link Cited by: p1.
  40. [63] C. Lange (2006-08) A Semantic Wiki for Mathematical Knowledge Management. Diploma thesis, Universität Trier. External Links: Link Cited by: 62.
  41. [8] S. Buswell, O. Caprotti, D. P. Carlisle, M. C. Dewar, M. Gaëtano, and M. Kohlhase (2004) The Open Math standard, version 2.0. Technical report The OpenMath Society. External Links: Link Cited by: p1.
  42. [2] A. Asperti, M. Kohlhase, and C. Sacerdoti Coen (2003) Prototype n. d2.b document type descriptors: OMDoc proofs. MoWGLI Deliverable The MoWGLI Project. Cited by: p1.
  43. [3] S. Autexier, F. Eberhardt, D. Hutter, M. Kohlhase, and R. Anghelache (2003) Distributed knowledge management and version control. Deliverable Technical Report D5.a, The MoWGLI Project. Cited by: p1.
  44. [4] C. Benzmüller, M. Kohlhase, and C. E. Brown (2003) Higher order semantics and extensionality.. Technical Report Technical Report 03-001, Department of Mathematical Sciences, Carnegie Mellon University. External Links: Link Cited by: p1.
  45. [10] R. Ausbrooks, S. Buswell, D. Carlisle, S. Dalmas, S. Devitt, A. Diaz, M. Froumentin, R. Hunter, P. Ion, M. Kohlhase, R. Miner, N. Poppelier, B. Smith, N. Soiffer, R. Sutor, and S. WattD. Carlisle, P. Ion, R. Miner, and N. Poppelier (Eds.) (2003) Mathematical Markup Language (MathML) version 2.0 (second edition). W3C Recommendation World Wide Web Consortium (W3C). External Links: Link Cited by: p1.
  46. [43] M. Kohlhase and M. Simons (2002) Interpreting negatives in discourse. Technical report Technical Report CMU-PHIL-127, Philosophy, Carnegie Mellon University. External Links: Link Cited by: p1.
  47. [50] M. Kohlhase (2000) OMDoc: towards an OpenMath representation of mathematical documents. Seki Report Technical Report SR-00-02, Fachbereich Informatik, Universität des Saarlandes. External Links: Link Cited by: p1.
  48. [35] M. Kohlhase and K. Konrad (1999) Model generation for discourse representation theory. SEKI-Report Technical Report SR-99-01, Dept. of Computer Science, Universität des Saarlandes, Germany. Cited by: p1.
  49. [7] P. Blackburn, J. Bos, M. Kohlhase, and H. de Nivelle (1998) Inference and computational semantics. CLAUS Report Technical Report 99, University of the Saarland, Saarbrücken. Cited by: p1.
  50. [34] M. Kohlhase and K. Konrad (1998) Higher-order automated theorem proving for natural language semantics. Seki Report Technical Report SR-98-04, Fachbereich Informatik, Universität Saarbrücken. External Links: Link Cited by: p1.
  51. [29] M. Kerber and M. Kohlhase (1997-09) Reasoning without believing: on the mechanization of presuppositions and partiality. Technical report Technical Report CSRP-97-23, University of Birmingham, School of Computer Science. External Links: Link Cited by: p1.
  52. [5] C. Benzmüller and M. Kohlhase (1997) Model existence for higher-order logic. SEKI-Report Technical Report SR-97-09, Universität des Saarlandes. Cited by: p1.
  53. [6] C. Benzmüller and M. Kohlhase (1997) Resolution for henkin models. SEKI-Report Technical Report SR-97-10, Universität des Saarlandes. Cited by: p1.
  54. [15] C. Gardent, M. Kohlhase, and K. Konrad (1997) Higher–order coloured unification: a linguistic application. CLAUS Report Technical Report 97, University of the Saarland, Saarbrücken. Cited by: p1.
  55. [37] M. Kohlhase and S. Kuschert (1997) Dynamic lambda calculus. Technical report CLAUS-Report 91, Universität des Saarlandes, Computer Linguistics, Saarland University. Cited by: p1.
  56. [16] C. Gardent, M. Kohlhase, and N. van Leusen (1996) Corrections and higher-order unification. CLAUS Report Technical Report 77, University of the Saarland, Saarbrücken. Cited by: p1.
  57. [17] C. Gardent and M. Kohlhase (1996) Focus and higher–order coloured unification. CLAUS Report Technical Report 75, University of the Saarland, Saarbrücken. Cited by: p1.
  58. [18] C. Gardent and M. Kohlhase (1996) Higher–order coloured unification and natural language semantics. CLAUS Report Technical Report 76, University of the Saarland, Saarbrücken. Cited by: p1.
  59. [27] M. Kerber, M. Kohlhase, and V. Sorge (1996) An Integration of Mechanised Reasoning and Computer Algebra that Respects Explicit Proofs. Seki Report Technical Report SR-96-06, Fachbereich 14 Informatik, Universität des Saarlandes. External Links: Link Cited by: p1.
  60. [49] M. Kohlhase (1996) Higher-order tableaux with combinators. SEKI Report Technical Report SR-96-01, Dept. of Computer Science, Universität des Saarlandes, Germany. Cited by: p1.
  61. [20] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann (1995) Omega-MKRP, ein mathematisches assistenzsystem. SEKI Working Paper Technical Report SWP-95-01, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
  62. [23] D. Hutter and M. Kohlhase (1995) A coloured version of the λ-calculus. Technical Report Technical Report SR-95-05, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
  63. [42] M. Kohlhase and O. Scheja (1995) Higher-order multi-valued resolution. SEKI Report Technical Report SR-95-04, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
  64. [47] M. Kohlhase (1994) A mechanization of sorted higher-order logic based on the resolution principle. SEKI Report Technical Report SR-94-10, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
  65. [48] M. Kohlhase (1994) Higher-order order-sorted resolution. Seki Report Technical Report SR-94-1, Fachbereich Informatik, Universität des Sarrlandes. Cited by: p1.
  66. [26] P. Johann and M. Kohlhase (1993) Unification in an extensional lambda calculus with ordered function sorts and constant overloading. SEKI-Report Technical Report SR-93-14, Universität des Saarlandes. Cited by: p1.
  67. [28] M. Kerber and M. Kohlhase (1993) A mechanization of strong Kleene logic for partial functions. SEKI-Report Technical Report SR-93-20 (SFB), Universität des Saarlandes, Saarbrücken. Cited by: p1.
  68. [46] M. Kohlhase (1993) A unifying principle for extensional higher-order logic. Technical Report Technical Report 93–153, Dept. of Mathematics, Carnegie Mellon University. Cited by: p1.
  69. [21] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann (1992) Ω-MKRP – a proof development environment. Technical Report Technical Report SR-92-22, Universität des Saarlandes. Cited by: p1.
  70. [22] X. Huang, M. Kerber, and M. Kohlhase (1992) Methods — the basic unit for planning and verifying proofs. SEKI-Report Technical Report SR-92-20, Fachbereich Informatik, Universität des Saarlandes. Cited by: p1.
  71. [45] M. Kohlhase (1991) Order-sorted type theory I: unification. SEKI-Report Technical Report SR-91-18 (SFB), Universität des Saarlandes, Saarbrücken. Cited by: p1.
  72. [40] M. Kohlhase and D. Müller The sTeX3 manual. Technical report External Links: Link Cited by: p1.
  73. [41] M. Kohlhase and C. Prodescu MathWebSearch manual. Web Manual Jacobs University. External Links: Link Cited by: p1.

Unpublished

  1. [21] M. Kohlhase and M. Schütz (2024) Reusing learning objects via theory morphisms. Note: submitted External Links: Link Cited by: p1.
  2. [49] N. Roux (2022-07-21) A framework for defining structure-preserving diagram operators (slides). M.Sc. Thesis Defense Slides, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  3. [48] N. Roux (2021-03-22) A beginner’s guide to logical relations for a logical framework. seminar paper, FAU Erlangen-Nürnberg. Note: written as a student of the kwarc seminar External Links: Link Cited by: p1.
  4. [47] N. Roux (2021-01-27) A beginner’s guide to logical relations for a logical framework (slides). seminar presentation, FAU Erlangen-Nürnberg. Note: presented as a student of the kwarc seminar External Links: Link Cited by: p1.
  5. [36] F. Rabe and N. Roux (2021) Modular formalization of formal systems. Note: under review External Links: Link Cited by: p1.
  6. [45] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: 44.
  7. [3] J. Carette, W. M. Farmer, Y. Sharoda, K. Berčič, M. Kohlhase, D. Müller, and F. Rabe (2020) The space of mathematical software systems – a survey of paradigmatic systems. Note: preprint; http://arxiv.org/abs/2002.04955 Cited by: p1.
  8. [11] A. Kohlhase and M. Kohlhase (2020) Linebreaking formulae – an eye-tracking study. External Links: Link Cited by: p1.
  9. [17] M. Kohlhase, F. Rabe, C. S. Coen, and J. F. Schaefer (2020) Logic-independent proof search in logical frameworks (extended report). Note: extended report of conference submission External Links: Link Cited by: p1.
  10. [18] M. Kohlhase, F. Rabe, and M. Wenzel (2020) Making Isabelle content accessible in knowledge representation formats. External Links: Link, 2005.08884 Cited by: p1.
  11. [19] M. Kohlhase and F. Rabe (2020) Experiences from exporting major proof assistant libraries. External Links: Link, 2005.03089 Cited by: p1.
  12. [20] M. Kohlhase and M. Rapp (2020) Argumentation via context graphs. Cited by: p1.
  13. [42] M. Rapp, A. Adrian, and M. Kohlhase (2020) Context graphs for legal reasoning and argumentation. External Links: 2007.00732, Link Cited by: p1.
  14. [43] N. Roux and F. Rabe (2020) Diagram Operators in a Logical Framework. Extended Abstract, Frontiers in Artificial Intelligence and Applications. External Links: Link Cited by: p1.
  15. [44] N. Roux and F. Rabe (2020) Functorial Diagram Operators. Extended Abstract. Note: Extended abstract accepted as [45] Cited by: p1.
  16. [46] N. Roux (2019-07-15) Refactoring of theory graphs in knowledge representation systems (slides). B.Sc. Thesis Defense Slides, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  17. [35] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. Extended Abstract. External Links: Link Cited by: p1.
  18. [41] F. Rabe (2018) MMT: a foundation-independent logical framework. Online Documentation. External Links: Link Cited by: p1.
  19. [7] T. G. D. M. L. W. Group (2016) International mathematical knowledge trust charter. External Links: Link Cited by: p1.
  20. [9] M. Iancu, M. Kohlhase, F. Rabe, and H. Yuan (2016) Mixing surface languages for OMDoc. External Links: Link Cited by: p1.
  21. [10] M. Iancu, M. Kohlhase, and F. Rabe (2016) Understanding the pragmatics of module systems for mathematics. External Links: Link Cited by: p1.
  22. [30] M. Kohlhase (2016) An open markup format for mathematical documents OMDoc [version 1.3]. Note: Draft Specification External Links: Link Cited by: p1.
  23. [31] M. Kohlhase (2016) An open markup format for mathematical documents OMDoc [version 1.6 (pre-2.0)]. Note: Draft Specification External Links: Link Cited by: p1.
  24. [50] A. Toader, M. Kohlhase, and A. Kohlhase (2015) Assessment for spreadsheets via theory graphs. External Links: Link Cited by: p1.
  25. [4] M. A. Dumitru, D. Ginev, M. Kohlhase, V. Merticariu, S. Mirea, and T. Wiesing (2014) System description: KAT an annotation tool for STEM documents. External Links: Link Cited by: p1.
  26. [16] M. Kohlhase and C. Jucovschi (2014) Editing workflows in SMGloM. Note: SMGloM Blue Note External Links: Link Cited by: p1.
  27. [28] M. Kohlhase (2014) Content management in smglom. Note: SMGloM Blue Note External Links: Link Cited by: p1.
  28. [29] M. Kohlhase (2014) SMGloM primer. Note: SMGloM Blue Note External Links: Link Cited by: p1.
  29. [2] T. Breitsprecher, M. Codescu, C. Jucovschi, M. Kohlhase, L. Schröder, and S. Wartzack (2013) Towards ontological support for principle solutions in mechanical engineering. External Links: Link Cited by: p1.
  30. [15] M. Kohlhase, D. Ginev, and V. Merticariu (2013) A framework for semantic publishing of modular content objects. External Links: Link Cited by: p1.
  31. [27] M. Kohlhase (2013) SMGloM: a semantic multilingual glossary system for mathematics. Note: SMGloM Blue Note External Links: Link Cited by: p1.
  32. [5] D. Ginev (2012-06) On digital corpora of scientific documents - knowledge management and representations. Note: unpublished KWARC blue notes External Links: Link Cited by: p1.
  33. [6] D. Ginev (2012-06) Towards a build system for digital corpora of scientific documents. Note: unpublished KWARC blue notes External Links: Link Cited by: p1.
  34. [14] M. Kohlhase, C. David, D. Ginev, B. Matican, V. Merticariu, and S. Mirea (2012) A framework for semantic publishing of modular content objects. External Links: Link Cited by: p1.
  35. [40] F. Rabe (2012) A type theory based on reflection. Note: Manuscript Cited by: p1.
  36. [8] F. Horozal, M. Kohlhase, F. Rabe, and K. Sojakova (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
  37. [34] F. Rabe and M. Iancu (2010) A Formalized Set-Theoretical Semantics of Isabelle/HOL. External Links: Link Cited by: p1.
  38. [51] V. Zholudev and C. Lange (2010) TNTBase – a versioned XML database. External Links: Link Cited by: p1.
  39. [26] M. Kohlhase (2009-08) Towards bootstrapping the pragmatic to strict mapping in OMDoc. Note: unpublished KWARC blue notes Cited by: p1.
  40. [1] S. Awodey and F. Rabe (2009) Kripke Semantics for Martin-Löf’s Extensional Type Theory. External Links: Link Cited by: p1.
  41. [12] M. Kohlhase, C. Lange, C. Müller, N. Müller, and F. Rabe (2009) Notations for Active Mathematical Documents. Cited by: p1.
  42. [24] M. Kohlhase (2009) An OMDoc primer [version 1.6 (pre-2.0)]. External Links: Link Cited by: p1.
  43. [25] M. Kohlhase (2009) OMDoc: an open markup format for mathematical documents; language specification, primer, projects, applications [version 1.6 (pre-2.0)]. External Links: Link Cited by: p1.
  44. [33] N. Müller (2009) Change management on semi-structured documents. Note: https://kwarc.info/nmueller/papers/doceng09.pdf External Links: Link Cited by: p1.
  45. [39] F. Rabe (2009) The MMT Language. Cited by: p1.
  46. [13] M. Kohlhase, Ş. Anca, C. Jucovschi, A. González Palomo, and I. A. Şucan (2008) MathWebSearch 0.4, a semantic search engine for mathematics. Note: manuscript External Links: Link Cited by: p1.
  47. [38] F. Rabe (2008) Institutions with Proofs and their Representation in a Logical Framework. External Links: Link Cited by: p1.
  48. [22] M. Kohlhase CodeML: an open markup format the content and presentatation of program code. External Links: Link Cited by: p1.
  49. [23] M. Kohlhase The theorem prover museum – conserving the system heritage of automated reasoning. External Links: Link Cited by: p1.
  50. [32] R. Marcus, M. Kohlhase, and F. Rabe TGView3D system description: 3-dimensional visualization of theory graphs. External Links: Link Cited by: p1.
  51. [37] F. Rabe Theory expressions (a survey). Cited by: p1.

Miscellaneous

  1. [43] M. Kohlhase (2020) Logic-based natural language processing. External Links: Link Cited by: p1.
  2. [2] C. Acevedo (2014) OpenMathMap: interaction. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. External Links: Link Cited by: p1.
  3. [16] A. Dumitru, D. Ginev, M. Kohlhase, V. Merticariu, S. Mirea, and T. Wiesing (2014) KAT: an annotation tool for STEM documents; manual. External Links: Link Cited by: p1.
  4. [26] A. Giurgiu (2014) Semantically enhanced text documents. Jacobs University. Note: Bachelor’s Thesis Cited by: p1.
  5. [28] D. Hasegan (2014) Sorted unification in MathWebSearch. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. Cited by: p1.
  6. [51] A. L. Lezza (2014) Creating semantic interactions in airbus spreadsheet reports. Jacobs University. Note: Bachelor’s Thesis Cited by: p1.
  7. [59] A. V. Toader (2014) Assessment service for spreadsheet documents. Note: Bachelor’s Thesis, Jacobs University Cited by: p1.
  8. [46] C. Lange, M. Kerber, and C. RowatU. Furbach, R. Grimm, F. Hampe, S. Staab, and M. Wimmer (Eds.) (2013-09-17) Applying mechanised reasoning in economics – making reasoners applicable for domain experts. Note: Tutorial at INFORMATIK 2013, Computer science adapted to humans, organization and the environment, 43rd annual meeting of the German Informatics Society (Gesellschaft für Informatik e.V. (GI)) External Links: Link Cited by: p1.
  9. [7] M. B. Caminati, M. Kerber, C. Lange, and C. Rowat (2013) Proving soundness of combinatorial Vickrey auctions and generating verified executable code. External Links: 1308.1779 Cited by: p1.
  10. [13] J. W. Doerrie (2013) OpenMathMap: accessing math via interactive maps. B. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  11. [27] A. Guseva (2013) Towards understanding context dimensions of spreadsheet knowledge. Jacobs University. Note: Bachelor’s Thesis Cited by: p1.
  12. [52] S. Mirea (2013) An evaluation of responsive user interface options for multi-modal and mathematical search engines. Jacobs University. Note: Bachelor’s Thesis Cited by: p1.
  13. [36] M. Kerber, C. Lange, and C. RowatK. Judd (Ed.) (2012-07-25) An economist’s guide to mechanized reasoning or My computer just proved 84 impossibility theorems. Note: Invited lecture at the Initiative for Computational Economics summer school External Links: Link Cited by: p1.
  14. [3] M. Alecu (2012) Generic unification for type theories. Jacobs University Bremen. Note: Bachelor’s thesis Cited by: p1.
  15. [33] I. Ignatov (2012) Modular Encoding of Type Theory. Jacobs University Bremen. Note: Bachelor’s thesis Cited by: p1.
  16. [44] M. Kohlhase (2012) Mathematical documents want to be active, digital math libraries want to be semantic — position paper for wdml 2012. Position Paper at WDML Symposium. External Links: Link Cited by: p1.
  17. [8] M. Cîrlănaru (2011) Authoring, publishing and interacting with units and quantities in technical documents. B. Sc. Thesis, Jacobs University Bremen. Cited by: p1.
  18. [17] M. Kohlhase (2011) General Computer Science: GenCS I/II Lecture Notes. Semantic Course Notes in Panta Rhei. External Links: Link Cited by: p1.
  19. [18] M. Kohlhase (2011) General Computer Science; 320101: GenCS I Lecture Notes. External Links: Link Cited by: p1.
  20. [19] M. Kohlhase (2011) General Computer Science; Problems and Solutions for 320101 GenCS I. External Links: Link Cited by: p1.
  21. [20] M. Kohlhase (2011) General Computer Science; Problems for 320101 GenCS I. External Links: Link Cited by: p1.
  22. [21] M. Kohlhase (2011) General Computer Science: 320201 GenCS II Lecture Notes. External Links: Link Cited by: p1.
  23. [22] M. Kohlhase (2011) General Computer Science: Problems and Solutions for 320201 GenCS II. External Links: Link Cited by: p1.
  24. [23] M. Kohlhase (2011) General Computer Science: Problems for 320201 GenCS II. External Links: Link Cited by: p1.
  25. [41] M. Kohlhase and L. Schroeder (2011) The FormalCAD Project. External Links: Link Cited by: p1.
  26. [50] C. Lange (2011) Survey results on collaborative mathematical knowledge management. Note: Appendix to the Ph.D. thesis “Enabling Collaboration on Semiformal Mathematical Knowledge by Semantic Web Integration” External Links: Link Cited by: p1.
  27. [61] V. Zamdzhiev (2011) Formalizing Syntactical Objects within Formalized Set Theory. Jacobs University Bremen. Note: Bachelor’s thesis Cited by: p1.
  28. [62] V. Zamdzhiev (2011) Universal OpenMath machine. B. Sc. Thesis, Jacobs University Bremen. Cited by: p1.
  29. [1] (2010) Note: http://tntbase.org/wiki/restful Cited by: p1.
  30. [12] C. David (2010) Interactive documents as interfaces to computer algebra systems: JOBAD and Wolfram—Alpha. B. Sc. Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  31. [14] S. Dumbrava and F. Rabe (2010) Structuring Theories with Partial Morphisms. Note: Workshop on Abstract Development Techniques Cited by: p1.
  32. [15] S. Dumbrava (2010) Structured specifications with hiding in the edinburgh logical framework LF. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  33. [53] D. Misev (2010) Integrating SUMO and OMDoc. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. Cited by: p1.
  34. [11] J. H. Davenport and M. Kohlhase (2009) Unifying Math Ontologies: A tale of two standards (full paper). Note: http://opus.bath.ac.uk/13079 External Links: Link Cited by: p1.
  35. [24] J. Gičeva (2009) Integrating web services into active mathematical documents. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. External Links: Link Cited by: p1.
  36. [25] D. Ginev (2009) An architecture for recovering meaning in a to OMDoc conversion. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  37. [29] F. Horozal and F. Rabe (2009) A Formal Proof of the Soundness of First-order Logic. Cited by: p1.
  38. [32] A. Iacob (2009) Reasoning about theory morphisms. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  39. [37] M. Kohlhase, T. Mossakowski, and F. Rabe (2009) The LATIN Project. External Links: Link Cited by: p1.
  40. [45] S. Kuryla (2009) OMDoc as an ontology language: OWL→OMDoc translation implementation. Project report. Cited by: p1.
  41. [57] F. Rabe and C. Schürmann (2009) A Module System for Twelf. External Links: Link Cited by: p1.
  42. [49] C. Lange (2008-03) Mathematik lernen in einem semantischen wiki. Note: Invited talk at the 99th MNU-Kongress (Deutscher Verein zur Förderung des mathematischen und naturwissenschaftlichen Unterrichts e.V.) External Links: Link Cited by: p1.
  43. [35] A. Ioniţă (2008) Extracting RDF knowledge from OMDoc. Bachelor’s thesis, Jacobs University Bremen. Cited by: p1.
  44. [63] V. Zholudev (2008) Towards distributed mathematical knowledge management. Jacobs University of Bremen. Note: https://kwarc.info/vzholudev/pubs/proposal.pdf External Links: Link Cited by: p1.
  45. [54] C. Müller (2007-03) Lectora: Towards an Interactive, Collaborative Reader for Mathematical Documents. Jacobs University Bremen. Note: Research proposal External Links: Link Cited by: p1.
  46. [60] C. Lange and others (2007-03) OMDoc (from Wikipedia, the free encyclopedia). Note: http://en.wikipedia.org/w/index.php?title=OMDoc&oldid=112340133 External Links: Link Cited by: p1.
  47. [48] C. Lange (2007-02) Towards a Semantic Wiki for Science. Jacobs University Bremen. Note: https://kwarc.info/swim/pubs/swimplus-resprop.pdfResearch proposal for a Ph. D. thesis External Links: Link Cited by: p1.
  48. [4] Ş. Anca (2007) MaTeSearch a combined math and text search engine. Bachelor’s Thesis, Jacobs University Bremen. External Links: Link Cited by: p1.
  49. [6] M. Bröcheler (2007) A mathematical semantic web. Bachelor’s Thesis, Computer Science, Jacobs University, Bremen. External Links: Link Cited by: p1.
  50. [10] C. Müller (2007) Panta Rhei: Case Study Fall2007. Note: https://kwarc.info/panta-rhei/papers/cs_Fall2007.pdf External Links: Link Cited by: p1.
  51. [34] A. Ioniţă (2007) Developing a REST interface to a database for OMDoc. Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI) Bremen. External Links: Link Cited by: p1.
  52. [31] D. Hutter and M. Kohlhase (2006) Ontology-driven management of change. External Links: Link Cited by: p1.
  53. [55] N. Müller (2006) Towards an Ontology-Driven Management of Change – Research proposal for a Ph.D. thesis. International University Bremen. Note: https://kwarc.info/nmueller/papers/resprop.pdf External Links: Link Cited by: p1.
  54. [9] A. Kohlhase (2005) CPoint. External Links: Link Cited by: p1.
  55. [38] M. Kohlhase and D. Carlisle (2003) Guidelines for graphics in MathML 2. Note: W3C Note External Links: Link Cited by: p1.
  56. [39] M. Kohlhase and S. Devitt (2003) Bound variables in MathML. Note: W3C Working Group Note External Links: Link Cited by: p1.
  57. [40] M. Kohlhase and S. Devitt (2003) Structured types in MathML 2.0. Note: W3C Note External Links: Link Cited by: p1.
  58. [42] M. Kohlhase (2001) OMDoc: an open markup format for mathematical documents (version 1.1). Open Specification. External Links: Link Cited by: p1.
  59. [30] X. Huang, M. Kerber, M. Kohlhase, D. Nesmith, and J. Richts (1994) A test for evaluating the practical usefulness of deduction systems. Note: Workshop “Evaluation of Automated Theorem Proving Systems” on CADE’94 Cited by: p1.
  60. [5] K. Berčič Math databases wiki. External Links: Link Cited by: p1.
  61. [47] C. Lange, N. Müller, and C. Müller Document ontologies. Note: project homepage External Links: Link Cited by: p1.
  62. [56] Open digital research environment toolkit for the advancement of mathematics. Project Proposal. External Links: Link Cited by: p1.
  63. [58] F. Rabe The MMT language and system. External Links: Link Cited by: p1.