Short Biography: Christoph Benzmüller

Christoph Benzmüller is affiliated as Privatdozent for Computer Science and Mathematics with Freie Universität Berlin and Saarland University, Saarbrücken. At present, he is visiting University of Luxemburg. Previous research stations of Christoph include Stanford University, USA (visiting scholar), Articulate Software, USA (senior researcher), Intl. University of Germany, Bruchsal (full professor), University of Cambridge, UK (senior researcher), Saarland University (associate professor), University of Birmingham, UK and the University of Edinburgh, UK (postdoc).

Christoph received his PhD (1999) and his Habilitation (2007) in computer science from Saarland University. His PhD was partly conducted at Carnegie Mellon University, USA. In 2012, Christoph had been awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG).

Christoph is an expert in higher-order automated and interactive theorem proving, which he utilises as a basis for an approach towards universal logic reasoning. His broader interests concern all aspects of knowledge representation and reasoning. Moreover, Christoph is well known for his interdisciplinary applications. Most recently, for example, he has pioneered, together with colleagues, the area of computational metaphysics.

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 serves in various further functions (chair, editorial board, steering committee, trustee, etc.) for various conferences and organisations.

Prior to his academia career, Christoph Benzmüller was a successful long-distance runner at German national level.