×
Author ID: kohlhase.michael Recent zbMATH articles by "Kohlhase, Michael"
Published as: Kohlhase, Michael
Homepage: https://kwarc.info/people/mkohlhase
External Links: MGP · ORCID · Wikidata · Google Scholar · dblp · GND
all top 5

Co-Authors

10 single-authored
31 Rabe, Florian
13 Müller, Dennis
11 Kohlhase, Andrea
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 Betzendahl, Jonas
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 Schaefer, Jan Frederik
2 Siekmann, Jörg H.
2 Teschke, Olaf
2 Thiéry, Nicolas Marc
2 Urban, Josef
2 Wenzel, Makarius
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 Berges, Marc
1 Bösl, Benjamin
1 Bratsas, Charalampos
1 Brezhnev, Vladimir
1 Chugh, Abhishek
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 Lohr, Dominic
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
...and 20 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

88 Publications have been cited 387 times in 199 Documents Cited by Year
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
39
2013
Higher-order semantics and extensionality. Zbl 1071.03024
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
28
2004
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
19
2013
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
18
2011
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
A search engine for mathematical formulae. Zbl 1156.68306
Kohlhase, Michael; Sucan, Ioan
15
2006
Using LaTEXas a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
13
2008
\(\Omega\)mega: towards a mathematical assistant. Zbl 1430.68393
Benzmü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
10
1997
Integrating computer algebra into proof planning. Zbl 0916.68144
Kerber, Manfred; Kohlhase, Michael; Sorge, Volker
9
1998
Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina
8
2012
Cut-simulation and impredicativity. Zbl 1160.03004
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael
8
2009
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
7
2012
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
7
2008
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
7
2010
OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511
Kohlhase, Michael
7
2001
Proof development with \(\Omega\)MEGA. Zbl 1072.68591
Siekmann, 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
7
2002
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
7
2014
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
7
2014
A mechanization of strong Kleene logic for partial functions. Zbl 1433.03024
Kerber, Manfred; Kohlhase, Michael
7
1994
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
5
2017
Theories as types. Zbl 1511.68340
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
4
2018
MathML-aware article conversion from LaTeX a comparison study. Zbl 1176.68233
Stamerjohanns, Heinrich; Ginev, Deyan; David, Catalin; Misey, Dimitar; Zamdzhiev, Vladimir; Kohlhase, Michael
4
2009
Agent-oriented integration of distributed mathematical services. Zbl 0961.68117
Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker
4
1999
Transforming large collections of scientific publications to XML. Zbl 1205.68490
Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce
4
2010
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
Kohlhase, Michael
4
2014
System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601
Zimmer, Jürgen; Kohlhase, Michael
4
2002
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
4
2014
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
Representing structural language features in formal meta-languages. Zbl 1455.68268
Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael
4
2020
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
3
2006
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
Higher-order automated theorem proving. Zbl 0971.68141
Kohlhase, Michael
3
1998
Reimplementing the mathematics subject classification (MSC) as a linked open dataset. Zbl 1257.68135
Lange, Christoph; Ion, Patrick; Dimou, Anastasia; Bratsas, Charalampos; Corneli, Joseph; Sperber, Wolfram; Kohlhase, Michael; Antoniou, Ioannis
3
2012
The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337
Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael
3
2011
MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153
Kohlhase, Michael; Franke, Andreas
3
2001
Extensional higher-order resolution. Zbl 0928.03004
Benzmüller, Christoph; Kohlhase, Michael
3
1998
Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157
Normann, Immanuel; Kohlhase, Michael
3
2007
Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530
Grigore, Mihai; Wolska, Magdalena; Kohlhase, Michael
3
2009
A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173
Kohlhase, Michael
3
2014
Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268
Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom
3
2016
Mathematical formula search. Zbl 1310.68217
Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf
3
2013
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
3
2019
Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175
Betzendahl, Jonas; Kohlhase, Michael
2
2018
Managing structural information by higher-order colored unification. Zbl 0959.03007
Hutter, Dieter; Kohlhase, Michael
2
2000
Communities of practice in MKM: an extensional model. Zbl 1188.68281
Kohlhase, Andrea; Kohlhase, Michael
2
2006
MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu
2
2012
Unifying math ontologies: a tale of two standards. Zbl 1247.68268
Davenport, James H.; Kohlhase, Michael
2
2009
Spreadsheet interaction with frames: exploring a mathematical practice. Zbl 1247.68274
Kohlhase, Andrea; Kohlhase, Michael
2
2009
A tableau claculus for partial functions. Zbl 0851.03004
Kerber, Manfred; Kohlhase, Michael
2
1996
Reexamining the MKM value proposition: From Math Web Search to Math Web ReSearch. Zbl 1202.68467
Kohlhase, Andrea; Kohlhase, Michael
2
2007
STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294
Jucovschi, Constantin; Kohlhase, Michael
2
2010
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
2
2017
System description: MBase, an open mathematical knowledge base. Zbl 0963.68543
Franke, Andreas; Kohlhase, Michael
2
2000
Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6–7, 2000. Zbl 0962.00008
2
2001
A universal machine for biform theory graphs. Zbl 1278.68267
Kohlhase, Michael; Mance, Felix; Rabe, Florian
2
2013
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
2
2021
System description STEX3 – a LATEX-based ecosystem for semantic/active mathematical documents. Zbl 07691299
Kohlhase, Michael; Müller, Dennis
2
2022
Automatically finding theory morphisms for knowledge management. Zbl 1417.68211
Müller, Dennis; Kohlhase, Michael; Rabe, Florian
1
2018
MBase: Representing mathematical knowledge in a relational data base. Zbl 0958.68163
Franke, Andreas; Kohlhase, Michael
1
1999
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.68279
Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich
1
2006
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
1
2012
Semantic alliance: a framework for semantic allies. Zbl 1278.68298
David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael
1
2012
The Planetary project: towards eMath3.0. Zbl 1278.68339
Kohlhase, Michael
1
2012
Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275
Kohlhase, Andrea; Kohlhase, Michael
1
2009
A mathematical approach to ontology authoring and documentation. Zbl 1247.68279
Lange, Christoph; Kohlhase, Michael
1
2009
Workflows for the management of change in science, technologies, engineering and mathematics. Zbl 1278.68291
Autexier, Serge; David, Catalin; Dietrich, Dominik; Kohlhase, Michael; Zholudev, Vyacheslav
1
2011
Combining source, content, presentation, narration, and relational representation. Zbl 1278.68292
Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian
1
2011
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
2001
Towards collaborative content management and version control for structured mathematical knowledge. Zbl 1022.68618
Kohlhase, Michael; Anghelache, Romeo
1
2003
CPoint: Dissolving the author’s dilemma. Zbl 1108.68593
Kohlhase, Andrea; Kohlhase, Michael
1
2004
Cut elimination with \(\xi\)-functionality. Zbl 1226.03060
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
1
2008
Resource-adaptive model generation as a performance model. Zbl 1061.68158
Kohlhase, Michael; Koller, Alexander
1
2003
Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280
Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu
1
2014
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
1
2016
Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661
Luzhnica, Enxhell; Kohlhase, Michael
1
2016
Software citations, information systems, and beyond. Zbl 1367.68336
Kohlhase, Michael; Sperber, Wolfram
1
2017
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian
1
2021
A colored version of the \(\lambda\)-calculus. Zbl 1430.68412
Hutter, Dieter; Kohlhase, Michael
1
1997
Semantics of OpenMath and MathML3. Zbl 1271.68221
Kohlhase, Michael; Rabe, Florian
1
2012
Making Isabelle content accessible in knowledge representation formats. Zbl 07756106
Kohlhase, Michael; Rabe, Florian; Wenzel, Makarius
1
2020
Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2019
Unification in an extensional lambda calculus with ordered function sorts and constant overloading. Zbl 1433.68554
Johann, Patricia; Kohlhase, Michael
1
1994
Towards a heterogeneous query language for mathematical knowledge. Zbl 1455.68264
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2020
TGView3D: a system for 3-dimensional visualization of theory graphs. Zbl 1455.68267
Marcus, Richard; Kohlhase, Michael; Rabe, Florian
1
2020
Injecting formal mathematics into LaTeX. Zbl 07691298
Müller, Dennis; Kohlhase, Michael
1
2022
System description STEX3 – a LATEX-based ecosystem for semantic/active mathematical documents. Zbl 07691299
Kohlhase, Michael; Müller, Dennis
2
2022
Injecting formal mathematics into LaTeX. Zbl 07691298
Müller, Dennis; Kohlhase, Michael
1
2022
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
2
2021
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. Zbl 1493.68391
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian
1
2021
Representing structural language features in formal meta-languages. Zbl 1455.68268
Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael
4
2020
Making Isabelle content accessible in knowledge representation formats. Zbl 07756106
Kohlhase, Michael; Rabe, Florian; Wenzel, Makarius
1
2020
Towards a heterogeneous query language for mathematical knowledge. Zbl 1455.68264
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2020
TGView3D: a system for 3-dimensional visualization of theory graphs. Zbl 1455.68267
Marcus, Richard; Kohlhase, Michael; Rabe, Florian
1
2020
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
3
2019
Towards a unified mathematical data infrastructure: database and interface generation. Zbl 1428.68356
Berčič, Katja; Kohlhase, Michael; Rabe, Florian
1
2019
Theories as types. Zbl 1511.68340
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
4
2018
Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175
Betzendahl, Jonas; Kohlhase, Michael
2
2018
Automatically finding theory morphisms for knowledge management. Zbl 1417.68211
Müller, Dennis; Kohlhase, Michael; Rabe, Florian
1
2018
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
5
2017
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 1497.68550
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Making PVS accessible to generic services by interpretation in a universal format. Zbl 1484.68311
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
2
2017
Software citations, information systems, and beyond. Zbl 1367.68336
Kohlhase, Michael; Sperber, Wolfram
1
2017
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
4
2016
Interoperability in the OpenDreamKit project: the math-in-the-middle approach. Zbl 1344.68268
Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom
3
2016
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
1
2016
Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661
Luzhnica, Enxhell; Kohlhase, Michael
1
2016
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
7
2014
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
7
2014
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
Kohlhase, Michael
4
2014
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
4
2014
A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173
Kohlhase, Michael
3
2014
Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280
Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu
1
2014
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
39
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
19
2013
Mathematical formula search. Zbl 1310.68217
Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf
3
2013
A universal machine for biform theory graphs. Zbl 1278.68267
Kohlhase, Michael; Mance, Felix; Rabe, Florian
2
2013
Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina
8
2012
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
7
2012
Reimplementing the mathematics subject classification (MSC) as a linked open dataset. Zbl 1257.68135
Lange, 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.68296
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu
2
2012
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
1
2012
Semantic alliance: a framework for semantic allies. Zbl 1278.68298
David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael
1
2012
The Planetary project: towards eMath3.0. Zbl 1278.68339
Kohlhase, Michael
1
2012
Semantics of OpenMath and MathML3. Zbl 1271.68221
Kohlhase, Michael; Rabe, Florian
1
2012
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
18
2011
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337
Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael
3
2011
Workflows for the management of change in science, technologies, engineering and mathematics. Zbl 1278.68291
Autexier, Serge; David, Catalin; Dietrich, Dominik; Kohlhase, Michael; Zholudev, Vyacheslav
1
2011
Combining source, content, presentation, narration, and relational representation. Zbl 1278.68292
Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian
1
2011
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
7
2010
Transforming large collections of scientific publications to XML. Zbl 1205.68490
Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce
4
2010
STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294
Jucovschi, Constantin; Kohlhase, Michael
2
2010
Cut-simulation and impredicativity. Zbl 1160.03004
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael
8
2009
MathML-aware article conversion from LaTeX a comparison study. Zbl 1176.68233
Stamerjohanns, Heinrich; Ginev, Deyan; David, Catalin; Misey, Dimitar; Zamdzhiev, Vladimir; Kohlhase, Michael
4
2009
Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530
Grigore, Mihai; Wolska, Magdalena; Kohlhase, Michael
3
2009
Unifying math ontologies: a tale of two standards. Zbl 1247.68268
Davenport, James H.; Kohlhase, Michael
2
2009
Spreadsheet interaction with frames: exploring a mathematical practice. Zbl 1247.68274
Kohlhase, Andrea; Kohlhase, Michael
2
2009
Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275
Kohlhase, Andrea; Kohlhase, Michael
1
2009
A mathematical approach to ontology authoring and documentation. Zbl 1247.68279
Lange, Christoph; Kohlhase, Michael
1
2009
Using LaTEXas a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
13
2008
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
7
2008
Cut elimination with \(\xi\)-functionality. Zbl 1226.03060
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
1
2008
Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157
Normann, Immanuel; Kohlhase, Michael
3
2007
Reexamining the MKM value proposition: From Math Web Search to Math Web ReSearch. Zbl 1202.68467
Kohlhase, Andrea; Kohlhase, Michael
2
2007
A search engine for mathematical formulae. Zbl 1156.68306
Kohlhase, Michael; Sucan, Ioan
15
2006
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
3
2006
Communities of practice in MKM: an extensional model. Zbl 1188.68281
Kohlhase, 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.68279
Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich
1
2006
Higher-order semantics and extensionality. Zbl 1071.03024
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
28
2004
CPoint: Dissolving the author’s dilemma. Zbl 1108.68593
Kohlhase, Andrea; Kohlhase, Michael
1
2004
Towards collaborative content management and version control for structured mathematical knowledge. Zbl 1022.68618
Kohlhase, Michael; Anghelache, Romeo
1
2003
Resource-adaptive model generation as a performance model. Zbl 1061.68158
Kohlhase, Michael; Koller, Alexander
1
2003
Proof development with \(\Omega\)MEGA. Zbl 1072.68591
Siekmann, 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
7
2002
System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601
Zimmer, Jürgen; Kohlhase, Michael
4
2002
OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511
Kohlhase, Michael
7
2001
MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153
Kohlhase, Michael; Franke, Andreas
3
2001
Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6–7, 2000. Zbl 0962.00008
2
2001
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
2001
Managing structural information by higher-order colored unification. Zbl 0959.03007
Hutter, Dieter; Kohlhase, Michael
2
2000
System description: MBase, an open mathematical knowledge base. Zbl 0963.68543
Franke, Andreas; Kohlhase, Michael
2
2000
Agent-oriented integration of distributed mathematical services. Zbl 0961.68117
Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker
4
1999
MBase: Representing mathematical knowledge in a relational data base. Zbl 0958.68163
Franke, Andreas; Kohlhase, Michael
1
1999
Integrating computer algebra into proof planning. Zbl 0916.68144
Kerber, Manfred; Kohlhase, Michael; Sorge, Volker
9
1998
Higher-order automated theorem proving. Zbl 0971.68141
Kohlhase, Michael
3
1998
Extensional higher-order resolution. Zbl 0928.03004
Benzmüller, Christoph; Kohlhase, Michael
3
1998
\(\Omega\)mega: towards a mathematical assistant. Zbl 1430.68393
Benzmü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
10
1997
A colored version of the \(\lambda\)-calculus. Zbl 1430.68412
Hutter, Dieter; Kohlhase, Michael
1
1997
A tableau claculus for partial functions. Zbl 0851.03004
Kerber, Manfred; Kohlhase, Michael
2
1996
A mechanization of strong Kleene logic for partial functions. Zbl 1433.03024
Kerber, Manfred; Kohlhase, Michael
7
1994
Unification in an extensional lambda calculus with ordered function sorts and constant overloading. Zbl 1433.68554
Johann, Patricia; Kohlhase, Michael
1
1994
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
all top 5

Cited by 268 Authors

43 Kohlhase, Michael
30 Rabe, Florian
21 Benzmüller, Christoph Ewald
12 Kaliszyk, Cezary
8 Müller, Dennis
8 Pąk, Karol
7 Farmer, William M.
7 Korniłowicz, Artur
7 Naumowicz, Adam
6 Horozal, Fulya
6 Iancu, Mihnea
5 Blanchette, Jasmin Christian
5 Brown, Chad Edward
5 Carette, Jacques
5 Schubotz, Moritz
5 Teschke, Olaf
5 Urban, Josef
4 Ataeva, O. M.
4 Autexier, Serge
4 Grabowski, Adam
4 Kerber, Manfred
4 Kohlhase, Andrea
4 Mossakowski, Till
4 Paulson, Lawrence Charles
4 Sacerdoti Coen, Claudio
4 Serebryakov, V. A.
4 Steen, Alexander
4 Sutcliffe, Geoff
4 Tuchkova, Natal’ya Pavlovna
3 Codescu, Mihai
3 Gauthier, Thibault
3 Ginev, Deyan
3 Hutter, Dieter
3 Jucovschi, Constantin
3 Lipachëv, E. K.
3 Melis, Erica
3 Miller, Bruce R.
3 Nevzorova, Ol’ga Avenirovna
3 Nipkow, Tobias
3 Siekmann, Jörg H.
3 Sorge, Volker
3 Vukmirović, Petar
3 Waldmann, Uwe
3 Wiesing, Tom
2 Backes, Julian
2 Bancerek, Grzegorz
2 Bentkamp, Alexander
2 Byliński, Czesław
2 Caprotti, Olga
2 Chen, Xiaoyu
2 David, Catalin
2 de Nivelle, Hans
2 Dundua, Besik
2 Elizarov, A. M.
2 Fehrer, Detlef
2 Guidi, Ferruccio
2 Kanckos, Annika
2 Kirillovich, Aleksandr Vital’evich
2 Kutsia, Temur
2 Lange, Christoph
2 Matuszewski, Roman
2 Meier, Andreas
2 Müller, Fabian
2 Runnwerth, Mila
2 Schaefer, Jan Frederik
2 Solov’ëv, V. D.
2 Sperber, Wolfram
2 Stamerjohanns, Heinrich
2 Sultana, Nik
2 Theiss, Frank
2 Tourret, Sophie
2 Wenzel, Makarius
2 Wirth, Claus-Peter
2 Wisniewski, Max
2 Woltzenlogel Paleo, Bruno
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 Berges, Marc
1 Bergstra, Jan A.
1 Betzendahl, Jonas
1 Bickford, Mark
1 Billingsley, William
1 Botta, Nicola
1 Bradley, Elizabeth
1 Brauburger, Jürgen
1 Brede, Nuria
1 Brucker, Achim D.
1 Bundy, Alan
1 Cairns, Paul
1 Carter, Nathan C.
1 Cheikhrouhou, Lassaad
1 Chugh, Abhishek
...and 168 more Authors

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.