Archival Literature

Articles in Journals

  1. [24] M. Kohlhase and F. Rabe (2016) QED reloaded: towards a pluralistic formal library of mathematical knowledge. 9 (1), pp. 201–234. External Links: Link Cited by: p1.
  2. [29] M. Kohlhase (2014-06) Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. pp. 22–27. External Links: Link Cited by: p1.
  3. [20] M. Kohlhase and M. Iancu (2014) Co-representing structure and meaning of mathematical documents. 38 (2), pp. 49–80. Note: Special Issue “The language of mathematics – computational, linguistic and logical aspects” External Links: Link Cited by: p1.
  4. [22] M. Kohlhase, H. Mihaljevic-Brandt, W. Sperber and O. Teschke (2013-09) Zentralblatt column: mathematical formula search. pp. 56–57. External Links: Link Cited by: p1.
  5. [11] M. Iancu, M. Kohlhase, F. Rabe and J. Urban (2013) The Mizar Mathematical Library in OMDoc: translation and applications. 50 (2), pp. 191–202. External Links: Link, Document Cited by: p1.
  6. [17] A. Kohlhase and M. Kohlhase (2013) Spreadsheets with a semantic layer. 62, pp. 1–20. External Links: Link Cited by: p1.
  7. [31] F. Rabe and M. Kohlhase (2013) A scalable module system. 0 (230), pp. 1–54. External Links: Link Cited by: p1.
  8. [15] M. Kerber and M. Kohlhase (2012) Reasoning without believing: on the mechanization of presuppositions and partiality. 22 (4), pp. 295–317. External Links: Document Cited by: p1.
  9. [23] M. Kohlhase and F. Rabe (2012) Semantics of OpenMath and MathML3. 6 (3), pp. 235–260. External Links: Link Cited by: p1.
  10. [18] M. Kohlhase, J. Corneli, C. David, D. Ginev, Jucovschi, A. Kohlhase, C. Lange, B. Matican, S. Mirea and V. Zholudev (2011) The planetary system: web 3.0 & active documents for STEM. 4, pp. 598–607. Note: Finalist at the Executable Paper Grand Challenge External Links: Link, Document Cited by: p1.
  11. [34] H. Stamerjohanns, D. Ginev, C. David, D. M. and and M. Kohlhase (2010) Conversion d’articles en LaTeX vers XML avec MathML : une étude comparative. 51, pp. 7–28. External Links: Link Cited by: p1.
  12. [35] H. Stamerjohanns, M. Kohlhase, D. Ginev, C. D. and B. Miller (2010) Transforming large collections of scientific publications to XML. 3 (3), pp. 299–307. External Links: Link Cited by: p1.
  13. [36] 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. 17 (3), pp. 285–308. External Links: Document Cited by: p1.
  14. [2] C. E. Benzmüller, C. E. Brown and M. Kohlhase (2009) Cut-simulation and impredicativity. 5 (1), pp. 1–21. External Links: Link Cited by: p1.
  15. [30] C. Müller and M. Kohlhase (2009) Context-Aware Adaptation: A Case Study on Mathematical Notations. 26 (3), pp. 215–230. External Links: ISSN 1934-8703 Cited by: p1.
  16. [16] A. Kohlhase and M. Kohlhase (2008-06) Semantic knowledge management for education. 96 (6), pp. 970–989. External Links: Link Cited by: p1.
  17. [28] M. Kohlhase (2008) Using LaTeX as a semantic markup format. 2 (2), pp. 279–304. External Links: Link Cited by: p1.
  18. [1] C. Benzmüller, C. Brown and M. Kohlhase (2004) Higher order semantics and extensionality. 69, pp. 1027–1088. External Links: Link Cited by: p1.
  19. [3] P. Blackburn and M. Kohlhase (2004) Inference and computational semantics. 13 (2), pp. 117–120. External Links: Link Cited by: p1.
  20. [12] S. Jeschke, M. Kohlhase and R. Seiler (2004) eLearning-, eTeaching- & eResearch-technologien – Chancen und Potentiale für die Mathematik. 12 (2). External Links: Link Cited by: p1.
  21. [4] J. Bos and M. Kohlhase (2003) Editorial. 11 (4), pp. 381–384. Cited by: p1.
  22. [21] M. Kohlhase and A. Koller (2003) Resource-adaptive model generation as a performance model. 11 (4), pp. 435–456. External Links: Link Cited by: p1.
  23. [19] M. Kohlhase and A. Franke (2001) MBase: representing knowledge and context for the integration of mathematical software systems. 32 (4), pp. 365–402. External Links: Document, Link Cited by: p1.
  24. [10] D. Hutter and M. Kohlhase (2000) Managing structural information by higher-order colored unification. 25 (2), pp. 123–164. External Links: Link Cited by: p1.
  25. [27] M. Kohlhase (2000) OMDoc: an infrastructure for OpenMath content dictionary information. 34 (2), pp. 43–48. External Links: Link Cited by: p1.
  26. [6] A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase and V. Sorge (1999) Agent-oriented integration of distributed mathematical services. 5, pp. 156–187. External Links: Link Cited by: p1.
  27. [7] A. Franke and M. Kohlhase (1999) MBase: representing mathematical knowledge in a relational data base. 23 (3). Cited by: p1.
  28. [8] C. Gardent, M. Kohlhase and K. Konrad (1999) Higher-order colored unification: a linguistic application. 18 (2), pp. 1–28. External Links: Link Cited by: p1.
  29. [25] M. Kohlhase and O. Scheja (1999) Higher-order multi-valued resolution. 9. External Links: Link Cited by: p1.
  30. [32] 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. 3 (11), pp. 326–342. External Links: Link Cited by: p1.
  31. [5] M. Egg, C. Gardent and M. Kohlhase (1998) Steuerung der Inferenz in der Diskursverarbeitung. 7 (3), pp. 106–110. External Links: Link Cited by: p1.
  32. [13] M. Kerber, M. Kohlhase and V. Sorge (1998) Integrating computer algebra into proof planning. 21 (3), pp. 327–355. External Links: Link Cited by: p1.
  33. [33] J. Siekmann, M. Kohlhase and E. Melis (1998) Ωmega, ein mathematisches Assistenzsystem. 7 (3), pp. 101–105. External Links: Link Cited by: p1.
  34. [9] X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts and J. Siekmann (1996) Die Beweisentwicklungsumgebung Ωmega. 11, pp. 20–26. Cited by: p1.
  35. [14] M. Kerber and M. Kohlhase (1996) A tableau calculus for partial functions. 2, pp. 21–49. External Links: Link Cited by: p1.
  36. [26] M. Kohlhase (1996) Sorten für das automatische Beweisen höherer Stufe. Cited by: p1.

Articles in Collections

  1. [18] C. Lange and M. Kohlhase (2013) Mashups using mathematical knowledge. In Semantic mashups, B. Endres-Niggemeyer (Ed.), pp. 171–204. External Links: Link Cited by: p1.
  2. [6] A. Kohlhase and M. Kohlhase (2009) Compensating the computational bias of spreadsheets. In Festschrift 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.
  3. [7] 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 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.
  4. [17] 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 and E. Ras (Eds.), pp. 47–68. External Links: Link Cited by: p1.
  5. [3] 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.
  6. [15] M. Kohlhase (2008) Wissensrepräsentation für computerunterstützte Lehre. In Selbstorganisiertes Lernen im Internet, V. Hornung-Prähauser, M. Luckmann and M. Kalz (Eds.), pp. 248–251. Cited by: p1.
  7. [2] G. Bancerek and M. Kohlhase (2007) Towards a Mizar Mathematical Library in OMDoc format. In From 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.
  8. [5] 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], LNAI. Cited by: p1.
  9. [13] M. Kohlhase (2006-08) Standardizing context in system interoperability. In OMDoc – an open markup format for mathematical documents [version 1.2], LNAI. Cited by: p1.
  10. [14] M. Kohlhase (2006-08) STeX: a LaTeX-based workflow for OMDoc. In OMDoc – an open markup format for mathematical documents [version 1.2], LNAI. Cited by: p1.
  11. [16] 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.
  12. [12] M. Kohlhase (2003) Artificial intelligence: automated reasoning. pp. 247–250. Cited by: p1.
  13. [4] P. Blackburn, J. Bos, M. Kohlhase and H. de Nivelle (2001) Inference and computational semantics. In Computing meaning (volume 2), H. Bunt, L. Kievit, R. Muskens and M. Verlinden (Eds.), pp. 11–28. Cited by: p1.
  14. [8] M. Kohlhase, E. Melis and J. Siekmann (1999) ΩMEGA – a mathematical assistant. pp. 248–251. External Links: Link Cited by: p1.
  15. [1] (1998) Automated deduction – a basis for applications. In Automated deduction – a basis for applications, W. Bibel and P. Schmitt (Eds.), Cited by: p1.
  16. [10] M. Kohlhase (1998) Automated theorem proving in mathematics. In Automated deduction – a basis for applications, W. Bibel and P. Schmitt (Eds.), pp. 3–7. Cited by: p1.
  17. [11] M. Kohlhase (1998) Higher-order automated theorem proving. In Automated deduction – a basis for applications, W. Bibel and P. Schmitt (Eds.), pp. 431–462. External Links: Link Cited by: p1.
  18. [9] M. Kohlhase (1992) Beweissysteme mit Logiken höherer Stufe. pp. 213–238. Cited by: p1.

Papers at International, Peer-Reviewed Conferences

  1. [50] A. Kohlhase, M. Kohlhase and M. Fürsich (2017) Visual structure in math expressions. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  2. [69] M. Kohlhase, T. Koprucki, D. Müller and K. Tabelow (2017) Mathematical models as research data via flexiformal theory graphs. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  3. [98] 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 mathematics, LNAI. External Links: Link Cited by: p1.
  4. [102] W. Sperber and M. Kohlhase (2017) Software citations, information systems, and beyond. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  5. [19] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. P. , F. Rabe, N. M. Thiéry and T. Wiesing (2016) Interoperability in the OpenDreamKit project: the math-in-the-middle approach. In Intelligent computer mathematics, M. Kohlhase, M. Johansson, B. Miller, L. de Moura and Tompa (Eds.), LNAI. External Links: Link Cited by: p1.
  6. [27] 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 congress, G. Greuel, T. Koch, P. Paule and A. Sommese (Eds.), LNCS, Vol. 9725. External Links: Link Cited by: p1.
  7. [29] R. Hambasan and M. Kohlhase (2016) Faceted search for mathematics. In MACIS 2015, I. S. Kotsireas, S. M. Rump and C. K. Yap (Eds.), LNAI. External Links: Link Cited by: p1.
  8. [96] E. Luzhnica and M. Kohlhase (2016) Formula semantification and automated relation finding in the OEIS. In Mathematical 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.
  9. [42] M. Iancu and M. Kohlhase (2015) A flexiformal model of knowledge dissemination and aggregation in mathematics. In Intelligent computer mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and Sorge (Eds.), LNCS, pp. 137–152. External Links: Link Cited by: p1.
  10. [43] M. Iancu and M. Kohlhase (2015) Math literate knowledge management via induced material. In Intelligent computer mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and Sorge (Eds.), LNCS, pp. 187–202. External Links: Link Cited by: p1.
  11. [79] M. Kohlhase and W. Sperber (2015) The SMGloM project or why we need a semantic glossary of mathematics. External Links: Link Cited by: p1.
  12. [10] 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 2014, P. Garbacz and O. Kutz (Eds.), Frontiers in Artificial Intelligence and Applications, Vol. 267, pp. 427–432. External Links: Link, Document Cited by: p1.
  13. [11] J. Carette, W. Farmer and M. Kohlhase (2014) Realms: a structure for consolidating knowledge about mathematical theories. In Intelligent computer mathematics, 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.
  14. [35] F. Horozal, M. Kohlhase and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  15. [40] M. Iancu, C. Jucovschi, M. Kohlhase and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  16. [41] M. Iancu, M. Kohlhase and C. Prodescu (2014) Representing, archiving, and searching the space of mathematical knowledge. In Mathematical software - ICMS 2014 - 4th international congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 26–30. External Links: Link, Document Cited by: p1.
  17. [66] L. Kohlhase and M. Kohlhase (2014) System description: a semantics-aware LaTeX-to-office converter. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 440–443. External Links: Link Cited by: p1.
  18. [68] M. Kohlhase and M. Iancu (2014) Discourse-level parallel markup and meaning adoption in flexiformal theory graphs. In Mathematical software - ICMS 2014 - 4th international congress, H. Hong and C. Yap (Eds.), LNCS, Vol. 8592, pp. 36–40. External Links: Link, Document Cited by: p1.
  19. [92] M. Kohlhase (2014) A data model and encoding for a semantic, multilingual terminology of mathematics. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 169–183. External Links: Link Cited by: p1.
  20. [51] A. Kohlhase, M. Kohlhase, C. Jucovschi and A. Toader (2013) Full semantic transparency: overcoming boundaries of applications. In Human-computer interaction – interact 2013, P. Kotzé, G. Marsden, G. Lindgaard, J. Wesson and Winckler (Eds.), LNCS, pp. 406–423. External Links: Link Cited by: p1.
  21. [72] M. Kohlhase, F. Mance and F. Rabe (2013) A universal machine for biform theory graphs. In Intelligent computer mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka and Windsteiger (Eds.), Lecture Notes in Computer Science. External Links: Link Cited by: p1.
  22. [76] 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), External Links: Link Cited by: p1.
  23. [90] M. Kohlhase (2013) Knowledge management for systematic engineering design in CAD systems. In Professionelles Wissenmanagement Management, Konferenzbeiträge der 7. Konferenz, F. Lehner, N. Amende and N. Fteimi (Eds.), pp. 202–217. External Links: Link Cited by: p1.
  24. [91] M. Kohlhase (2013) The flexiformalist manifesto. In 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.
  25. [17] C. David, C. Jucovschi, A. Kohlhase and M. Kohlhase (2012) Semantic Alliance: a framework for semantic allies. In Intelligent 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.
  26. [34] F. Horozal, M. Kohlhase and F. Rabe (2012) Extending MKM formats at the statement level. In Intelligent 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.
  27. [73] M. Kohlhase, B. A. Matican and C. C. Prodescu (2012) MathWebSearch 0.5 – Scaling an Open Formula Search Engine. In Intelligent 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.
  28. [89] M. Kohlhase (2012) The Planetary project: towards eMath3.0. In Intelligent 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.
  29. [93] C. Lange, P. Ion, A. Dimou, C. B. , 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 web, E. Simperl, P. Cimiano, A. Polleres, O. Corcho and Presutti (Eds.), LNCS, pp. 763–777. External Links: Link, Document Cited by: p1.
  30. [1] J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, Rudnicki and J. Urban (2011) Licensing the Mizar Mathematical Library. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 149–163. Cited by: p1.
  31. [4] S. Autexier, C. David, D. Dietrich and M. K. and (2011) Workflows for the management of change in science, technologies, engineering and mathematics. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 164–179. External Links: Link Cited by: p1.
  32. [13] 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 Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  33. [14] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, Rabe and K. Sojakova (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  34. [15] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski and Rabe (2011) Project abstract: logic atlas and integrator (LATIN). In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 289–291. External Links: Link Cited by: p1.
  35. [28] D. Ginev, H. Stamerjohanns and M. Kohlhase (2011) The LaTeXML daemon: editable math on the collaborative web. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 292–294. External Links: Link Cited by: p1.
  36. [32] F. Horozal, A. Iacob, C. Jucovschi and M. K. and (2011) Combining source, content, presentation, narration, and relational representation. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 212–227. External Links: Link Cited by: p1.
  37. [33] F. Horozal, M. Kohlhase and F. Rabe (2011) Extending OpenMath with Sequences. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
  38. [63] 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), pp. 167–174. External Links: Link Cited by: p1.
  39. [64] A. Kohlhase and M. Kohlhase (2011) Maintaining islands of consistency via versioned links. In Intelligent computer mathematics – work in progress papers, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), External Links: Link Cited by: p1.
  40. [65] 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), pp. 181–188. External Links: Link Cited by: p1.
  41. [77] M. Kohlhase, F. Rabe and C. Sacerdoti Coen (2011) A foundational view on integration problems. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 107–122. Note: http://kwarc.info/kohlhase/papers/cicm11-integration.pdf External Links: Link Cited by: p1.
  42. [94] C. Lange, M. Kohlhase, C. David, D. Ginev, 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), G. Antoniou, M. Grobelnik, E. Paslaru Bontas Simperl, Parsia, D. Plexousakis, P. D. Leenheer and J. Z. Pan (Eds.), LNCS, pp. 471–475. External Links: 1103.1482 Cited by: p1.
  43. [18] C. David, M. Kohlhase, C. Lange, F. Rabe, Zhiltsov and V. Zholudev (2010) Publishing math lecture notes as linked data. In 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.
  44. [45] C. Jucovschi and M. Kohlhase (2010) sTeXIDE: an integrated development environment for sTeX collections. In Intelligent computer mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. I. and, R. Rioboo and A. P. Sexton (Eds.), LNAI, pp. 336–344. External Links: 1005.5489v1 Cited by: p1.
  45. [52] A. Kohlhase, M. Kohlhase and C. Lange (2010) Dimensions of formality: a case study for MKM in software engineering. In Intelligent computer mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. I. and, R. Rioboo and A. P. Sexton (Eds.), LNAI, pp. 355–369. External Links: 1004.5071v1 Cited by: p1.
  46. [53] 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 web, A. Paschke, N. Henze, T. Pellegrini and H. Weigand (Eds.), External Links: 1006.4474v1, Document Cited by: p1.
  47. [62] 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), S. Thorne (Ed.), pp. 111–121. External Links: Link Cited by: p1.
  48. [78] M. Kohlhase, F. Rabe and V. Zholudev (2010) Towards MKM in the large: modular representation and scalable software architecture. In Intelligent computer mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. I. and, R. Rioboo and A. P. Sexton (Eds.), LNAI, pp. 370–384. External Links: 1005.5232v2 Cited by: p1.
  49. [105] V. Zholudev and M. Kohlhase (2010) Scripting documents with xquery: virtual documents in TNTBase. In Proceedings 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.
  50. [16] J. H. Davenport and M. Kohlhase (2009-07) Unifying Math Ontologies: A tale of two standards. In MKM/Calculemus proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen and S. M. Watt (Eds.), LNAI, pp. 263–278. External Links: Link Cited by: p1.
  51. [58] A. Kohlhase and M. Kohlhase (2009-07) Compensating the computational bias of spreadsheets with MKM techniques. In MKM/Calculemus proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen and S. M. Watt (Eds.), LNAI, pp. 357–372. External Links: Link Cited by: p1.
  52. [59] A. Kohlhase and M. Kohlhase (2009-07) Spreadsheet interaction with frames: exploring a mathematical practice. In MKM/Calculemus proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen and S. M. Watt (Eds.), LNAI, pp. 341–356. External Links: Link Cited by: p1.
  53. [95] C. Lange and M. Kohlhase (2009-07) A mathematical approach to ontology authoring and documentation. In MKM/Calculemus proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen and S. M. Watt (Eds.), LNAI, pp. 389–404. External Links: Link Cited by: p1.
  54. [60] 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), B. Mehlenbacher, A. Protopsaltis, A. Williams and S. Slatterey (Eds.), pp. 135–142. External Links: Link Cited by: p1.
  55. [61] 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), B. Mehlenbacher, A. Protopsaltis, A. Williams and S. Slatterey (Eds.), pp. 89–96. External Links: Link Cited by: p1.
  56. [71] 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), A. Cavalcanti and D. Dams (Eds.), LNCS, pp. 223–238. External Links: Link Cited by: p1.
  57. [104] V. Zholudev and M. Kohlhase (2009) TNTBase: a versioned storage for XML. In Proceedings of balisage: the markup conference 2009, Balisage Series on Markup Technologies. Note: available at http://kwarc.info/vzholudev/pubs/balisage.pdf External Links: Link Cited by: p1.
  58. [74] M. Kohlhase, C. Müller and F. Rabe (2008) Notations for living mathematical documents. In Intelligent computer mathematics, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. and F. Wiedijk (Eds.), LNAI, pp. 504–519. External Links: Link Cited by: p1.
  59. [97] C. Müller and M. Kohlhase (2008) Towards a community of practice toolkit based on semantically marked up artifacts. pp. 41–50. Cited by: p1.
  60. [103] H. Stamerjohanns and M. Kohlhase (2008) Transforming the arXiv to XML. In Intelligent computer mathematics, S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. and F. Wiedijk (Eds.), LNAI, pp. 574–582. External Links: Link Cited by: p1.
  61. [57] A. Kohlhase and M. Kohlhase (2007) Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch. In MKM/Calculemus, M. Kauers, M. Kerber, R. Miner and W. Windsteiger (Eds.), LNAI, pp. 266–279. External Links: Link Cited by: p1.
  62. [99] I. Normann and M. Kohlhase (2007) Extended formula normalization for ϵ-retrieval and sharing of mathematical knowledge. In MKM/Calculemus, M. Kauers, M. Kerber, R. Miner and W. Windsteiger (Eds.), LNAI, pp. 266–279. Cited by: p1.
  63. [6] C. E. Benzmüller, C. E. Brown and M. Kohlhase (2006) Cut-simulation in impredicative logics. In Automated reasoning — third international joint conference, ijcar 2006, U. Furbach and N. Shankar (Eds.), LNAI, pp. 220–234. External Links: Link Cited by: p1.
  64. [31] E. Hilf, M. Kohlhase and H. Stamerjohanns (2006) Capturing the content of physics: systems, observables, and experiments. In Mathematical Knowledge Management (MKM), J. Borwein and W. M. Farmer (Eds.), LNAI, pp. 165–178. External Links: Link Cited by: p1.
  65. [55] A. Kohlhase and M. Kohlhase (2006) An exploration in the space of mathematical knowledge. In Mathematical knowledge management, MKM’05, M. Kohlhase (Ed.), LNAI, pp. 17–32. External Links: Link Cited by: p1.
  66. [56] A. Kohlhase and M. Kohlhase (2006) Communities of Practice in MKM: An Extensional Model. In Mathematical Knowledge Management (MKM), J. Borwein and W. M. Farmer (Eds.), LNAI, pp. 179–193. External Links: Link Cited by: p1.
  67. [80] M. Kohlhase and I. Şucan (2006) A search engine for mathematical formulae. In Proceedings 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.
  68. [88] M. Kohlhase (2005-11) OMDoc: Open Mathematical Documents. In Open 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.
  69. [54] A. Kohlhase and M. Kohlhase (2004) CPoint: dissolving the author’s dilemma. In Mathematical knowledge management, MKM’04, A. Asperti, G. Bancerek and A. Trybulec (Eds.), LNAI, pp. 175–189. External Links: Link Cited by: p1.
  70. [12] 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), T. Hardin and R. Rioboo (Eds.), pp. 69–74. External Links: Link Cited by: p1.
  71. [67] M. Kohlhase and R. Anghelache (2003) Towards collaborative content management and version control for structured mathematical knowledge. In Mathematical knowledge management, MKM’03, A. Asperti, B. Buchberger and J. H. Davenport (Eds.), LNCS, pp. 147–161. External Links: Link Cited by: p1.
  72. [3] A. Asperti and M. Kohlhase (2002) MathML in the MoWGLI project. In Second international conference on mathml and technologies for math on the web, External Links: Link Cited by: p1.
  73. [81] 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 web, External Links: Link Cited by: p1.
  74. [101] 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-18, A. Voronkov (Ed.), LNAI, pp. 144–149. Cited by: p1.
  75. [106] J. Zimmer and M. Kohlhase (2002) System Description: The MathWeb software bus for distributed mathematical reasoning. In Automated deduction — cade-18, A. Voronkov (Ed.), LNAI, pp. 247–252. External Links: Link Cited by: p1.
  76. [86] 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’2001, B. Buchberger and O. Caprotti (Eds.), External Links: Link Cited by: p1.
  77. [87] 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’2000, E. R. Lozano (Ed.), LNAI, pp. 32–52. External Links: Link Cited by: p1.
  78. [2] 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 deduction, M. Kerber and M. Kohlhase (Eds.), pp. 34–48. External Links: Link Cited by: p1.
  79. [22] A. Franke and M. Kohlhase (2000) System description: MBase, an open mathematical knowledge base. In Automated Deduction – cade-17, D. McAllester (Ed.), LNAI, pp. 455–459. External Links: Link Cited by: p1.
  80. [85] M. Kohlhase (2000) Model generation for discourse representation theory. In Proceedings of of the 14th european conference on artifical intelligence, W. Horn (Ed.), pp. 441–445. External Links: Link Cited by: p1.
  81. [100] M. Pinkal and M. Kohlhase (2000) Feature logic for dotted types: a formalism for complex word meanings. Hongkong, pp. 521–528. External Links: Link Cited by: p1.
  82. [9] 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), H. Bunt, L. Kievit, R. Muskens and M. Verlinden (Eds.), pp. 5–19. Cited by: p1.
  83. [21] A. Franke and M. Kohlhase (1999) System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Automated deduction — CADE-16, H. Ganzinger (Ed.), LNAI, pp. 217–221. External Links: Link Cited by: p1.
  84. [30] S. Hess, C. Jung, M. Kohlhase and V. Sorge (1998-07) An implementation of distributed mathematical services. In 6th calculemus and types workshop, A. Cohen and H. Barendregt (Eds.), Cited by: p1.
  85. [7] C. Benzmüller and M. Kohlhase (1998) Extensional higher order resolution. In Proceedings of the 15th Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 56–72. External Links: Link Cited by: p1.
  86. [8] C. Benzmüller and M. Kohlhase (1998) LEO – a higher order theorem prover. In Proceedings of the 15th Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 139–144. External Links: Link Cited by: p1.
  87. [5] C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. K. , 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 Deduction, W. McCune (Ed.), LNAI, pp. 252–255. External Links: Link Cited by: p1.
  88. [20] M. Egg and M. Kohlhase (1997) Dynamic control of quantifier scope. Amsterdam, The Netherlands, pp. 109–114. Cited by: p1.
  89. [26] C. Gardent and M. Kohlhase (1997) Computing parallelism in discourse. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI), M. E. Pollack (Ed.), pp. 1016–1021. External Links: Link Cited by: p1.
  90. [39] D. Hutter and M. Kohlhase (1997) A coloured version of the λ-calculus. In Proceedings of the 14th Conference on Automated Deduction, W. McCune (Ed.), LNAI, pp. 291–305. Cited by: p1.
  91. [49] M. Kerber and M. Kohlhase (1997) Mechanising partiality without re-implementation. In Proceedings 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.
  92. [70] M. Kohlhase and S. Kuschert (1997) Dynamic lambda calculus. pp. 85–92. Cited by: p1.
  93. [48] M. Kerber and M. Kohlhase (1996-08) A resolution calculus for presuppositions. In Proceedings of the 12th european conference on artificial intelligence, W. Wahlster (Ed.), pp. 375–379. External Links: Link Cited by: p1.
  94. [23] C. Gardent, M. Kohlhase and N. van Leusen (1996) Corrections and higher-order unification. Bielefeld, Germany, pp. 268–279. External Links: Link Cited by: p1.
  95. [24] C. Gardent and M. Kohlhase (1996) Focus and higher–order unification. Copenhagen, pp. 268–279. External Links: Link Cited by: p1.
  96. [25] C. Gardent and M. Kohlhase (1996) Higher–order coloured unification and natural language semantics. Santa Cruz, pp. 1–9. External Links: Link Cited by: p1.
  97. [46] M. Kerber, M. Kohlhase and V. Sorge (1996) Integrating computer algebra with proof planning. In Design and implementation of symbolic computation systems, disco’96, J. Calmet and C. Limogelli (Eds.), LNCS, pp. 204–215. Cited by: p1.
  98. [84] M. Kohlhase (1995) Higher-order tableaux. Koblenz, Germany, pp. 294–309. External Links: Link Cited by: p1.
  99. [36] 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 Deduction, A. Bundy (Ed.), LNAI, pp. 807–810. External Links: Link Cited by: p1.
  100. [37] 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 Deduction, A. Bundy (Ed.), LNAI, pp. 788–792. External Links: Link Cited by: p1.
  101. [38] 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 intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 379–390. External Links: Link Cited by: p1.
  102. [44] 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 Deduction, A. Bundy (Ed.), LNAI, pp. 620–634. External Links: Link Cited by: p1.
  103. [47] M. Kerber and M. Kohlhase (1994) A mechanization of strong Kleene logic for partial functions. In Proceedings of the 12th Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 371–385. External Links: Link Cited by: p1.
  104. [83] M. Kohlhase (1994) Unification in a λ-calculus with term declarations and function sorts. In 18th annual german conference on aritificial intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 331–342. External Links: Link Cited by: p1.
  105. [75] M. Kohlhase and F. Pfenning (1993) Unification in a λ-calculus with intersection types. pp. 488–505. External Links: Link Cited by: p1.
  106. [82] M. Kohlhase (1992) Unification in order-sorted type theory. In Proceedings of the international conference on logic programming and automated reasoning lpar’92, A. Voronkov (Ed.), LNAI, pp. 421–432. Cited by: p1.

Monographs

  1. [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.
  2. [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.

Conference Proceedings Edited

  1. [4] M. Kohlhase, M. Johansson, B. Miller, L. de Moura and Tompa (Eds.) (2016) Intelligent computer mathematics. LNAI, Springer. External Links: ISBN 978-3-319-08434-3 Cited by: p1.
  2. [2] 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.
  3. [5] M. Kohlhase (Ed.) (2006) Mathematical knowledge management, MKM’05. LNAI, Springer Verlag. Cited by: p1.
  4. [1] 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.
  5. [3] M. Kerber and M. Kohlhase (Eds.) (2000) CALCULEMUS-2000, systems for integrated computation and deduction. AKPeters, St. Andrews, Scotland. Cited by: p1.

Theses

  1. [2] 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.
  2. [1] 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. [7] M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, 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.
  2. [9] 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.
  3. [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.
  4. [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.
  5. [1] 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.
  6. [3] P. Blackburn and M. Kohlhase (Eds.) (2001) ICoS-3. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
  7. [4] J. Bos and M. Kohlhase (Eds.) (2000) ICoS-2. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
  8. [2] 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.
  9. [8] 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. [35] A. Kohlhase, M. Kohlhase and M. Fürsich (2017) Visual structure in math expressions. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  2. [45] M. Kohlhase, T. Koprucki, D. Müller and K. Tabelow (2017) Mathematical models as research data via flexiformal theory graphs. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  3. [50] M. Kohlhase, D. Müller, S. Owre and F. Rabe (2017) Making PVS accessible to generic services by interpretation in a universal format. Note: accepted at ITP 2017 External Links: Link Cited by: p1.
  4. [71] 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 mathematics, LNAI. External Links: Link Cited by: p1.
  5. [79] M. Rupprecht, M. Kohlhase and D. Müller (2017) A flexible, interactive theory-graph viewer. In MathUI 2017: the 12th workshop on mathematical user interfaces, A. Kohlhase and M. Pollanen (Eds.), External Links: Link Cited by: p1.
  6. [83] W. Sperber and M. Kohlhase (2017) Software citations, information systems, and beyond. In Intelligent computer mathematics, LNAI. External Links: Link Cited by: p1.
  7. [86] I. Toloaca and M. Kohlhase (2016-07) Notation-based semantification. In Mathematical user interfaces workshop at CICM, A. Kohlhase and P. Libbrecht (Eds.), pp. 73–81. External Links: Link Cited by: p1.
  8. [3] 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 technologies, N. Kando, T. Sakai and M. Sanderson (Eds.), pp. 299–308. External Links: Link Cited by: p1.
  9. [32] C. Kaliszyk, M. Kohlhase, D. Müller and F. Rabe (2016) A standard for aligning mathematical concepts. In Intelligent computer mathematics – work in progress papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, Naumowicz, W. Neuper, P. Quaresma, F. Tompa and M. Suda (Eds.), External Links: Link Cited by: p1.
  10. [78] 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 papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, Naumowicz, W. Neuper, P. Quaresma, F. Tompa and M. Suda (Eds.), External Links: Link Cited by: p1.
  11. [24] R. Hambasan and M. Kohlhase (2015-10) Faceted search for mathematics. In Proceedings 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.
  12. [67] 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 FGDB, R. Bergmann, S. Görg and G. Müller (Eds.), pp. 296–303. External Links: Link Cited by: p1.
  13. [21] D. Ginev, S. Lal, M. Kohlhase and T. Wiesing (2015-07) KAT: an annotation tool for STEM documents. In Mathematical user interfaces workshop at CICM, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  14. [73] N. Pentrel and M. Kohlhase (2015-07) Relational presentations using semantic closeness spatial narrative for mathematical content. In Mathematical user interfaces workshop at CICM, A. Kohlhase and P. Libbrecht (Eds.), External Links: Link Cited by: p1.
  15. [36] A. Kohlhase, M. Kohlhase and A. Guseva (2015) Context in spreadsheet comprehension. In Second workshop on software engineering methods in spreadsheets, External Links: Link Cited by: p1.
  16. [85] A. Toader, M. Kohlhase and A. Kohlhase (2015) Assessment for spreadsheets. In Second workshop on software engineering methods in spreadsheets, External Links: Link Cited by: p1.
  17. [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 2014, 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.
  18. [2] A. Aizawa, M. Kohlhase, I. Ounis and M. Schubotz (2014) NTCIR-11 Math-2 task overview. In NTCIR workshop 11 meeting, N. Kando, H. Joho and K. Kishida (Eds.), pp. 88–98. External Links: Link Cited by: p1.
  19. [8] J. Carette, W. Farmer and M. Kohlhase (2014) Realms: a structure for consolidating knowledge about mathematical theories. In Intelligent computer mathematics, 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.
  20. [23] R. Hambasan, M. Kohlhase and C. Prodescu (2014) MathWebSearch at NTCIR-11. In NTCIR workshop 11 meeting, N. Kando, H. Joho and K. Kishida (Eds.), pp. 114–119. External Links: Link Cited by: p1.
  21. [28] F. Horozal, M. Kohlhase and F. Rabe (2014) Flexary operators for formalized mathematics. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 312–327. External Links: Link Cited by: p1.
  22. [31] M. Iancu, C. Jucovschi, M. Kohlhase and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  23. [41] L. Kohlhase and M. Kohlhase (2014) System description: a semantics-aware LaTeX-to-office converter. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 440–443. External Links: Link Cited by: p1.
  24. [60] M. Kohlhase (2014) A data model and encoding for a semantic, multilingual terminology of mathematics. In Intelligent computer mathematics, S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), LNCS, pp. 169–183. External Links: Link Cited by: p1.
  25. [61] 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 2014, 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.
  26. [62] 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 2014, 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.
  27. [4] A. Aizawa, M. Kohlhase and I. Ounis (2013) NTCIR-10 Math pilot task overview. In NTCIR workshop 10 meeting, N. Kando and K. Kishida (Eds.), pp. 1–8. External Links: Link Cited by: p1.
  28. [7] T. Breitsprecher, M. Codescu, C. Jucovschi, M. Kohlhase, L. Schröder and S. Wartzack (2013) Semantic support for engineering design processes. External Links: Link Cited by: p1.
  29. [16] J. W. Dörrie, M. Kohlhase and L. Linsen (2013) OpenMathMap: accessing math via interactive maps. pp. 81–98. External Links: Link Cited by: p1.
  30. [17] 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 2013, C. Lange, D. Aspinall, J. Carette, J. D. and, M. Kohlhase, P. Libbrecht, P. Q. , F. Rabe, P. Sojka, I. Whiteside and W. Windsteiger (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  31. [51] 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), External Links: Link Cited by: p1.
  32. [52] M. Kohlhase and C. Prodescu (2013) MathWebSearch at NTCIR-10. In NTCIR workshop 10 meeting, N. Kando and K. Kishida (Eds.), pp. 675–679. External Links: Link Cited by: p1.
  33. [58] M. Kohlhase (2013) Knowledge management for systematic engineering design in CAD systems. In Professionelles Wissenmanagement Management, Konferenzbeiträge der 7. Konferenz, F. Lehner, N. Amende and N. Fteimi (Eds.), pp. 202–217. External Links: Link Cited by: p1.
  34. [59] M. Kohlhase (2013) The flexiformalist manifesto. In 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.
  35. [43] M. Kohlhase and M. Iancu (2012) Searching the space of mathematical knowledge. In DML and MIR 2012, P. Sojka and M. Kohlhase (Eds.), External Links: Link Cited by: p1.
  36. [74] 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 proceedings, External Links: Link Cited by: p1.
  37. [10] M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, Rabe and K. Sojakova (2011) Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In Recent Trends in Algebraic Development Techniques, H. Kreowski and T. Mossakowski (Eds.), LNCS. Cited by: p1.
  38. [13] C. David, D. Ginev, M. Kohlhase, B. Matican and 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 Conference, A. García Castro, C. Lange, E. Sandhaus and A. de Waard (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: p1.
  39. [27] F. Horozal, M. Kohlhase and F. Rabe (2011) Extending OpenMath with Sequences. In Intelligent computer mathematics, J. Davenport, W. Farmer, F. Rabe and J. Urban (Eds.), LNAI, pp. 58–72. External Links: Link Cited by: p1.
  40. [40] 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), pp. 181–188. External Links: Link Cited by: p1.
  41. [87] M. Wolska, M. Grigore and M. Kohlhase (2011) Using discourse context to interpret object-denoting mathematical expressions. In Towards digital mathematics library, dml workshop, P. Sojka (Ed.), pp. 85–101. External Links: Link Cited by: p1.
  42. [15] C. David, M. Kohlhase, C. Lange, F. Rabe and Zholudev (2010-06) JOBAD/MMT – interactive mathematics. In AI Mashup Challenge, A. Giurca, B. Endres-Niggemeyer, C. Lange, L. Maicher and P. Hitzler (Eds.), External Links: Link Cited by: p1.
  43. [12] 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 Applications, I. Mierlus-Mazilu (Ed.), External Links: Link Cited by: p1.
  44. [14] C. David, M. Kohlhase, C. Lange, F. Rabe, Zhiltsov and V. Zholudev (2010) Publishing math lecture notes as linked data. In 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.
  45. [18] 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 Conference, C. Lange, J. Reutelshöfer, S. Schaffert and H. Skaf-Molli (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  46. [37] A. Kohlhase, M. Kohlhase and C. Lange (2010) Dimensions of formality: a case study for MKM in software engineering. In Intelligent computer mathematics, S. Autexier, J. Calmet, D. Delahaye, P. D. F. I. and, R. Rioboo and A. P. Sexton (Eds.), LNAI, pp. 355–369. External Links: 1004.5071v1 Cited by: p1.
  47. [22] M. Grigore, M. Wolska and M. Kohlhase (2009-12-14) Towards context-based disambiguation of mathematical expressions. Fukuoka, Japan, pp. 262–271. External Links: ISSN 1881-4042, Link Cited by: p1.
  48. [26] 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: 39, 66.
  49. [39] 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), FGWM, C. Lange and J. Reutelshöfer (Eds.), pp. 22–29. External Links: Link Cited by: p1.
  50. [42] M. Kohlhase, J. Gičeva, C. Lange and V. Zholudev (2009-09) JOBAD – interactive mathematical documents. In AI Mashup Challenge, B. Endres-Niggemeyer, V. Zacharias and P. Hitzler (Eds.), External Links: Link Cited by: p1.
  51. [66] C. Lange and M. Kohlhase (2009-09) A mathematical approach to ontology authoring and documentation. In Wissens- und erfahrungsmanagement (knowledge and experience management), FGWM, C. Lange and J. Reutelshöfer (Eds.), Cited by: p1.
  52. [11] J. H. Davenport and M. Kohlhase (2009-07) Quantifiers and big operators in OpenMath. In 22nd openmath workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  53. [53] M. Kohlhase and F. Rabe (2009-07) Semantics of OpenMath and MathML3. In 22nd openmath workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  54. [65] C. Lange and M. Kohlhase (2009-07) A mathematical approach to ontology authoring and documentation. In MKM/Calculemus proceedings, J. Carette, L. Dixon, C. Sacerdoti Coen and S. M. Watt (Eds.), LNAI, pp. 389–404. External Links: Link Cited by: p1.
  55. [77] F. Rabe and M. Kohlhase (2009-07) A better role system for OpenMath. In 22nd openmath workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1.
  56. [64] C. Lange and M. Kohlhase (2009-06) Documenting ontologies the mathematical way. External Links: Link Cited by: p1.
  57. [20] 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. External Links: Link Cited by: p1.
  58. [84] H. Stamerjohanns, D. Ginev, C. David, D. M. and and M. Kohlhase (2009) MathML-aware article conversion from LaTeX, a comparison study. In Towards digital mathematics library, dml 2009 workshop, P. Sojka (Ed.), pp. 109–120. External Links: Link Cited by: p1.
  59. [38] A. Kohlhase and M. Kohlhase (2008-10) Compensating the semantic bias of spreadsheets. In Wissens- 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.
  60. [72] 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 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.
  61. [69] C. Müller and M. Kohlhase (2008-06) Towards A Community of Practice Toolkit. In 2nd workshop on scientific communities of practice (SCooP-2008), C. Müller (Ed.), Cited by: p1.
  62. [70] C. Müller and M. Kohlhase (2008) Communities of practice in mathematical elearning. pp. 34–35. Cited by: p1.
  63. [75] F. Rabe and M. Kohlhase (2008) An exchange format for modular knowledge. Aachen, pp. 50–68. External Links: ISSN 1613-0073 Cited by: p1.
  64. [76] F. Rabe and M. Kohlhase (2008) An Exchange Format for Modular Knowledge. pp. 50–68. Cited by: p1.
  65. [47] M. Kohlhase, C. Lange and F. Rabe (2007-06) Presenting mathematical content with flexible elisions. In OpenMath/JEM workshop 2007, O. Caprotti, M. Kohlhase and P. Libbrecht (Eds.), Cited by: p1.
  66. [49] 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 MKM, P. Libbrecht (Ed.), Cited by: p1.
  67. [48] 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 proceedings, A. Hinneburg (Ed.), pp. 324–229. Cited by: p1.
  68. [68] C. Müller and M. Kohlhase (2007) Panta rhei. In Wissens- und Erfahrungsmanagement LWA (Lernen, Wissensentdeckung und Adaptivität) conference proceedings, A. Hinneburg (Ed.), pp. 318–323. Cited by: p1.
  69. [63] 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 Conference, M. Völkel, S. Schaffert and S. Decker (Eds.), CEUR Workshop Proceedings. Cited by: p1.
  70. [57] M. Kohlhase (2004) Semantic markup for TeX/LaTeX. In Mathematical user interfaces workshop 2004, P. Libbrecht (Ed.), Cited by: p1.
  71. [9] E. Clarke, M. Kohlhase, J. Ouaknine and K. Sutner (2003) Resurrecting the Analytica theorem prover. In First qpq workshop on deductive software components, Cited by: p1.
  72. [25] B. Han and M. Kohlhase (2003) A time calculus for natural language. In ICoS-4. inference in computational semantics. workshop proceedings, P. Blackburn and J. Bos (Eds.), pp. 113–127. External Links: Link Cited by: p1.
  73. [56] M. Kohlhase (2003) Applying unification techniques to XML document management?. In 17th workshop on unification, Cited by: p1.
  74. [54] 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 web, External Links: Link Cited by: p1.
  75. [88] J. Zimmer and M. Kohlhase (2002) System Description: The MathWeb software bus for distributed mathematical reasoning. In Automated deduction — cade-18, A. Voronkov (Ed.), LNAI, pp. 247–252. External Links: Link Cited by: p1.
  76. [44] M. Kohlhase and A. Koller (2000) Towards a tableaux machine for language understanding. In ICoS-2. inference in computational semantics. workshop proceedings, J. Bos and M. Kohlhase (Eds.), pp. 57–88. Cited by: p1.
  77. [80] 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. Montreal. Cited by: p1.
  78. [6] P. Blackburn, J. Bos and M. Kohlhase (1999) Automated reasoning for computational semantics. Batumi, Georgia. Cited by: p1.
  79. [5] 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”, P. Baumgartner, U. Furbach, M. Kohlhase, W. McCune, W. Reif, M. Stickel and T. Uribe (Eds.), Cited by: p1.
  80. [81] 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 provers, R. C. Backhouse (Ed.), Computing Science Reports, pp. 130–138. Cited by: p1.
  81. [82] 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. Eindhoven, Netherlands. External Links: Link Cited by: p1.
  82. [19] M. Egg and M. Kohlhase (1997) Underspecification of quantifier scope. Heidelberg. External Links: Link Cited by: p1.
  83. [34] M. Kerber and M. Kohlhase (1996) Partiality without the cost. Cited by: p1.
  84. [46] M. Kohlhase, S. Kuschert and M. Pinkal (1996) A type-theoretic semantics for λ-DRT. Amsterdam, pp. 479–498. External Links: Link Cited by: p1.
  85. [29] X. Huang, M. Kerber, M. Kohlhase, D. Nesmith and Richts (1994) Guaranteeing correctness through the communication of checkable proofs (or: would you really trust an automated reasoning system?). Cited by: p1.
  86. [30] 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”, C. W. Wolfgang Bibel (Ed.), Forschungsbericht, FB Informatik, TH Darmstadt, pp. 12–12. Cited by: p1.
  87. [33] M. Kerber and M. Kohlhase (1994) Formalizing mathematics with dependent sorts. Cited by: p1.
  88. [55] M. Kohlhase (1993) Higher-order resolution with combinators. pp. 15. Cited by: p1.

Technical Reports

  1. [32] 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.
  2. [39] 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.
  3. [70] 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.
  4. [9] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. P. , 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.
  5. [10] P. Dehaye, M. Iancu, M. Kohlhase, A. Konovalov, S. Lelièvre, D. Müller, M. P. , 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.
  6. [26] M. Kohlhase, D. Ginev and R. Ambrus (2016) modules.sty: semantic macros and module scoping in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  7. [27] M. Kohlhase and D. Ginev (2016) presentation.sty: an infrastructure for presenting semantic macros in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  8. [28] M. Kohlhase and D. Ginev (2016) smultiling.sty: multilinguality support for sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  9. [29] 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.
  10. [46] M. Kohlhase (2016) Active/structured documents requirements and existing solutions. Deliverable Technical Report D4.2, OpenDreamKit. External Links: Link Cited by: p1.
  11. [47] M. Kohlhase (2016) cmath.sty: an infrastructure for building inline content math in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  12. [48] M. Kohlhase (2016) cmathml.sty: a TeX/LaTeX-based syntax for content MathML. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  13. [49] M. Kohlhase (2016) CNXLaTeX: a LaTeX-based syntax for Connexions modules. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  14. [50] M. Kohlhase (2016) dcm.sty: an infrastructure for marking up Dublin Core metadata in LaTeX documents. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  15. [51] M. Kohlhase (2016) Editorial notes for LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). Cited by: p1.
  16. [52] M. Kohlhase (2016) hwexam.sty/cls: an infrastructure for formatting assignments and exams. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  17. [53] M. Kohlhase (2016) metakeys.sty: a generic framework for extensible metadata in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  18. [54] M. Kohlhase (2016) omdoc.sty/cls: semantic markup for open mathematical documents in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  19. [55] M. Kohlhase (2016) omtext: semantic markup for mathematical text fragments in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  20. [56] M. Kohlhase (2016) owl2onto.cls: marking up OWL2 ontologies in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  21. [57] M. Kohlhase (2016) physml.sty: an infrastructure for marking up PhysML in TeX/LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  22. [58] M. Kohlhase (2016) Preparing dfg proposals and reports in LaTeX with dfgproposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  23. [59] M. Kohlhase (2016) Preparing fp7 eu proposals and reports in LaTeX with euproposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  24. [60] M. Kohlhase (2016) Preparing proposals in LaTeX with proposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  25. [61] M. Kohlhase (2016) problem.sty: an infrastructure for formatting problems. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  26. [62] M. Kohlhase (2016) RDFa metadata in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  27. [63] M. Kohlhase (2016) reqdoc.sty: semantic markup for requirements specification documents. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  28. [64] M. Kohlhase (2016) Slides and course notes. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  29. [65] M. Kohlhase (2016) sproof.sty: structural markup for proofs. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  30. [66] M. Kohlhase (2016) sref.sty: semantic crossreferencing in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  31. [67] M. Kohlhase (2016) statements.sty: structural markup for mathematical statements. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  32. [68] M. Kohlhase (2016) sTeX: semantic markup in TeX/LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  33. [69] M. Kohlhase (2016) workaddress.sty: an infrastructure for marking up Dublin Core metadata in LaTeX documents. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
  34. [74] F. Rabe and M. Kohlhase (2012) An XML-based syntax for MMT. Technical report External Links: Link Cited by: p1.
  35. [19] 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.
  36. [20] M. Iancu, M. Kohlhase and F. Rabe (2011) Translating the Mizar Mathematical Library into OMDoc format. KWARC Report Jacobs University Bremen. Note: https://svn.omdoc.org/repos/latin/public/Mizar2OMDoc-Report.pdf External Links: Link Cited by: p1.
  37. [71] 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.
  38. [76] 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: http://kwarc.info/vzholudev/pubs/XMLPrague_long.pdf External Links: Link Cited by: p1.
  39. [35] 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: http://kwarc.info/publications/papers/KLMMR_NfAD.pdf External Links: Link Cited by: p1.
  40. [25] 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.
  41. [75] H. Stamerjohanns, D. Ginev, C. David, D. M. and and M. Kohlhase (2009) A comparison study of MathML-aware LaTeX converters. KWARC Report Jacobs University Bremen. Note: https://svn.kwarc.info/repos/arXMLiv/doc/dml09/report.pdf External Links: Link Cited by: p1.
  42. [72] 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.
  43. [73] 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.
  44. [34] 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.
  45. [7] 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.
  46. [1] 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.
  47. [2] 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.
  48. [3] 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.
  49. [8] 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.
  50. [38] 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.
  51. [45] 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.
  52. [31] 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.
  53. [6] 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.
  54. [30] 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.
  55. [24] 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.
  56. [4] 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.
  57. [5] 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.
  58. [11] 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.
  59. [33] 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.
  60. [12] 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.
  61. [13] 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.
  62. [14] 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.
  63. [22] 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.
  64. [44] 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.
  65. [15] 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.
  66. [18] 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.
  67. [37] 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.
  68. [42] 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.
  69. [43] M. Kohlhase (1994) Higher-order order-sorted resolution. Seki Report Technical Report SR-94-1, Fachbereich Informatik, Universität des Sarrlandes. Cited by: p1.
  70. [21] 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.
  71. [23] 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.
  72. [41] 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.
  73. [16] 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.
  74. [17] 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.
  75. [40] 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.
  76. [36] M. Kohlhase and C. Prodescu MathWebSearch manual. Web Manual Jacobs University. External Links: Link Cited by: p1.

Unpublished

  1. [17] M. Kohlhase (2017-10) Math object identifiers – towards research data in mathematics. Note: in press External Links: Link Cited by: p1.
  2. [4] T. G. D. M. L. W. Group (2016) International mathematical knowledge trust charter. External Links: Link Cited by: p1.
  3. [8] C. Kaliszyk, M. Kohlhase, D. Müller and F. Rabe (2016) Aligning the libraries of formal mathematical systems. External Links: Link Cited by: p1.
  4. [15] M. Kohlhase (2016) An open markup format for mathematical documents OMDoc [version 1.3]. Note: Draft Specification External Links: Link Cited by: p1.
  5. [16] 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.
  6. [3] D. Ginev, M. Iancu, C. Jucovschi, A. Kohlhase, M. Kohlhase, H. Kröger, J. Schefter and W. Sperber (2015) The SMGLoM project and system. External Links: Link Cited by: p1.
  7. [2] 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.
  8. [1] 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.
  9. [9] 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.
  10. [5] F. Horozal, M. Kohlhase, F. Rabe and K. Sojakova (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
  11. [13] M. Kohlhase (2009) An OMDoc primer [version 1.6 (pre-2.0)]. External Links: Link Cited by: p1.
  12. [14] 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.
  13. [6] M. Iancu, M. Kohlhase, F. Rabe and H. Yuan Mixing surface languages for OMDoc. External Links: Link Cited by: p1.
  14. [7] M. Iancu, M. Kohlhase and F. Rabe Understanding the pragmatics of module systems for mathematics. External Links: Link Cited by: p1.
  15. [10] M. Kohlhase, D. Ginev and V. Merticariu A framework for semantic publishing of modular content objects. External Links: Link Cited by: p1.
  16. [11] M. Kohlhase, D. Müller, M. Pfeiffer, F. R. , N. Thiéry, V. Vasilyev and T. Wiesing REGULAR-t1: knowledge-based interoperability for mathematical software systems. Note: submitted to MACIS-2017 External Links: Link Cited by: p1.
  17. [12] M. Kohlhase CodeML: an open markup format the content and presentatation of program code. External Links: Link Cited by: p1.
  18. [18] A. Toader, M. Kohlhase and A. Kohlhase Assessment for spreadsheets via theory graphs. External Links: Link Cited by: p1.
  19. [19] T. Wiesing, M. Kohlhase and F. Rabe REGULAR-t1: virtual theories – a uniform interface to mathematical knowledge bases. Note: submitted to MACIS-2017 External Links: Link Cited by: p1.

Miscellaneous

  1. [2] 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.
  2. [18] 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.
  3. [3] M. Kohlhase (2011) General Computer Science: GenCS I/II Lecture Notes. Semantic Course Notes in Panta Rhei. External Links: Link Cited by: p1.
  4. [4] M. Kohlhase (2011) General Computer Science; 320101: GenCS I Lecture Notes. External Links: Link Cited by: p1.
  5. [5] M. Kohlhase (2011) General Computer Science; Problems and Solutions for 320101 GenCS I. External Links: Link Cited by: p1.
  6. [6] M. Kohlhase (2011) General Computer Science; Problems for 320101 GenCS I. External Links: Link Cited by: p1.
  7. [7] M. Kohlhase (2011) General Computer Science: 320201 GenCS II Lecture Notes. External Links: Link Cited by: p1.
  8. [8] M. Kohlhase (2011) General Computer Science: Problems and Solutions for 320201 GenCS II. External Links: Link Cited by: p1.
  9. [9] M. Kohlhase (2011) General Computer Science: Problems for 320201 GenCS II. External Links: Link Cited by: p1.
  10. [16] M. Kohlhase and L. Schroeder (2011) The FormalCAD Project. External Links: Link Cited by: p1.
  11. [1] 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.
  12. [12] M. Kohlhase, T. Mossakowski and F. Rabe (2009) The LATIN Project. External Links: Link Cited by: p1.
  13. [11] D. Hutter and M. Kohlhase (2006) Ontology-driven management of change. External Links: Link Cited by: p1.
  14. [13] M. Kohlhase and D. Carlisle (2003) Guidelines for graphics in MathML 2. Note: W3C Note External Links: Link Cited by: p1.
  15. [14] M. Kohlhase and S. Devitt (2003) Bound variables in MathML. Note: W3C Working Group Note External Links: Link Cited by: p1.
  16. [15] M. Kohlhase and S. Devitt (2003) Structured types in MathML 2.0. Note: W3C Note External Links: Link Cited by: p1.
  17. [17] M. Kohlhase (2001) OMDoc: an open markup format for mathematical documents (version 1.1). Open Specification. External Links: Link Cited by: p1.
  18. [10] 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.
  19. [19] Open digital research environment toolkit for the advancement of mathematics. Project Proposal. External Links: Link Cited by: p1.