×

zbMATH — the first resource for mathematics

Kohlhase, Michael

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 · Wikidata · ORCID · dblp · GND
Documents Indexed: 105 Publications since 1992, including 4 Books
all top 5

Co-Authors

10 single-authored
28 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, Alexander B.
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

67 Publications have been cited 258 times in 144 Documents Cited by Year
A scalable module system. Zbl 1358.68283
Rabe, Florian; Kohlhase, Michael
26
2013
Higher-order semantics and extensionality. Zbl 1071.03024
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
19
2004
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
12
2013
Project abstract: logic atlas and integrator (LATIN). Zbl 1278.68285
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
12
2011
Using LaTEX as a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
9
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
OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge. Zbl 1042.00511
Kohlhase, Michael
7
2001
Towards logical frameworks in the heterogeneous tool set Hets. Zbl 1278.68286
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina
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
Cut-simulation and impredicativity. Zbl 1160.03004
Benzmüller, Christoph E.; Brown, Chad E.; Kohlhase, Michael
6
2009
Notations for living mathematical documents. Zbl 1166.00304
Kohlhase, Michael; Müller, Christine; Rabe, Florian
6
2008
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
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
5
2014
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
5
2012
Transforming large collections of scientific publications to XML. Zbl 1205.68490
Stamerjohanns, Heinrich; Kohlhase, Michael; Ginev, Deyan; David, Catalin; Miller, Bruce
4
2010
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
System description: The MathWeb software bus for distributed mathematical reasoning. Zbl 1072.68601
Zimmer, Jürgen; Kohlhase, Michael
4
2002
Agent-oriented integration of distributed mathematical services. Zbl 0961.68117
Franke, Andreas; Hess, Stephan M.; Jung, Christoph G.; Kohlhase, Michael; Sorge, Volker
4
1999
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
Kohlhase, Michael
3
2014
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
3
2014
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
3
2014
A data model and encoding for a semantic, multilingual terminology of mathematics. Zbl 1304.68173
Kohlhase, Michael
3
2014
The LaTeXML daemon: editable math on the collaborative web. Zbl 1278.68337
Ginev, Deyan; Stamerjohanns, Heinrich; Miller, Bruce R.; Kohlhase, Michael
3
2011
Extended formula normalization for \(\epsilon \)-retrieval and sharing of mathematical knowledge. Zbl 1202.68157
Normann, Immanuel; Kohlhase, Michael
3
2007
Higher-order automated theorem proving. Zbl 0971.68141
Kohlhase, Michael
3
1998
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 07036055
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
2
2017
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
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
MathWebSearch 0.5: scaling an open formula search engine. Zbl 1278.68296
Kohlhase, Michael; Matican, Bogdan A.; Prodescu, Corneliu-Claudiu
2
2012
STEXIDE: an integrated development environment for STEX collections. Zbl 1278.68294
Jucovschi, Constantin; Kohlhase, Michael
2
2010
Towards context-based disambiguation of mathematical expressions. Zbl 1186.68530
Grigore, Mihai; Wolska, Magdalena; 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
Communities of practice in MKM: an extensional model. Zbl 1188.68281
Kohlhase, Andrea; Kohlhase, Michael
2
2006
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
2
2006
MBase: Representing knowledge and context for the integration of mathematical software systems. Zbl 0981.68153
Kohlhase, Michael; Franke, Andreas
2
2001
Managing structural information by higher-order colored unification. Zbl 0959.03007
Hutter, Dieter; Kohlhase, Michael
2
2000
A tableau claculus for partial functions. Zbl 0851.03004
Kerber, Manfred; Kohlhase, Michael
2
1996
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
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
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
Kohlhase, Michael (ed.); Johansson, Moa (ed.); Miller, Bruce (ed.); de Moura, Leonardo (ed.); Tompa, Frank (ed.)
1
2016
Representing, archiving, and searching the space of mathematical knowledge. Zbl 1403.68280
Iancu, Mihnea; Kohlhase, Michael; Prodescu, Corneliu
1
2014
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
1
2012
The Planetary project: towards eMath3.0. Zbl 1278.68339
Kohlhase, Michael
1
2012
Semantic alliance: a framework for semantic allies. Zbl 1278.68298
David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael
1
2012
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
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
A mathematical approach to ontology authoring and documentation. Zbl 1247.68279
Lange, Christoph; Kohlhase, Michael
1
2009
Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275
Kohlhase, Andrea; Kohlhase, Michael
1
2009
Unifying math ontologies: a tale of two standards. Zbl 1247.68268
Davenport, James H.; Kohlhase, Michael
1
2009
Capturing the content of physics: systems, observables, and experiments. Zbl 1188.68279
Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich
1
2006
Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Zbl 1096.68004
Kohlhase, Michael (ed.)
1
2006
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
Communication protocols for mathematical services based on KQML and OMRS. Zbl 0986.68003
Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio
1
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
Kerber, Manfred (ed.); Kohlhase, Michael (ed.)
1
2001
System description: MBase, an open mathematical knowledge base. Zbl 0963.68543
Franke, Andreas; Kohlhase, Michael
1
2000
MBase: Representing mathematical knowledge in a relational data base. Zbl 0958.68163
Franke, Andreas; Kohlhase, Michael
1
1999
Extensional higher-order resolution. Zbl 0928.03004
Benzmüller, Christoph; Kohlhase, Michael
1
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 mechanization of strong Kleene logic for partial functions. Zbl 1433.03024
Kerber, Manfred; Kohlhase, Michael
1
1994
Virtual theories – a uniform interface to mathematical knowledge bases. Zbl 07036055
Wiesing, Tom; Kohlhase, Michael; Rabe, Florian
2
2017
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
2
2017
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
QED reloaded: towards a pluralistic formal library of mathematical knowledge. Zbl 1451.68343
Kohlhase, Michael; Rabe, Florian
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
Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Zbl 1342.68025
Kohlhase, Michael (ed.); Johansson, Moa (ed.); Miller, Bruce (ed.); de Moura, Leonardo (ed.); Tompa, Frank (ed.)
1
2016
Flexary operators for formalized mathematics. Zbl 1304.68171
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael
5
2014
Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Zbl 1317.68241
Kohlhase, Michael
3
2014
System description: MathHub.info. Zbl 1304.68196
Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom
3
2014
Realms: a structure for consolidating knowledge about mathematical theories. Zbl 1304.68169
Carette, Jacques; Farmer, William M.; Kohlhase, Michael
3
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
26
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
12
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
6
2012
Extending MKM formats at the statement level. Zbl 1278.68293
Horozal, Fulya; Kohlhase, Michael; Rabe, Florian
5
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
1
2012
The Planetary project: towards eMath3.0. Zbl 1278.68339
Kohlhase, Michael
1
2012
Semantic alliance: a framework for semantic allies. Zbl 1278.68298
David, Catalin; Jucovschi, Constantin; Kohlhase, Andrea; Kohlhase, Michael
1
2012
A proof theoretic interpretation of model theoretic hiding. Zbl 1278.68202
Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian
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
12
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
6
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
2
2009
Spreadsheet interaction with frames: exploring a mathematical practice. Zbl 1247.68274
Kohlhase, Andrea; Kohlhase, Michael
2
2009
A mathematical approach to ontology authoring and documentation. Zbl 1247.68279
Lange, Christoph; Kohlhase, Michael
1
2009
Compensating the computational bias of spreadsheets with MKM techniques. Zbl 1247.68275
Kohlhase, Andrea; Kohlhase, Michael
1
2009
Unifying math ontologies: a tale of two standards. Zbl 1247.68268
Davenport, James H.; Kohlhase, Michael
1
2009
Using LaTEX as a semantic markup format. Zbl 1176.68230
Kohlhase, Michael
9
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
Communities of practice in MKM: an extensional model. Zbl 1188.68281
Kohlhase, Andrea; Kohlhase, Michael
2
2006
An exploration in the space of mathematical knowledge. Zbl 1151.68666
Kohlhase, Andrea; Kohlhase, Michael
2
2006
Capturing the content of physics: systems, observables, and experiments. Zbl 1188.68279
Hilf, Eberhard R.; Kohlhase, Michael; Stamerjohanns, Heinrich
1
2006
Mathematical knowledge management. 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005. Revised selected papers. Zbl 1096.68004
Kohlhase, Michael (ed.)
1
2006
Higher-order semantics and extensionality. Zbl 1071.03024
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael
19
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
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
Kerber, Manfred (ed.); Kohlhase, Michael (ed.)
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
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
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
1
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
1
1994
Unification in order-sorted type theory. Zbl 0925.03080
Kohlhase, Michael
3
1992
all top 5

Cited by 206 Authors

34 Kohlhase, Michael
19 Benzmüller, Christoph Ewald
19 Rabe, Florian
9 Kaliszyk, Cezary
7 Naumowicz, Adam
6 Farmer, William M.
6 Horozal, Fulya
6 Iancu, Mihnea
6 Korniłowicz, Artur
6 Pąk, Karol
5 Urban, Josef
4 Autexier, Serge
4 Carette, Jacques
4 Grabowski, Adam
4 Kohlhase, Andrea
4 Paulson, Lawrence Charles
3 Brown, Chad Edward
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 Schubotz, Moritz
3 Siekmann, Jörg H.
3 Sorge, Volker
3 Steen, Alexander
3 Teschke, Olaf
3 Wiesing, Tom
3 Wisniewski, Max
3 Woltzenlogel Paleo, Bruno
2 Ataeva, O. M.
2 Bancerek, Grzegorz
2 Blanchette, Jasmin Christian
2 Byliński, Czesław
2 Caprotti, Olga
2 Codescu, Mihai
2 David, Catalin
2 Guidi, Ferruccio
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, N. P.
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 Backes, Julian
1 Barsotti, Damián
1 Berčič, Katja
1 Bickford, Mark
1 Billingsley, William
1 Brucker, Achim D.
1 Cairns, Paul
1 Carter, Nathan C.
1 Cheikhrouhou, Lassaad
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 de Nivelle, Hans
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
1 Fürsich, Michael
1 Futatsugi, Kokichi
1 Gabbay, Murdoch James
1 Gast, Holger
1 Geuvers, Jan Herman
1 Giceva, Jana
...and 106 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.