Christoph Benzmüller
Heisenberg Fellow of the German Research Foundation, Freie Universität Berlin & Heisenberg Research Fellow of the DFG, Germany
In 2012, Christoph Benzmüller was awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG). In this position he is currently affiliated with Freie Universität Berlin, Germany, where he holds a venia legendi in Mathematics and Computer Science, and with Stanford University, CSLI/Cordula Hall, CA, USA. Previously, Christoph held positions as a full professor at the International University in Bruchsal, Germany, and as an Associate and Assistant Professor at Saarland University, Saarbrücken, Germany.
Christoph received his PhD (1999) and his Habilitation (2007) in computer science from Saarland University. His PhD, titled 'Equality and Extensionality in Higher-Order Theorem Proving', was supported by a grant of the 'Studienstiftung des Deutschen Volkes' and was partly conducted at Carnegie Mellon University, Pittsburgh, USA. Core research interests of Christoph include the theory, implementation, and application of reasoning systems for expressive logics, including classical and non-classical first-order and higher-order logics.
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).
Prior to his academia career, Christoph Benzmüller was a successful long-distance runner at German national level.
Links
http://christoph-benzmueller.de