Academic Qualifications

2008, Full Professor, International University in Germany, Bruchsal

2007, Habilitation, Computer Science, Saarland University

1999, Dr.-Ing., Computer Science, Saarland University

1995, Dipl.-Inform., Computer Science, Saarland University

Christoph received his MSc, PhD and Habilitation in Computer Science from Saarland University, Germany and his PhD research on semantics and automation of higher-order logic, which he partly conducted at Carnegie Mellon University in Pittsburgh, USA, has been supported by a grant of the German 'Studienstiftung des Deutschen Volkes'. He is the main developer of the automated higher-order theorem prover LEO which he reimplemented and improved in the research project LEO-II with Prof. Lawrence Paulson in 2007 at Cambridge University, UK. Christoph Benzmüller has also been working at the boundry of Computational Logic, Artificial Intelligence, Computational Linguistics and Computer-supported Mathematics in several projects at Saarland University, Germany, The University of Birmingham, England, and the University of Edinburgh, Scotland. He was head of the OMEGA group of Prof. Jörg Siekmann at Saarland University (2001-2007), he served as scientific coordinator of the European Union 5th Framework Research Training Network 'CALCULEMUS: Systems for integrated Computation and Deduction' (2000-2004), and he was principal investigator of four projects in the DFG Collaborative Research Center on Resource-adaptive Cognitive Processes (SFB 378) at Saarland University between 2001 and 2008. This includes the projects 'DIALOG: Natural language-based Interaction with a Mathematical Assistant System' and 'OMEGA: Agent-oriented Proof Planning'. The latest research activities of Christoph Benzmüller include the automation of quantified multi-modal logics and access control logics (as natural fragments of higher-order logic) and the automation of challenge aspects (such as modalities and time) in ontology reasoning. In the latter research Christoph cooperated with Articulate Software, Angwin, CA, in a DFG-Forschungsstipendium.

Christoph is an executive officer of The International Federation for Computational Logic (IFCOLOG), and a steering committee member of the User Interfaces for Theorem Provers (UITP) workshop series. He was formerly a trustee of the Conference on Automated Deduction (CADE), a trustee of CALCULEMUS and a steering committee member of the International Joint Conference on Automated Reasoning (IJCAR). Moreover, he is editorial board member of the Journal of Applied Logic, the Logic Journal of the IGPL, and the Journal of Algorithms in Cognition, Informatics and Logic. He served as chair of more than 10 international workshops and he was main organizer and programme chair of the European Union CALCULEMUS summer school in Pisa in 2002. He is co-author of more than 100 refereed publications in journals or at international conferences and workshops.

http://christoph-benzmueller.de