OMDoc--An Open Markup Format for Mathematical Documents [version 1.2]: Foreword by Alan Bundy M Kohlhase Springer, 2006 | 478* | 2006 |

Ωmega: Towards a mathematical assistant C Benzmüller, L Cheikhrouhou, D Fehrer, A Fiedler, X Huang, M Kerber, ... Automated Deduction—CADE-14: 14th International Conference on Automated …, 1997 | 239 | 1997 |

Mathematical markup language (MathML) version 2.0 . W3C Recommendation R Ausbrooks, S Buswell, D Carlisle, S Dalmas, S Devitt, A Diaz, ... World Wide Web Consortium 2003, 2003 | 227 | 2003 |

A search engine for mathematical formulae M Kohlhase, I Sucan International conference on artificial intelligence and symbolic computation …, 2006 | 218 | 2006 |

The open math standard S Buswell, O Caprotti, DP Carlisle, MC Dewar, M Gaetano, M Kohlhase version 2.0. Technical report, The Open Math Society, 2004. http://www …, 2004 | 191 | 2004 |

A scalable module system F Rabe, M Kohlhase Information and Computation 230, 1-54, 2013 | 161 | 2013 |

Higher-order semantics and extensionality C Benzmüller, CE Brown, M Kohlhase The Journal of Symbolic Logic 69 (4), 1027-1088, 2004 | 146 | 2004 |

Mbase: Representing knowledge and context for the integration of mathematical software systems M Kohlhase, A Franke Journal of Symbolic Computation 32 (4), 365-402, 2001 | 140 | 2001 |

Omdoc: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge M Kohlhase Artificial Intelligence and Symbolic Computation: International Conference …, 2001 | 130 | 2001 |

Inference and computational semantics P Blackburn, J Bos, M Kohlhase, H De Nivelle Computing Meaning: Volume 2, 11-28, 2001 | 122 | 2001 |

Proof Development with Ωmega J Siekmann, C Benzmüller, V Brezhnev, L Cheikhrouhou, A Fiedler, ... Automated Deduction—CADE-18: 18th International Conference on Automated …, 2002 | 114 | 2002 |

System description: LEO—a higher-order theorem prover C Benzmüller, M Kohlhase International Conference on Automated Deduction, 139-143, 1998 | 112 | 1998 |

Using as a semantic markup format M Kohlhase Mathematics in Computer Science 2, 279-304, 2008 | 111 | 2008 |

NTCIR-11 Math-2 Task Overview. A Aizawa, M Kohlhase, I Ounis, M Schubotz NTCIR 11, 88-98, 2014 | 102 | 2014 |

NTCIR-12 MathIR Task Overview. R Zanibbi, A Aizawa, M Kohlhase, I Ounis, Goran Topic, K Davila NTCIR, 2016 | 98 | 2016 |

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving H Ganzinger, A Franke, M Kohlhase Automated Deduction—CADE-16: 16th International Conference on Automated …, 1999 | 88 | 1999 |

NTCIR-10 Math Pilot Task Overview. A Aizawa, M Kohlhase, I Ounis NTCIR, 2013 | 86 | 2013 |

Agent-Oriented Integration of Distributed Mathematical Services. A Franke, SM Hess, CG Jung, M Kohlhase, V Sorge J. Univers. Comput. Sci. 5 (3), 156-187, 1999 | 86 | 1999 |

Integrating computer algebra into proof planning M Kerber, M Kohlhase, V Sorge Journal of Automated Reasoning 21, 327-355, 1998 | 84 | 1998 |

Ω-MKRP: A proof development environment X Huang, M Kerber, M Kohlhase, E Melis, D Nesmith, J Richts, ... Automated Deduction—CADE-12: 12th International Conference on Automated …, 1994 | 83 | 1994 |