Christoph Benzmüller – Heisenberg Fellow of the German Research Foundation
Research topics: Logic (in CS, AI, Philosophy, Maths, Computational Linguistics), Knowledge Representation and Reasoning, Automated and Interactive Theorem Proving, Formal Ontologies, Computational Metaphysics, Type theory
| Christoph is well known for his automated higher-order theorem provers LEO-I and LEO-II. The latter system was developed in a project at Cambridge University, UK (2006-2007). Previously, Christoph has also been working at the boundry of computational logic, artificial intelligence, computational linguistics and computer-supported mathematics in several projects at Saarland University, the University of Birmingham, UK, and the University of Edinburgh, UK. The latest research activities of Christoph include the automation of various quantified non-classical logics logics as natural fragments of classical higher-order logic, and the automation of challenge aspects, in particular, modal contexts, in ontology reasoning. In the latter research Christoph cooperated with Articulate Software, Angwin, CA, USA (2008-2011). Recently, Christoph received major international recognition for his work (with B. Woltzenlogel-Paleo) on the formalization and automation of Kurt Gödel’s ontological argument for the existence of God on the computer.
Christoph is trustee and vice-president of CADE (Conference on Automated Deduction), board member of AAR (Association of Automated Reasoning) and spokesman of the section Deduction Systems of the Gesellschaft für Informatik. He is editorial board member of the Journal of Applied Logic and the Logic Journal of the IGPL, and a permanent steering committee member of the User Interfaces for Theorem Provers workshop series. Moreover, he served as a trustee or steering committee member of several other conferences and he is an executive officer of The International Federation for Computational Logic (IFCoLog).
|
 Christoph Benzmüller |