Edit Profile (opens in new tab) Kohlhase, Michael Compute Distance To: Compute Author ID: kohlhase.michael Published as: Kohlhase, Michael Homepage: https://kwarc.info/people/mkohlhase External Links: MGP · ORCID · Wikidata · Google Scholar · dblp · GND Documents Indexed: 102 Publications since 1992 5 Contributions as Editor Co-Authors: 117 Co-Authors with 97 Joint Publications 1,087 Co-Co-Authors all top 5 Co-Authors 10 single-authored 30 Rabe, Florian 11 Kohlhase, Andrea 10 Müller, Dennis 8 Iancu, Mihnea 7 Benzmüller, Christoph Ewald 6 Horozal, Fulya 6 Kerber, Manfred 6 Wiesing, Tom 5 Franke, Andreas 5 Stamerjohanns, Heinrich 4 Brown, Chad Edward 4 David, Catalin 4 Ginev, Deyan 4 Jucovschi, Constantin 4 Sorge, Volker 4 Sperber, Wolfram 3 Codescu, Mihai 3 Lange, Christoph 3 Miller, Bruce R. 3 Mossakowski, Till 3 Sacerdoti Coen, Claudio 2 Berčič, Katja 2 Carette, Jacques 2 Cheikhrouhou, Lassaad 2 Farmer, William M. 2 Fiedler, Armin 2 Hutter, Dieter 2 Marcus, Richard 2 Meier, Andreas 2 Melis, Erica 2 Normann, Immanuel 2 Pfeiffer, Markus 2 Prodescu, Corneliu-Claudiu 2 Siekmann, Jörg H. 2 Teschke, Olaf 2 Thiéry, Nicolas Marc 2 Urban, Josef 2 Zholudev, Vyacheslav 2 Zimmer, Jürgen 1 Alama, Jesse 1 Amann, Kai 1 Anghelache, Romeo 1 Antoniou, Ioannis E. 1 Armando, Alessandro 1 Autexier, Serge 1 Betzendahl, Jonas 1 Bösl, Benjamin 1 Bratsas, Charalampos 1 Brezhnev, Vladimir 1 Condoluci, Andrea 1 Corneli, Joseph 1 Davenport, James Harold 1 De Feo, Luca 1 de Moura, Leonardo 1 Dehaye, Paul-Olivier 1 Dietrich, Dominik 1 Dimou, Anastasia 1 Fehrer, Detlef 1 Freksa, Christian 1 Fürsich, Michael 1 Gauthier, Thibault 1 Grigore, Mihai 1 Hambasan, Radu 1 Hess, Stephan M. 1 Hilf, Eberhard R. 1 Horacek, Helmut 1 Huang, Xiaorong 1 Iacob, Alin 1 Ion, Patrick D. F. 1 Johann, Patricia 1 Johansson, Moa 1 Jucovshi, Constantin 1 Jung, Christoph G. 1 Kaliszyk, Cezary 1 Kohlhase, Lukas 1 Koller, Alexander 1 Konovalov, Olexandr 1 Konrad, Karsten 1 Koprucki, Thomas 1 Köstler, Harald 1 Lelièvre, Samuel 1 Luzhnica, Enxhell 1 Mamane, Lionel Elie 1 Mance, Felix 1 Matican, Bogdan A. 1 Mihaljević, Helena 1 Misey, Dimitar 1 Moschner, Markus 1 Müller, Christine 1 Naumowicz, Adam 1 Oripov, Akbar 1 Ouypornkochagorn, Taweechai 1 Owre, Sam 1 Pollet, Martin 1 Pollinger, Theresa 1 Ranise, Silvio 1 Rochau, Denis 1 Rothgang, Colin 1 Roux, Navid 1 Rudnicki, Piotr ...and 17 more Co-Authors all top 5 Serials 4 Journal of Automated Reasoning 3 Lecture Notes in Computer Science 3 Mathematics in Computer Science 2 Journal of Applied Non-Classical Logics 2 European Mathematical Society Newsletter 1 The Mathematical Intelligencer 1 The Journal of Symbolic Logic 1 Journal of Symbolic Computation 1 Information and Computation 1 Journal of Logic, Language and Information 1 Logic Journal of the IGPL 1 Journal of Universal Computer Science 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning all top 5 Fields 99 Computer science (68-XX) 18 Mathematical logic and foundations (03-XX) 12 General and overarching topics; collections (00-XX) 2 History and biography (01-XX) 2 Mathematics education (97-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 75 Publications have been cited 309 times in 166 Documents Cited by ▼ Year ▼ A scalable module system. Zbl 1358.68283Rabe, Florian; Kohlhase, Michael 30 2013 Higher-order semantics and extensionality. Zbl 1071.03024Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael 26 2004 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 16 2011 Using LaTEX as a semantic markup format. Zbl 1176.68230Kohlhase, Michael 10 2008 A search engine for mathematical formulae. Zbl 1156.68306Kohlhase, Michael; Sucan, Ioan 10 2006 Integrating computer algebra into proof planning. Zbl 0916.68144Kerber, Manfred; Kohlhase, Michael; Sorge, Volker 9 1998 Cut-simulation and impredicativity. Zbl 1160.03004Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael 9 2009 OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511Kohlhase, Michael 7 2001 Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina 7 2012 Notations for living mathematical documents. Zbl 1166.00304Kohlhase, Michael; Müller, Christine; Rabe, Florian 7 2008 Extending MKM formats at the statement level. Zbl 1278.68293Horozal, Fulya; Kohlhase, Michael; Rabe, Florian 6 2012 Proof development with \(\Omega\)MEGA. Zbl 1072.68591Siekmann, Jörg; Benzmüller, Christoph; Brezhnev, Vladimir; Cheikhrouhou, Lassaad; Fiedler, Armin; Franke, Andreas; Horacek, Helmut; Kohlhase, Michael; Meier, Andreas; Melis, Erica; Moschner, Markus; Normann, Immanuel; Pollet, Martin; Sorge, Volker; Ullrich, Carsten; Wirth, Claus-Peter; Zimmer, Jürgen 6 2002 Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav 6 2010 A foundational view on integration problems. Zbl 1278.68289Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio 6 2011 Flexary operators for formalized mathematics. Zbl 1304.68171Horozal, Fulya; Rabe, Florian; Kohlhase, Michael 5 2014 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 4 2017 System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601Zimmer, Jürgen; Kohlhase, Michael 4 2002 Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169Carette, Jacques; Farmer, William M.; Kohlhase, Michael 4 2014 MathML-aware article conversion from LaTeX a comparison study. Zbl 1176.68233Stamerjohanns, Heinrich; Ginev, Deyan; David, Catalin; Misey, Dimitar; Zamdzhiev, Vladimir; Kohlhase, Michael 4 2009 Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241Kohlhase, Michael 4 2014 Transforming large collections of scientific publications to XML. Zbl 1205.68490Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce 4 2010 Extensional higher-order resolution. Zbl 0928.03004Benzmüller, Christoph; Kohlhase, Michael 3 1998 Unification in order-sorted type theory. Zbl 0925.03080Kohlhase, Michael 3 1992 Reimplementing the mathematics subject classification (MSC) as a linked open dataset. Zbl 1257.68135Lange, Christoph; Ion, Patrick; Dimou, Anastasia; Bratsas, Charalampos; Corneli, Joseph; Sperber, Wolfram; Kohlhase, Michael; Antoniou, Ioannis 3 2012 Mathematical formula search. Zbl 1310.68217Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf 3 2013 Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157Normann, Immanuel; Kohlhase, Michael 3 2007 A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173Kohlhase, Michael 3 2014 System description: MathHub.info. Zbl 1304.68196Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom 3 2014 The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael 3 2011 Agent-oriented integration of distributed mathematical services. Zbl 0961.68117Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker 3 1999 Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530Grigore, Mihai; Wolska, Magdalena; Kohlhase, Michael 3 2009 Higher-order automated theorem proving. Zbl 0971.68141Kohlhase, Michael 3 1998 MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu 2 2012 Communities of practice in MKM: an extensional model. Zbl 1188.68281Kohlhase, Andrea; Kohlhase, Michael 2 2006 Reexamining the MKM value proposition: From Math Web Search to Math Web ReSearch. Zbl 1202.68467Kohlhase, Andrea; Kohlhase, Michael 2 2007 A tableau claculus for partial functions. Zbl 0851.03004Kerber, Manfred; Kohlhase, Michael 2 1996 A universal machine for biform theory graphs. Zbl 1278.68267Kohlhase, Michael; Mance, Felix; Rabe, Florian 2 2013 An exploration in the space of mathematical knowledge. Zbl 1151.68666Kohlhase, Andrea; Kohlhase, Michael 2 2006 QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343Kohlhase, Michael; Rabe, Florian 2 2016 A mechanization of strong Kleene logic for partial functions. Zbl 1433.03024Kerber, Manfred; Kohlhase, Michael 2 1994 MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153Kohlhase, Michael; Franke, Andreas 2 2001 Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550Wiesing, Tom; Kohlhase, Michael; Rabe, Florian 2 2017 STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294Jucovschi, Constantin; Kohlhase, Michael 2 2010 Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom 2 2016 Representing structural language features in formal meta-languages. Zbl 1455.68268Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael 2 2020 Unifying math ontologies: a tale of two standards. Zbl 1247.68268Davenport, James H.; Kohlhase, Michael 2 2009 Spreadsheet interaction with frames: exploring a mathematical practice. Zbl 1247.68274Kohlhase, Andrea; Kohlhase, Michael 2 2009 Managing structural information by higher-order colored unification. Zbl 0959.03007Hutter, Dieter; Kohlhase, Michael 2 2000 System description: MBase, an open mathematical knowledge base. Zbl 0963.68543Franke, Andreas; Kohlhase, Michael 2 2000 CPoint: Dissolving the author’s dilemma. Zbl 1108.68593Kohlhase, Andrea; Kohlhase, Michael 1 2004 Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661Luzhnica, Enxhell; Kohlhase, Michael 1 2016 A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 1 2012 Semantic alliance: a framework for semantic allies. Zbl 1278.68298David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael 1 2012 The Planetary project: towards eMath3.0. Zbl 1278.68339Kohlhase, Michael 1 2012 Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Zbl 1096.68004 1 2006 Capturing the content of physics: systems, observables, and experiments. Zbl 1188.68279Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich 1 2006 Semantics of OpenMath and MathML3. Zbl 1271.68221Kohlhase, Michael; Rabe, Florian 1 2012 Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356Berčič, Katja; Kohlhase, Michael; Rabe, Florian 1 2019 Relational data across mathematical libraries. Zbl 1428.68352Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius 1 2019 Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio 1 2001 Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu 1 2014 Experiences from exporting major proof assistant libraries. Zbl 07461271Kohlhase, Michael; Rabe, Florian 1 2021 Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian 1 2021 \(\Omega\)mega: towards a mathematical assistant. Zbl 1430.68393Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg; Sorge, Volker 1 1997 Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175Betzendahl, Jonas; Kohlhase, Michael 1 2018 Theories as types. Zbl 06958124Müller, Dennis; Rabe, Florian; Kohlhase, Michael 1 2018 Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275Kohlhase, Andrea; Kohlhase, Michael 1 2009 A mathematical approach to ontology authoring and documentation. Zbl 1247.68279Lange, Christoph; Kohlhase, Michael 1 2009 Workflows for the management of change in science, technologies, engineering and mathematics. Zbl 1278.68291Autexier, Serge; David, Catalin; Dietrich, Dominik; Kohlhase, Michael; Zholudev, Vyacheslav 1 2011 Towards collaborative content management and version control for structured mathematical knowledge. Zbl 1022.68618Kohlhase, Michael; Anghelache, Romeo 1 2003 Resource-adaptive model generation as a performance model. Zbl 1061.68158Kohlhase, Michael; Koller, Alexander 1 2003 Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025 1 2016 Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian 1 2017 Experiences from exporting major proof assistant libraries. Zbl 07461271Kohlhase, Michael; Rabe, Florian 1 2021 Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian 1 2021 Representing structural language features in formal meta-languages. Zbl 1455.68268Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael 2 2020 Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356Berčič, Katja; Kohlhase, Michael; Rabe, Florian 1 2019 Relational data across mathematical libraries. Zbl 1428.68352Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius 1 2019 Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175Betzendahl, Jonas; Kohlhase, Michael 1 2018 Theories as types. Zbl 06958124Müller, Dennis; Rabe, Florian; Kohlhase, Michael 1 2018 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 4 2017 Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550Wiesing, Tom; Kohlhase, Michael; Rabe, Florian 2 2017 Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian 1 2017 QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343Kohlhase, Michael; Rabe, Florian 2 2016 Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom 2 2016 Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661Luzhnica, Enxhell; Kohlhase, Michael 1 2016 Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025 1 2016 Flexary operators for formalized mathematics. Zbl 1304.68171Horozal, Fulya; Rabe, Florian; Kohlhase, Michael 5 2014 Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169Carette, Jacques; Farmer, William M.; Kohlhase, Michael 4 2014 Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241Kohlhase, Michael 4 2014 A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173Kohlhase, Michael 3 2014 System description: MathHub.info. Zbl 1304.68196Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom 3 2014 Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu 1 2014 A scalable module system. Zbl 1358.68283Rabe, Florian; Kohlhase, Michael 30 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 Mathematical formula search. Zbl 1310.68217Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf 3 2013 A universal machine for biform theory graphs. Zbl 1278.68267Kohlhase, Michael; Mance, Felix; Rabe, Florian 2 2013 Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina 7 2012 Extending MKM formats at the statement level. Zbl 1278.68293Horozal, Fulya; Kohlhase, Michael; Rabe, Florian 6 2012 Reimplementing the mathematics subject classification (MSC) as a linked open dataset. Zbl 1257.68135Lange, Christoph; Ion, Patrick; Dimou, Anastasia; Bratsas, Charalampos; Corneli, Joseph; Sperber, Wolfram; Kohlhase, Michael; Antoniou, Ioannis 3 2012 MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu 2 2012 A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 1 2012 Semantic alliance: a framework for semantic allies. Zbl 1278.68298David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael 1 2012 The Planetary project: towards eMath3.0. Zbl 1278.68339Kohlhase, Michael 1 2012 Semantics of OpenMath and MathML3. Zbl 1271.68221Kohlhase, Michael; Rabe, Florian 1 2012 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian 16 2011 A foundational view on integration problems. Zbl 1278.68289Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio 6 2011 The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael 3 2011 Workflows for the management of change in science, technologies, engineering and mathematics. Zbl 1278.68291Autexier, Serge; David, Catalin; Dietrich, Dominik; Kohlhase, Michael; Zholudev, Vyacheslav 1 2011 Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav 6 2010 Transforming large collections of scientific publications to XML. Zbl 1205.68490Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce 4 2010 STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294Jucovschi, Constantin; Kohlhase, Michael 2 2010 Cut-simulation and impredicativity. Zbl 1160.03004Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael 9 2009 MathML-aware article conversion from LaTeX a comparison study. Zbl 1176.68233Stamerjohanns, Heinrich; Ginev, Deyan; David, Catalin; Misey, Dimitar; Zamdzhiev, Vladimir; Kohlhase, Michael 4 2009 Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530Grigore, Mihai; Wolska, Magdalena; Kohlhase, Michael 3 2009 Unifying math ontologies: a tale of two standards. Zbl 1247.68268Davenport, James H.; Kohlhase, Michael 2 2009 Spreadsheet interaction with frames: exploring a mathematical practice. Zbl 1247.68274Kohlhase, Andrea; Kohlhase, Michael 2 2009 Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275Kohlhase, Andrea; Kohlhase, Michael 1 2009 A mathematical approach to ontology authoring and documentation. Zbl 1247.68279Lange, Christoph; Kohlhase, Michael 1 2009 Using LaTEX as a semantic markup format. Zbl 1176.68230Kohlhase, Michael 10 2008 Notations for living mathematical documents. Zbl 1166.00304Kohlhase, Michael; Müller, Christine; Rabe, Florian 7 2008 Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157Normann, Immanuel; Kohlhase, Michael 3 2007 Reexamining the MKM value proposition: From Math Web Search to Math Web ReSearch. Zbl 1202.68467Kohlhase, Andrea; Kohlhase, Michael 2 2007 A search engine for mathematical formulae. Zbl 1156.68306Kohlhase, Michael; Sucan, Ioan 10 2006 Communities of practice in MKM: an extensional model. Zbl 1188.68281Kohlhase, Andrea; Kohlhase, Michael 2 2006 An exploration in the space of mathematical knowledge. Zbl 1151.68666Kohlhase, Andrea; Kohlhase, Michael 2 2006 Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Zbl 1096.68004 1 2006 Capturing the content of physics: systems, observables, and experiments. Zbl 1188.68279Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich 1 2006 Higher-order semantics and extensionality. Zbl 1071.03024Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael 26 2004 CPoint: Dissolving the author’s dilemma. Zbl 1108.68593Kohlhase, Andrea; Kohlhase, Michael 1 2004 Towards collaborative content management and version control for structured mathematical knowledge. Zbl 1022.68618Kohlhase, Michael; Anghelache, Romeo 1 2003 Resource-adaptive model generation as a performance model. Zbl 1061.68158Kohlhase, Michael; Koller, Alexander 1 2003 Proof development with \(\Omega\)MEGA. Zbl 1072.68591Siekmann, Jörg; Benzmüller, Christoph; Brezhnev, Vladimir; Cheikhrouhou, Lassaad; Fiedler, Armin; Franke, Andreas; Horacek, Helmut; Kohlhase, Michael; Meier, Andreas; Melis, Erica; Moschner, Markus; Normann, Immanuel; Pollet, Martin; Sorge, Volker; Ullrich, Carsten; Wirth, Claus-Peter; Zimmer, Jürgen 6 2002 System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601Zimmer, Jürgen; Kohlhase, Michael 4 2002 OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511Kohlhase, Michael 7 2001 MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153Kohlhase, Michael; Franke, Andreas 2 2001 Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio 1 2001 Managing structural information by higher-order colored unification. Zbl 0959.03007Hutter, Dieter; Kohlhase, Michael 2 2000 System description: MBase, an open mathematical knowledge base. Zbl 0963.68543Franke, Andreas; Kohlhase, Michael 2 2000 Agent-oriented integration of distributed mathematical services. Zbl 0961.68117Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker 3 1999 Integrating computer algebra into proof planning. Zbl 0916.68144Kerber, Manfred; Kohlhase, Michael; Sorge, Volker 9 1998 Extensional higher-order resolution. Zbl 0928.03004Benzmüller, Christoph; Kohlhase, Michael 3 1998 Higher-order automated theorem proving. Zbl 0971.68141Kohlhase, Michael 3 1998 \(\Omega\)mega: towards a mathematical assistant. Zbl 1430.68393Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg; Sorge, Volker 1 1997 A tableau claculus for partial functions. Zbl 0851.03004Kerber, Manfred; Kohlhase, Michael 2 1996 A mechanization of strong Kleene logic for partial functions. Zbl 1433.03024Kerber, Manfred; Kohlhase, Michael 2 1994 Unification in order-sorted type theory. Zbl 0925.03080Kohlhase, Michael 3 1992 all cited Publications top 5 cited Publications all top 5 Cited by 228 Authors 36 Kohlhase, Michael 23 Rabe, Florian 20 Benzmüller, Christoph Ewald 11 Kaliszyk, Cezary 7 Korniłowicz, Artur 7 Naumowicz, Adam 7 Pąk, Karol 6 Farmer, William M. 6 Horozal, Fulya 6 Iancu, Mihnea 5 Brown, Chad Edward 5 Urban, Josef 4 Ataeva, O. M. 4 Autexier, Serge 4 Blanchette, Jasmin Christian 4 Carette, Jacques 4 Grabowski, Adam 4 Kohlhase, Andrea 4 Paulson, Lawrence Charles 4 Sacerdoti Coen, Claudio 4 Schubotz, Moritz 4 Serebryakov, V. A. 4 Steen, Alexander 4 Teschke, Olaf 4 Tuchkova, Natal’ya Pavlovna 3 Gauthier, Thibault 3 Ginev, Deyan 3 Hutter, Dieter 3 Jucovschi, Constantin 3 Kerber, Manfred 3 Melis, Erica 3 Miller, Bruce R. 3 Mossakowski, Till 3 Müller, Dennis 3 Nipkow, Tobias 3 Siekmann, Jörg H. 3 Sorge, Volker 3 Wiesing, Tom 3 Wisniewski, Max 3 Woltzenlogel Paleo, Bruno 2 Backes, Julian 2 Bancerek, Grzegorz 2 Bentkamp, Alexander 2 Byliński, Czesław 2 Caprotti, Olga 2 Codescu, Mihai 2 David, Catalin 2 de Nivelle, Hans 2 Guidi, Ferruccio 2 Kanckos, Annika 2 Kirillovich, Aleksandr Vital’evich 2 Lange, Christoph 2 Lipachëv, E. K. 2 Matuszewski, Roman 2 Meier, Andreas 2 Nevzorova, Ol’ga Avenirovna 2 Runnwerth, Mila 2 Sperber, Wolfram 2 Stamerjohanns, Heinrich 2 Sultana, Nik 2 Sutcliffe, Geoff 2 Theiss, Frank 2 Tourret, Sophie 2 Vukmirović, Petar 2 Waldmann, Uwe 2 Wirth, Claus-Peter 2 Youssef, Abdou S. 1 Aizawa, Akiko N. 1 Alessi, Fabio 1 Allen, Stuart F. 1 Andrews, Peter B. 1 Armando, Alessandro 1 Arndt, Susanne 1 Auer, Sören 1 Barsotti, Damián 1 Berčič, Katja 1 Bickford, Mark 1 Billingsley, William 1 Botta, Nicola 1 Brede, Nuria 1 Brucker, Achim D. 1 Cairns, Paul 1 Carter, Nathan C. 1 Cheikhrouhou, Lassaad 1 Chen, Xiaoyu 1 Ciaffaglione, Alberto 1 Coglio, Alessandro 1 Cohen, Arjeh Marcel 1 Cohl, Howard Saul 1 Constable, Robert Lee 1 Danoff, Alex A. 1 Davenport, James Harold 1 Degtyarev, Anatoli Ivanovich 1 Dehaye, Paul-Olivier 1 Dennis, Louise Abigail 1 Di Gianantonio, Pietro 1 Dietrich, Dominik 1 Dowek, Gilles 1 Dunchev, Cvetan 1 Dundua, Besik ...and 128 more Authors all top 5 Cited in 30 Serials 24 Journal of Automated Reasoning 9 Journal of Symbolic Computation 6 Lobachevskii Journal of Mathematics 5 Journal of Applied Logic 4 Mathematics in Computer Science 3 Theoretical Computer Science 3 Formal Aspects of Computing 2 Artificial Intelligence 2 Journal of Philosophical Logic 2 Information and Computation 2 Journal of Applied Non-Classical Logics 2 Logica Universalis 1 Acta Informatica 1 The Mathematical Intelligencer 1 Studia Logica 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 MSCS. Mathematical Structures in Computer Science 1 Cybernetics and Systems Analysis 1 Journal of Functional Programming 1 Annals of Mathematics and Artificial Intelligence 1 European Mathematical Society Newsletter 1 Logic and Logical Philosophy 1 Sādhanā 1 Computer Languages, Systems & Structures 1 ACM Transactions on Computational Logic 1 Parallel Processing Letters 1 Mathematical Biosciences and Engineering 1 The Review of Symbolic Logic 1 Journal of Formalized Reasoning all top 5 Cited in 15 Fields 153 Computer science (68-XX) 49 Mathematical logic and foundations (03-XX) 5 General and overarching topics; collections (00-XX) 5 History and biography (01-XX) 3 Number theory (11-XX) 2 Combinatorics (05-XX) 2 Special functions (33-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Ordinary differential equations (34-XX) 1 Partial differential equations (35-XX) 1 Optics, electromagnetic theory (78-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.