Please respect any copyrights when downloading

- [3] (2020) (Deep) fair mathematics. it – Information Technology 62 (1), pp. 7–17. External Links: Document, Link Cited by: p1.
- [6] (2020) Big math and the one-brain barrier – the tetrapod model of mathematical knowledge. Mathematical Intelligencer. External Links: Document Cited by: p1.
- [32] (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.
- [26] (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.
- [31] (2014-06) Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. EMS Newsletter, pp. 22–27. External Links: Link Cited by: p1.
- [22] (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.
- [24] (2013-09) Zentralblatt column: mathematical formula search. EMS Newsletter, pp. 56–57. External Links: Link Cited by: p1.
- [13] (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.
- [19] (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.
- [34] (2013) A scalable module system. Information & Computation 0 (230), pp. 1–54. External Links: Link Cited by: p1.
- [17] (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.
- [25] (2012) Semantics of OpenMath and MathML3. Mathematics in Computer Science 6 (3), pp. 235–260. External Links: Link Cited by: p1.
- [20] (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.
- [37] (2010) Conversion d’articles en LaTeX vers XML avec MathML : une étude comparative. Cahiers GUTenberg 51, pp. 7–28. External Links: Link Cited by: p1.
- [38] (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] (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.
- [2] (2009) Cut-simulation and impredicativity. Logical Methods in Computer Science 5 (1), pp. 1–21. External Links: Link Cited by: p1.
- [33] (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.
- [18] (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.
- [30] (2008) Using LaTeX as a semantic markup format. Mathematics in Computer Science 2 (2), pp. 279–304. External Links: Link Cited by: p1.
- [1] (2004) Higher order semantics and extensionality. Journal of Symbolic Logic 69, pp. 1027–1088. External Links: Link Cited by: p1.
- [4] (2004) Inference and computational semantics. Journal of Logic, Language and Information 13 (2), pp. 117–120. External Links: Link Cited by: p1.
- [14] (2004) eLearning-, eTeaching- & eResearch-technologien – Chancen und Potentiale für die Mathematik. Mitteilungen der DMV 12 (2). External Links: Link Cited by: p1.
- [5] (2003) Editorial. Logic Journal of the IGPL 11 (4), pp. 381–384. Cited by: p1.
- [23] (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.
- [21] (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.
- [12] (2000) Managing structural information by higher-order colored unification. Journal of Automated Reasoning 25 (2), pp. 123–164. External Links: Link Cited by: p1.
- [29] (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.
- [8] (1999) Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science 5, pp. 156–187. External Links: Link Cited by: p1.
- [9] (1999) MBase: representing mathematical knowledge in a relational data base. Electronic Notes Theoretical Computer Science 23 (3). Cited by: p1.
- [10] (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.
- [27] (1999) Higher-order multi-valued resolution. Journal of Applied Non-Classical Logics 9. External Links: Link Cited by: p1.
- [35] (1999) L$\mathrm{\Omega}$UI: lovely $\mathrm{\Omega}$mega user interface. Formal Aspects of Computing 3 (11), pp. 326–342. External Links: Link Cited by: p1.
- [7] (1998) Steuerung der Inferenz in der Diskursverarbeitung. Kognitionswissenschaft 7 (3), pp. 106–110. External Links: Link Cited by: p1.
- [15] (1998) Integrating computer algebra into proof planning. Journal of Automated Reasoning 21 (3), pp. 327–355. External Links: Link Cited by: p1.
- [36] (1998) $\mathrm{\Omega}$mega, ein mathematisches Assistenzsystem. Kognitionswissenschaft 7 (3), pp. 101–105. External Links: Link Cited by: p1.
- [11] (1996) Die Beweisentwicklungsumgebung $\mathrm{\Omega}$mega. Informatik – Forschung und Entwicklung 11, pp. 20–26. Cited by: p1.
- [16] (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.
- [28] (1996) Sorten für das automatische Beweisen höherer Stufe. Künstliche Intelligenz. Cited by: p1.

- [2] (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.
- [19] (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.
- [7]
(2009)
Compensating the computational bias of spreadsheets.
In Festschrift in honour of Bernd Krieg-Brückner’s 60
^{th}birthdayFestschrift in Honour of Bernd Krieg-Brückner’s 60^{th}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. - [8]
(2009)
Formal management of CAD/CAM processes.
In Festschrift in honour of Bernd Krieg-Brückner’s 60
^{th}birthdayFestschrift in Honour of Bernd Krieg-Brückner’s 60^{th}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. - [18] (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.
- [4]
(2008)
Cut elimination with xi-functionality.
In Festschrift in honour of Peter B. Andrews on his 70
^{th}birthday, C. Benzmüller, C. Brown, J. Siekmann, and R. Statman (Eds.), External Links: Link Cited by: p1. - [16] (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.
- [3] (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.
- [6] (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] (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.
- [15] (2006-08) STeX: a LaTeX-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.
- [17] (2006-08) SWiM – an OMDoc-based semantic wiki. In OMDoc – an open markup format for mathematical documents [version 1.2], LNAI. Cited by: p1.
- [13] (2003) Artificial intelligence: automated reasoning. In Van Nostrand’s Scientific Encyclopedia, pp. 247–250. Cited by: p1.
- [5] (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.
- [9] (1999) $\mathrm{\Omega}$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.
- [1] (1998) M. Kohlhase, W. Bibel, and P. Schmitt (Eds.), Cited by: p1.
- [11] (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.
- [12] (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.
- [10] (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.

- [11] (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.
- [75] (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: Link Cited by: p1.
- [88] (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.
- [109] (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.
- [114] (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.
- [118] (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.
- [2] (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.
- [10] (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.
- [20] (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.
- [12] (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.
- [60] (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.
- [112] (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.
- [113] (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.
- [117] (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.
- [56] (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.
- [78] (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.
- [84] (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.
- [85] (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.
- [111] (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.
- [120] (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.
- [122] (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.
- [24] (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.
- [32] (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.
- [34] (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.
- [108] (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.
- [48] (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.
- [49] (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.
- [91] (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.
- [14] (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.
- [15] (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.
- [40] (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.
- [46] (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.
- [47] (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.
- [73] (2014) System description: a semantics-aware LaTeX-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.
- [76] (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.
- [104] (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.
- [57] (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.
- [81] (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.
- [87] (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.
- [102] (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.
- [103] (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.
- [22] (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.
- [39] (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] (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.
- [101] (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.
- [105] (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.
- [1] (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.
- [5] (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.
- [17] (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.
- [18] (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.
- [19] (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 Cited by: p1.
- [33] (2011) The LaTeXML 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.
- [37] (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.
- [38] (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.
- [70]
(2011)
Maintaining islands of consistency via versioned links.
In Proceedings of the 29
^{th}annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29^{th}annual ACM international conference on Design of communication (SIGDOC), pp. 167–174. External Links: Link Cited by: p1. - [71] (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.
- [72]
(2011)
Towards a flexible notion of document context.
In Proceedings of the 29
^{th}annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29^{th}annual ACM international conference on Design of communication (SIGDOC), pp. 181–188. External Links: Link Cited by: p1. - [89] (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] (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.
- [23] (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.
- [51] (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: 1005.5489v1 Cited by: p1.
- [58] (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.
- [59]
(2010)
sTeX – a system for flexible formalization of linked data.
In 6
^{th}international conference on semantic systems (I-Semantics) and the 5^{th}international conference on pragmatic webProceedings of the 6^{th}International Conference on Semantic Systems (I-Semantics) and the 5^{th}International Conference on Pragmatic Web, A. Paschke, N. Henze, T. Pellegrini, and H. Weigand (Eds.), External Links: 1006.4474v1, Document Cited by: p1. - [69] (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.
- [90] (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.
- [124] (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.
- [21] (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.
- [65] (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.
- [66] (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.
- [107] (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.
- [67]
(2009)
Modeling task experience in user assistance systems.
In Proceedings of the 27
^{th}annual ACM international conference on design of communication (SIGDOC)Proceedings of the 27^{th}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. - [68]
(2009)
Semantic transparency in user assistance systems.
In Proceedings of the 27
^{th}annual ACM international conference on design of communication (SIGDOC)Proceedings of the 27^{th}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. - [80]
(2009)
Formal management of CAD/CAM processes.
In 16
^{th}international symposium on formal methods (FM 2009)16^{th}International Symposium on Formal Methods (FM 2009), A. Cavalcanti and D. Dams (Eds.), LNCS, pp. 223–238. External Links: Link Cited by: p1. - [123] (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.
- [83] (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.
- [110]
(2008)
Towards a community of practice toolkit based on semantically marked up artifacts.
In Proceedings of the 1
^{st}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. - [121] (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.
- [64]
(2007)
*Re*examining the MKM Value Proposition: From Math Web Search to Math Web*Re*Search. 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. - [115] (2007) Extended formula normalization for $\u03f5$-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.
- [7] (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.
- [36] (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.
- [62] (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.
- [63] (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.
- [92] (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.
- [100] (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.
- [61] (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.
- [16]
(2003-09)
System description: analytica 2.
In 11
^{th}symposium on the integration of symbolic computation and mechanized reasoning (Calculemus 2003)Proceedings of the 11^{th}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. - [74] (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.
- [4] (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.
- [93] (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.
- [119] (2002) Proof development with $\mathrm{\Omega}$mega. In Automated deduction — cade-18Automated Deduction — CADE-18, A. Voronkov (Ed.), LNAI, pp. 144–149. Cited by: p1.
- [125] (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.
- [98] (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.
- [99] (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.
- [3]
(2000)
Communication protocols for mathematical services based on KQML and OMRS.
In CALCULEMUS-2000, systems for integrated computation and deductionProceedings of the 8
^{th}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. - [27] (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.
- [77] (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.
- [97]
(2000)
Model generation for discourse representation theory.
In Proceedings of of the 14
^{th}european conference on artifical intelligenceProceedings of of the 14^{th}European Conference on Artifical Intelligence, W. Horn (Ed.), pp. 441–445. External Links: Link Cited by: p1. - [116]
(2000)
Feature logic for dotted types: a formalism for complex word meanings.
In Proceedings of the 38
^{th}Annual Meeting of the Association for Computational Linguistics, Hongkong, pp. 521–528. External Links: Link Cited by: p1. - [13] (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.
- [26] (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.
- [35]
(1998-07)
An implementation of distributed mathematical services.
In 6
^{th}calculemus and types workshop6^{th}CALCULEMUS and TYPES Workshop, A. Cohen and H. Barendregt (Eds.), Cited by: p1. - [8]
(1998)
Extensional higher order resolution.
In Proceedings of the 15
^{th}Conference on Automated DeductionProceedings of the 15^{th}Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 56–72. External Links: Link Cited by: p1. - [9]
(1998)
LEO – a higher order theorem prover.
In Proceedings of the 15
^{th}Conference on Automated DeductionProceedings of the 15^{th}Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI, pp. 139–144. External Links: Link Cited by: p1. - [6]
(1997)
$\mathrm{\Omega}$mega: towards a mathematical assistant.
In Proceedings of the 14
^{th}Conference on Automated DeductionProceedings of the 14^{th}Conference on Automated Deduction, W. McCune (Ed.), LNAI, pp. 252–255. External Links: Link Cited by: p1. - [25]
(1997)
Dynamic control of quantifier scope.
In Proceedings of the 11
^{th}Amsterdam Colloquium, P. Dekker (Ed.), Amsterdam, The Netherlands, pp. 109–114. Cited by: p1. - [31]
(1997)
Computing parallelism in discourse.
In Proceedings of the 15
^{th}International Joint Conference on Artificial Intelligence (IJCAI)Proceedings of the 15^{th}International Joint Conference on Artificial Intelligence (IJCAI), M. E. Pollack (Ed.), pp. 1016–1021. External Links: Link Cited by: p1. - [45]
(1997)
A coloured version of the $\lambda $-calculus.
In Proceedings of the 14
^{th}Conference on Automated DeductionProceedings of the 14^{th}Conference on Automated Deduction, W. McCune (Ed.), LNAI, pp. 291–305. Cited by: p1. - [55] (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.
- [79]
(1997)
Dynamic lambda calculus.
In Proceedings of the 5
^{th}Meeting on Mathematics of Language – MOL5, pp. 85–92. Cited by: p1. - [54]
(1996-08)
A resolution calculus for presuppositions.
In Proceedings of the 12
^{th}european conference on artificial intelligenceProceedings of the 12^{th}European Conference on Artificial Intelligence, W. Wahlster (Ed.), pp. 375–379. External Links: Link Cited by: p1. - [28] (1996) Corrections and higher-order unification. In Proceedings of KONVENS’96, Bielefeld, Germany, pp. 268–279. External Links: Link Cited by: p1.
- [29]
(1996)
Focus and higher–order unification.
In Proceedings of the 16
^{th}International Conference on Computational Linguistics, Copenhagen, pp. 268–279. External Links: Link Cited by: p1. - [30]
(1996)
Higher–order coloured unification and natural language semantics.
In Proceedings of the 34
^{th}Annual Meeting of the Association for Computational Linguistics, Santa Cruz, pp. 1–9. External Links: Link Cited by: p1. - [52] (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.
- [96] (1995) Higher-order tableaux. In Proceedings of the Tableau Workshop, Koblenz, Germany, pp. 294–309. External Links: Link Cited by: p1.
- [41]
(1994)
KEIM: a toolkit for automated deduction.
In Proceedings of the 12
^{th}Conference on Automated DeductionProceedings of the 12^{th}Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 807–810. External Links: Link Cited by: p1. - [42]
(1994)
$\mathrm{\Omega}$-MKRP a proof development environment.
In Proceedings of the 12
^{th}Conference on Automated DeductionProceedings of the 12^{th}Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 788–792. External Links: Link Cited by: p1. - [43]
(1994)
Adapting methods to novel tasks in proof planning.
In 18
^{th}annual german conference on aritificial intelligence18^{th}Annual German Conference on Aritificial Intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 379–390. External Links: Link Cited by: p1. - [44]
(1994)
A colored version of the $\lambda $ calculus.
In Proceedings of the 12
^{th}Conference on Automated DeductionProceedings of the 12^{th}Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 291–305. Cited by: p1. - [50]
(1994)
Unification in an extensional lambda calculus with ordered function sorts and constant overloading.
In Proceedings of the 12
^{th}Conference on Automated DeductionProceedings of the 12^{th}Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 620–634. External Links: Link Cited by: p1. - [53]
(1994)
A mechanization of strong Kleene logic for partial functions.
In Proceedings of the 12
^{th}Conference on Automated DeductionProceedings of the 12^{th}Conference on Automated Deduction, A. Bundy (Ed.), LNAI, pp. 371–385. External Links: Link Cited by: p1. - [95]
(1994)
Unification in a $\lambda $-calculus with term declarations and function sorts.
In 18
^{th}annual german conference on aritificial intelligence18^{th}Annual German Conference on Aritificial Intelligence, B. Nebel and L. Dreschler-Fischer (Eds.), LNAI, pp. 331–342. External Links: Link Cited by: p1. - [86] (1993) Unification in a $\lambda $-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.
- [94] (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.

- [1] (2006-08) OMDoc – an open markup format for mathematical documents [version 1.2]. LNAI, Springer Verlag. External Links: Link Cited by: p1.

- [5] 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.
- [3] 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.
- [6] M. Kohlhase (Ed.) (2006) Mathematical knowledge management, MKM’05. LNAI, Springer Verlag. Cited by: p1.
- [2] 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.
- [1] J. Bos and M. Kohlhase (Eds.) (2000) ICoS-2. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
- [4] M. Kerber and M. Kohlhase (Eds.) (2000) CALCULEMUS-2000, systems for integrated computation and deduction. AKPeters, St. Andrews, Scotland. Cited by: p1.

- [2] (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.
- [1] (1989) Eine hinreichende Bedingung für die starke, homologische Minimalität von kompakten, $\mathcal{F}$-extremalen Hyperflächen in glatten Mannigfaltigkeiten. Master’s Thesis, Universität Bonn. External Links: Link Cited by: p1.

- [7] 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.
- [6] 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.
- [9] 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.
- [10] 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.
- [11] 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.
- [5]
O. Caprotti, S. Xambó, M. Huertas, M. Kohlhase, and M. Seppälä (Eds.) (2008)
3
^{rd}JEM workshop – joining educational mathematics. External Links: Link Cited by: p1. - [4] 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.
- [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.
- [3] P. Blackburn and M. Kohlhase (Eds.) (2001) ICoS-3. inference in computational semantics. workshop proceedings. Computational Linguistics, Saarland University. Cited by: p1.
- [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.
- [8] J. Denzinger, M. Kohlhase, and B. Spencer (Eds.) (1998) CADE-15 workshop “using AI methods in deduction”. Cited by: p1.

- [81] (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.
- [83] (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.
- [51] (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.
- [52] (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.
- [63] (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.
- [72] (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.
- [82] (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.
- [62] (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.
- [80] (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.
- [89] (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.
- [3] (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.
- [32] (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.
- [79] (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.
- [24] (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.
- [68] (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.
- [21] (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.
- [74] (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.
- [35] (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.
- [88] (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.
- [1] (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.
- [2] (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.
- [8] (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.
- [23] (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.
- [28] (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.
- [31] (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.
- [40] (2014) System description: a semantics-aware LaTeX-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.
- [59] (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.
- [60] (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.
- [61] (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.
- [4] (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.
- [7] (2013) Semantic support for engineering design processes. In Proc. 13th International Design Conference, DESIGN 2014, External Links: Link Cited by: p1.
- [16] (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.
- [17] (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.
- [48] (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.
- [49] (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.
- [57] (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.
- [58] (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.
- [42] (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.
- [75] (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.
- [10] (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.
- [13]
(2011)
A framework for modular semantic publishing with separate compilation and dynamic linking.
In Proceedings of the 1
^{st}workshop on semantic publication, Extended Semantic Web Conference1^{st}Workshop on Semantic Publication (SePublica), A. García Castro, C. Lange, E. Sandhaus, and A. de Waard (Eds.), CEUR Workshop Proceedings. Cited by: p1. - [27] (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.
- [39]
(2011)
Towards a flexible notion of document context.
In Proceedings of the 29
^{th}annual ACM international conference on design of communication (SIGDOC)Proceedings of the 29^{th}annual ACM international conference on Design of communication (SIGDOC), pp. 181–188. External Links: Link Cited by: p1. - [90] (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.
- [15] (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.
- [12]
(2010)
eMath 3.0: building blocks for a social and semantic web for online mathematics & ELearning.
In 1
^{st}International Workshop on Mathematics and ICT: Education, Research and Applications1^{st}International Workshop on Mathematics and ICT: Education, Research and Applications, I. Mierlus-Mazilu (Ed.), External Links: Link Cited by: p1. - [14] (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.
- [18]
(2010)
Prototyping a browser for a listed buildings database with Semantic MediaWiki.
In Proceedings of the 5
^{th}workshop on semantic wikis, Extended Semantic Web Conference5^{th}Workshop on Semantic Wikis, C. Lange, J. Reutelshöfer, S. Schaffert, and H. Skaf-Molli (Eds.), CEUR Workshop Proceedings. Cited by: p1. - [36] (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.
- [22] (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.
- [26] (2009-09) LWA 2009; Workshop-Woche: Lernen – Wissen – Adaptivität. Technical report Vol. TUD-KE-2009-04, Universität Darmstadt. Cited by: 38, 67.
- [38] (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.
- [41] (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.
- [67] (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.
- [11]
(2009-07)
Quantifiers and big operators in OpenMath.
In 22
^{nd}openmath workshop22^{nd}OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1. - [50]
(2009-07)
Semantics of OpenMath and MathML3.
In 22
^{nd}openmath workshop22^{nd}OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1. - [66] (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.
- [78]
(2009-07)
A better role system for OpenMath.
In 22
^{nd}openmath workshop22^{nd}OpenMath Workshop, J. H. Davenport (Ed.), External Links: Link Cited by: p1. - [65]
(2009-06)
Documenting ontologies the mathematical way.
In Poster Proceedings of the 6
^{th}European Semantic Web Conference (ESWC), External Links: Link Cited by: p1. - [20] (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.
- [87] (2009) MathML-aware article conversion from LaTeX, 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.
- [37] (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.
- [73] (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.
- [70]
(2008-06)
Towards A Community of Practice Toolkit.
In 2
^{nd}workshop on scientific communities of practice (SCooP-2008)Proceedings of the 2^{nd}SCooP Workshop, C. Müller (Ed.), Cited by: p1. - [71] (2008) Communities of practice in mathematical elearning. In In proceedings of the Workshop in Mathematical and Scientific eContent, pp. 34–35. Cited by: p1.
- [76]
(2008)
An exchange format for modular knowledge.
In Proceedings of the LPAR Workshops: Knowledge Exchange:
Automated Provers and Proof Assistants, and The 7
^{th}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. - [77] (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.
- [45] (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.
- [47] (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.
- [46] (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.
- [69] (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.
- [64]
(2006)
A semantic wiki for mathematical knowledge management.
In Proceedings of the 1
^{st}workshop on semantic wikis, European Semantic Web Conference1^{st}Workshop on Semantic Wikis, M. Völkel, S. Schaffert, and S. Decker (Eds.), CEUR Workshop Proceedings. Cited by: p1. - [56] (2004) Semantic markup for TeX/LaTeX. In Mathematical user interfaces workshop 2004Mathematical User Interfaces, P. Libbrecht (Ed.), Cited by: p1.
- [9] (2003) Resurrecting the Analytica theorem prover. In First qpq workshop on deductive software componentsFirst QPQ Workshop on Deductive Software Components, Cited by: p1.
- [25] (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.
- [55]
(2003)
Applying unification techniques to XML document management?.
In 17
^{th}workshop on unification17^{th}Workshop on Unification, Cited by: p1. - [53] (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.
- [91] (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.
- [43] (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.
- [84] (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.
- [6] (1999) Automated reasoning for computational semantics. In The Third International Tbilisi Symposium on Language, Logic and Computation, Batumi, Georgia. Cited by: p1.
- [5] (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.
- [85] (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.
- [86] (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.
- [19] (1997) Underspecification of quantifier scope. In Proceedings der 6. Fachtagung der Sektion Computerlinguistik der DGfS, Heidelberg. External Links: Link Cited by: p1.
- [34] (1996) Partiality without the cost. In Workshop on “Mechanization of Partial Functions” at CADE-13, Cited by: p1.
- [44]
(1996)
A type-theoretic semantics for $\lambda $-DRT.
In Proceedings of the 10
^{th}Amsterdam Colloquium, P. Dekker and M. Stokhof (Eds.), Amsterdam, pp. 479–498. External Links: Link Cited by: p1. - [29] (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.
- [30]
(1994)
A test for evaluating the practical usefulness of deduction systems.
In Informal Proc. of the 11
^{th}Annual Meeting of the “GI-Fachgruppe Deduktionssysteme”Informal Proc. of the 11^{th}Annual Meeting of the “GI-Fachgruppe Deduktionssysteme”, C. W. Wolfgang Bibel (Ed.), Forschungsbericht, FB Informatik, TH Darmstadt, pp. 12–12. Cited by: p1. - [33] (1994) Formalizing mathematics with dependent sorts. In Proceedings des Deduktionstreffen, AIDA-Report. Cited by: p1.
- [54] (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.

- [29] (2020) modules.sty: semantic macros and module scoping in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [30] (2020) presentation.sty: an infrastructure for presenting semantic macros in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [31] (2020) smultiling.sty: multilinguality support for sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [54] (2020) cmath.sty: an infrastructure for building inline content math in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [55] (2020) cmathml.sty: a TeX/LaTeX-based syntax for content MathML. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [56] (2020) CNXLaTeX: a LaTeX-based syntax for Connexions modules. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [57] (2020) 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.
- [58] (2020) Editorial notes for LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [59] (2020) hwexam.sty/cls: an infrastructure for formatting assignments and exams. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [60] (2020) MathHub support for s\tex. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [61] (2020) metakeys.sty: a generic framework for extensible metadata in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [62] (2020) omdoc.sty/cls: semantic markup for open mathematical documents in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [63] (2020) omtext: semantic markup for mathematical text fragments in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [64] (2020) owl2onto.cls: marking up OWL2 ontologies in sTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [65] (2020) physml.sty: an infrastructure for marking up PhysML in TeX/LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [66] (2020) Preparing dfg proposals and reports in LaTeX with dfgproposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [67] (2020) Preparing fp7 eu proposals and reports in LaTeX with euproposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [68] (2020) Preparing proposals in LaTeX with proposal.cls. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [69] (2020) problem.sty: an infrastructure for formatting problems. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [70] (2020) RDFa metadata in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [71] (2020) reqdoc.sty: semantic markup for requirements specification documents. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [72] (2020) Slides and course notes. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [73] (2020) sproof.sty: structural markup for proofs. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [74] (2020) sref.sty: semantic crossreferencing in LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [75] (2020) statements.sty: structural markup for mathematical statements. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [76] (2020) sTeX: semantic markup in TeX/LaTeX. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [77] (2020) structview.sty: structures and views in s\tex. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [78] (2020) tikzinput: selective input of tikz diagrams. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [79] (2020) 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.
- [86] (2020) pathsuris.sty: paths and uris for s\tex. Technical report Comprehensive TeX Archive Network (CTAN). External Links: Link Cited by: p1.
- [1] (2018) Notebook import into mathhub.info (interactive display). Deliverable Technical Report D4.11, OpenDreamKit. External Links: Link Cited by: p1.
- [10] (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.
- [11] (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.
- [35] (2017) Mathematical models as research data via flexiformal theory graphs. WIAS Preprint Technical Report 2385. External Links: Document Cited by: p1.
- [42] (2017) In-place computation in active documents (context/computation). Deliverable Technical Report D4.9, OpenDreamKit. External Links: Link Cited by: p1.
- [53] (2017) Distributed, collaborative, versioned editing of active documents in mathhub.info. Deliverable Technical Report D4.3, OpenDreamKit. External Links: Link Cited by: p1.
- [80] (2017) Model pathway diagrams for the representation of mathematical models. WIAS Preprint Technical Report 2431. External Links: Document Cited by: p1.
- [12] (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.
- [13] (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.
- [32] (2016) Full-text search (formulae + keywords) over latex-based documents. Deliverable Technical Report D6.1, OpenDreamKit. External Links: Link Cited by: p1.
- [52] (2016) Active/structured documents requirements and existing solutions. Deliverable Technical Report D4.2, OpenDreamKit. External Links: Link Cited by: p1.
- [51] M. Kohlhase (Ed.) (2015) Formats for topics and submissions for the math-3 task at ntcir-12. Technical report NTCIR. Cited by: p1.
- [50] 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.
- [49] M. Kohlhase (Ed.) (2012) Topics for the NTCIR-10 math task; math retrieval subtask. Technical report NTCIR. External Links: Link Cited by: p1.
- [84] (2012) An XML-based syntax for MMT. Technical report Cited by: p1.
- [22] (2011) Translating the Mizar Mathematical Library into OMDoc format. Technical report Technical Report KWARC Report-01/11, Jacobs University Bremen. Cited by: p1.
- [23] (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.
- [81] D. 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.
- [87] (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.
- [38] (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.
- [28] (2009) Notations for Active Mathematical Documents. Technical report Technical Report 2009-1, Jacobs University Bremen. Cited by: p1.
- [85] (2009) A comparison study of MathML-aware LaTeX converters. KWARC Report Jacobs University Bremen. Cited by: p1.
- [82] (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.
- [83] (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.
- [37] (2008-04) Adaptation of notations in living mathematical documents. KWARC Report Technical Report 2008-2, Jacobs University Bremen. External Links: Link Cited by: p1.
- [8] (2004) The Open Math standard, version 2.0. Technical report The OpenMath Society. External Links: Link Cited by: p1.
- [2] (2003) Prototype n. d2.b document type descriptors: OMDoc proofs. MoWGLI Deliverable The MoWGLI Project. Cited by: p1.
- [3] (2003) Distributed knowledge management and version control. Deliverable Technical Report D5.a, The MoWGLI Project. Cited by: p1.
- [4] (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.
- [9] D. 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.
- [41] (2002) Interpreting negatives in discourse. Technical report Technical Report CMU-PHIL-127, Philosophy, Carnegie Mellon University. External Links: Link Cited by: p1.
- [48] (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.
- [34] (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.
- [7] (1998) Inference and computational semantics. CLAUS Report Technical Report 99, University of the Saarland, Saarbrücken. Cited by: p1.
- [33] (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.
- [27] (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.
- [5] (1997) Model existence for higher-order logic. SEKI-Report Technical Report SR-97-09, Universität des Saarlandes. Cited by: p1.
- [6] (1997) Resolution for henkin models. SEKI-Report Technical Report SR-97-10, Universität des Saarlandes. Cited by: p1.
- [14] (1997) Higher–order coloured unification: a linguistic application. CLAUS Report Technical Report 97, University of the Saarland, Saarbrücken. Cited by: p1.
- [36] (1997) Dynamic lambda calculus. Technical report CLAUS-Report 91, Universität des Saarlandes, Computer Linguistics, Saarland University. Cited by: p1.
- [15] (1996) Corrections and higher-order unification. CLAUS Report Technical Report 77, University of the Saarland, Saarbrücken. Cited by: p1.
- [16] (1996) Focus and higher–order coloured unification. CLAUS Report Technical Report 75, University of the Saarland, Saarbrücken. Cited by: p1.
- [17] (1996) Higher–order coloured unification and natural language semantics. CLAUS Report Technical Report 76, University of the Saarland, Saarbrücken. Cited by: p1.
- [25] (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.
- [47] (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.
- [18] (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.
- [21] (1995) A coloured version of the $\lambda $-calculus. Technical Report Technical Report SR-95-05, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
- [40] (1995) Higher-order multi-valued resolution. SEKI Report Technical Report SR-95-04, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken. Cited by: p1.
- [45] (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.
- [46] (1994) Higher-order order-sorted resolution. Seki Report Technical Report SR-94-1, Fachbereich Informatik, Universität des Sarrlandes. Cited by: p1.
- [24] (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.
- [26] (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.
- [44] (1993) A unifying principle for extensional higher-order logic. Technical Report Technical Report 93–153, Dept. of Mathematics, Carnegie Mellon University. Cited by: p1.
- [19] (1992) $\mathrm{\Omega}$-MKRP – a proof development environment. Technical Report Technical Report SR-92-22, Universität des Saarlandes. Cited by: p1.
- [20] (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.
- [43] (1991) Order-sorted type theory I: unification. SEKI-Report Technical Report SR-91-18 (SFB), Universität des Saarlandes, Saarbrücken. Cited by: p1.
- [39] MathWebSearch manual. Web Manual Jacobs University. External Links: Link Cited by: p1.

- [2] (2020) The space of mathematical software systems – a survey of paradigmatic systems. Note: preprint; http://arxiv.org/abs/2002.04955 Cited by: p1.
- [8] (2020) Linebreaking formulae – an eye-tracking study. External Links: Link Cited by: p1.
- [11] (2020) Logic-independent proof search in logical frameworks (extended report). Note: extended report of conference submission External Links: Link Cited by: p1.
- [12] (2020) Experiences from exporting major proof assistant libraries. Note: under review External Links: Link, 2005.03089 Cited by: p1.
- [13] (2020) Argumentation via context graphs. Cited by: p1.
- [22] (2020) Context graphs for legal reasoning and argumentation. External Links: 2007.00732, Link Cited by: p1.
- [4] (2016) International mathematical knowledge trust charter. External Links: Link Cited by: p1.
- [6] (2016) Mixing surface languages for OMDoc. External Links: Link Cited by: p1.
- [7] (2016) Understanding the pragmatics of module systems for mathematics. External Links: Link Cited by: p1.
- [19] (2016) An open markup format for mathematical documents OMDoc [version 1.3]. Note: Draft Specification External Links: Link Cited by: p1.
- [20] (2016) An open markup format for mathematical documents OMDoc [version 1.6 (pre-2.0)]. Note: Draft Specification External Links: Link Cited by: p1.
- [23] (2015) Assessment for spreadsheets via theory graphs. External Links: Link Cited by: p1.
- [3] (2014) System description: KAT an annotation tool for STEM documents. External Links: Link Cited by: p1.
- [18] (2014) SMGloM primer. Note: SMGloM Blue Note External Links: Link Cited by: p1.
- [1] (2013) Towards ontological support for principle solutions in mechanical engineering. External Links: Link Cited by: p1.
- [10] (2013) A framework for semantic publishing of modular content objects. External Links: Link Cited by: p1.
- [9] (2012) A framework for semantic publishing of modular content objects. External Links: Link Cited by: p1.
- [5] (2010) Towards an atlas of logics. External Links: Link Cited by: p1.
- [16] (2009) An OMDoc primer [version 1.6 (pre-2.0)]. External Links: Link Cited by: p1.
- [17] (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.
- [14] CodeML: an open markup format the content and presentatation of program code. External Links: Link Cited by: p1.
- [15] The theorem prover museum – conserving the system heritage of automated reasoning. External Links: Link Cited by: p1.
- [21] TGView3D system description: 3-dimensional visualization of theory graphs. External Links: Link Cited by: p1.

- [18] (2020) Logic-based natural language processing. External Links: Link Cited by: p1.
- [2] (2014) KAT: an annotation tool for STEM documents; manual. External Links: Link Cited by: p1.
- [19] (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] (2011) General Computer Science: GenCS I/II Lecture Notes. Semantic Course Notes in Panta Rhei. External Links: Link Cited by: p1.
- [4] (2011) General Computer Science; 320101: GenCS I Lecture Notes. External Links: Link Cited by: p1.
- [5] (2011) General Computer Science; Problems and Solutions for 320101 GenCS I. External Links: Link Cited by: p1.
- [6] (2011) General Computer Science; Problems for 320101 GenCS I. External Links: Link Cited by: p1.
- [7] (2011) General Computer Science: 320201 GenCS II Lecture Notes. External Links: Link Cited by: p1.
- [8] (2011) General Computer Science: Problems and Solutions for 320201 GenCS II. External Links: Link Cited by: p1.
- [9] (2011) General Computer Science: Problems for 320201 GenCS II. External Links: Link Cited by: p1.
- [16] (2011) The FormalCAD Project. External Links: Link Cited by: p1.
- [1] (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] (2009) The LATIN Project. External Links: Link Cited by: p1.
- [11] (2006) Ontology-driven management of change. External Links: Link Cited by: p1.
- [13] (2003) Guidelines for graphics in MathML 2. Note: W3C Note External Links: Link Cited by: p1.
- [14] (2003) Bound variables in MathML. Note: W3C Working Group Note External Links: Link Cited by: p1.
- [15] (2003) Structured types in MathML 2.0. Note: W3C Note External Links: Link Cited by: p1.
- [17] (2001) OMDoc: an open markup format for mathematical documents (version 1.1). Open Specification. External Links: Link Cited by: p1.
- [10] (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.
- [20] Open digital research environment toolkit for the advancement of mathematics. Project Proposal. External Links: Link Cited by: p1.