×
Compute Distance To:
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
29 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
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 Sacerdoti Coen, Claudio
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 H.
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 16 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

71 Publications have been cited 283 times in 156 Documents Cited by Year
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
29
2013
Higher-order semantics and extensionality. Zbl 1071.03024
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
22
2004
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
14
2011
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
14
2013
Using LaTEX as a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
10
2008
A search engine for mathematical formulae. Zbl 1156.68306
Kohlhase, Michael; Sucan, Ioan
9
2006
Integrating computer algebra into proof planning. Zbl 0916.68144
Kerber, Manfred; Kohlhase, Michael; Sorge, Volker
8
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
7
2012
OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511
Kohlhase, Michael
7
2001
Cut-simulation and impredicativity. Zbl 1160.03004
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael
7
2009
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
6
2012
A foundational view on integration problems. Zbl 1278.68289
Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio
6
2011
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
6
2010
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
6
2002
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
6
2008
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
5
2014
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
4
2014
Transforming large collections of scientific publications to XML. Zbl 1205.68490
Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce
4
2010
System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601
Zimmer, Jürgen; Kohlhase, Michael
4
2002
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
Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157
Normann, Immanuel; Kohlhase, Michael
3
2007
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173
Kohlhase, Michael
3
2014
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
3
2014
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
Kohlhase, Michael
3
2014
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
3
2017
Agent-oriented integration of distributed mathematical services. Zbl 0961.68117
Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker
3
1999
Higher-order automated theorem proving. Zbl 0971.68141
Kohlhase, Michael
3
1998
The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337
Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael
3
2011
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
2
2016
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 07036055
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
2
2006
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
Reexamining the MKM value proposition: From Math Web Search to Math Web ReSearch. Zbl 1202.68467
Kohlhase, Andrea; Kohlhase, Michael
2
2007
MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153
Kohlhase, Michael; Franke, Andreas
2
2001
A mechanization of strong Kleene logic for partial functions. Zbl 1433.03024
Kerber, Manfred; Kohlhase, Michael
2
1994
Mathematical formula search. Zbl 1310.68217
Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf
2
2013
MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu
2
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
2
2012
Managing structural information by higher-order colored unification. Zbl 0959.03007
Hutter, Dieter; Kohlhase, Michael
2
2000
Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530
Grigore, Mihai; Wolska, Magdalena; Kohlhase, Michael
2
2009
STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294
Jucovschi, Constantin; Kohlhase, Michael
2
2010
Extensional higher-order resolution. Zbl 0928.03004
Benzmüller, Christoph; Kohlhase, Michael
2
1998
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
2
2016
Communities of practice in MKM: an extensional model. Zbl 1188.68281
Kohlhase, Andrea; Kohlhase, Michael
2
2006
A tableau claculus for partial functions. Zbl 0851.03004
Kerber, Manfred; Kohlhase, Michael
2
1996
A universal machine for biform theory graphs. Zbl 1278.68267
Kohlhase, Michael; Mance, Felix; Rabe, Florian
2
2013
Representing structural language features in formal meta-languages. Zbl 1455.68268
Müller, Dennis; Rabe, Florian; Rothgang, Colin; Kohlhase, Michael
2
2020
\(\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
1
1997
System description: MBase, an open mathematical knowledge base. Zbl 0963.68543
Franke, Andreas; Kohlhase, Michael
1
2000
Theories as types. Zbl 06958124
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
1
2018
Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175
Betzendahl, Jonas; Kohlhase, Michael
1
2018
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
2001
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
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
1
2019
Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280
Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu
1
2014
Making PVS accessible to generic services by interpretation in a universal format. Zbl 06821860
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
1
2017
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
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
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
Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661
Luzhnica, 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
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
Experiences from exporting major proof assistant libraries. Zbl 07461271
Kohlhase, Michael; Rabe, Florian
1
2021
Experiences from exporting major proof assistant libraries. Zbl 07461271
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
2
2020
Relational data across mathematical libraries. Zbl 1428.68352
Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius
1
2019
Theories as types. Zbl 06958124
Müller, Dennis; Rabe, Florian; Kohlhase, Michael
1
2018
Translating the IMPS theory library to MMT/OMDoc. Zbl 1417.68175
Betzendahl, Jonas; Kohlhase, Michael
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
3
2017
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 07036055
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Making PVS accessible to generic services by interpretation in a universal format. Zbl 06821860
Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian
1
2017
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
2
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
2
2016
Formula semantification and automated relation finding in the On-line Encyclopedia of Integer Sequences. Zbl 1434.68661
Luzhnica, 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.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
5
2014
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
4
2014
A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173
Kohlhase, Michael
3
2014
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
3
2014
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
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
29
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
14
2013
Mathematical formula search. Zbl 1310.68217
Kohlhase, Michael; Mihaljević-Brandt, Helena; Sperber, Wolfram; Teschke, Olaf
2
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
7
2012
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
6
2012
MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu
2
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
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
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
14
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
Towards MKM in the large: modular representation and scalable software architecture. Zbl 1278.68297
Kohlhase, Michael; Rabe, Florian; Zholudev, Vyacheslav
6
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
7
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
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
Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530
Grigore, Mihai; Wolska, Magdalena; 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 LaTEX as a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
10
2008
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
6
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
9
2006
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
2
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
22
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
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
6
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
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
1
2000
Agent-oriented integration of distributed mathematical services. Zbl 0961.68117
Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker
3
1999
Integrating computer algebra into proof planning. Zbl 0916.68144
Kerber, Manfred; Kohlhase, Michael; Sorge, Volker
8
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
2
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
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
2
1994
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
all top 5

Cited by 219 Authors

35 Kohlhase, Michael
22 Rabe, Florian
20 Benzmüller, Christoph Ewald
10 Kaliszyk, Cezary
7 Korniłowicz, Artur
7 Naumowicz, Adam
6 Farmer, William M.
6 Horozal, Fulya
6 Iancu, Mihnea
6 Pąk, Karol
5 Urban, Josef
4 Autexier, Serge
4 Brown, Chad Edward
4 Carette, Jacques
4 Grabowski, Adam
4 Kohlhase, Andrea
4 Paulson, Lawrence Charles
4 Schubotz, Moritz
4 Steen, Alexander
4 Teschke, Olaf
3 Blanchette, Jasmin Christian
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 Sacerdoti Coen, Claudio
3 Siekmann, Jörg H.
3 Sorge, Volker
3 Wiesing, Tom
3 Wisniewski, Max
3 Woltzenlogel Paleo, Bruno
2 Ataeva, O. M.
2 Backes, Julian
2 Bancerek, Grzegorz
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 Lange, Christoph
2 Matuszewski, Roman
2 Meier, Andreas
2 Serebryakov, V. A.
2 Sperber, Wolfram
2 Stamerjohanns, Heinrich
2 Sultana, Nik
2 Sutcliffe, Geoff
2 Theiss, Frank
2 Tuchkova, Natal’ya Pavlovna
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 Barsotti, Damián
1 Bentkamp, Alexander
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
1 Eaton, Richard
1 Elizarov, A. M.
1 Fehrer, Detlef
1 Fiedler, Armin
1 Fitelson, Branden
1 Franke, Andreas
1 Freitag, Burkhard
1 Fuenmayor, David
...and 119 more Authors

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.