Prof. Dr. Christoph Benzmueller

Professor

Academic Career

• 2007 Habilitation, Computer Science, Saarland University
• 1999 Dr.-Ing., Computer Science, Saarland University
• 1995 Dipl.-Inform., Computer Science, Saarland University

Professional Career

For more than a decade Christoph Benzmüller has been working at the boundary of AI, Computer Science, Computational Logic, (Computer-supported) Mathematics and Computational Linguistics. His main research interests include:

1. The collaborative development of large and integrated assistance systems for mathematics and formal methods.

2. The study of the theoretical foundations (model theory and proof theory) of higher-order logic.

3. The development of the cooperative higher-order/first-order theorem prover LEO-II and the development of an infrastructure for automated higher-order theorem proving.

The envisioned all-embracing assistance systems for mathematics and formal methods cover a wide range of typical characteristics an ambitious, integrated AI system shall have. Therefore, research goal (1) in addition to (2) and (3) requires the combination of techniques from several subfields of AI and Computer Science including knowledge representation and reasoning, knowledge bases and information systems, cognitive architectures and multi-agent systems, human computer interaction and user interfaces, machine learning, intelligent tutor systems, and dialog systems and natural language processing.

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, 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-II 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 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'.

Christoph is currently trustee of the Conference on Automated Deduction (CADE) and a steering committee member of the User Interfaces for Theorem Provers (UITP) workshop series. He was formerly 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 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 80 refereed publications in journals or at international conferences and workshops.

Research Interests include

• The collaborative development of large and integrated assistance systems for mathematics and formal methods.
• The study of the theoretical foundations (model theory and proof theory) of higher-order logic.
• The development of the cooperative higher-order/first-order theorem prover LEO-II and the development of an infrastructure for automated higher-order theorem proving. 

Publications

• Automating Access Control Logic in Simple Type Theory via LEO-II. 24th IFIP International Information Security Conference. Paphos, Cyprus, 2009. To appear.
• Cut-Simulation and Impredicativity. Logical Methods in Computer Science. 2009. To appear.
• Proof Step Analysis for Proof Tutoring – A Learning Approach to Granularity. Teaching Mathematics and Computer Science. 2009. In Print.
• LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. Fourth International Joint Conference on Automated Reasoning (IJCAR'08), LNAI vol. 5195, Sydney, Australia, 2008. Springer. ISBN 978-3-540-71069-1
• The Core TPTP Language for Classical Higher-Order Logic. Fourth International Joint Conference on Automated Reasoning (IJCAR'08), LNAI vol. 5195, Sydney, Australia, 2008. Springer. ISBN 978-3-540-71069-1
• Resource-bounded Modelling and Analysis of Human-level Interactive Proofs. In M. Crocker and J. Siekmann (eds.), Resource Adaptive Cognitive Systems. Cognitive Technologies Series. Springer. 2009. In print.
• OMEGA: Resource Adaptive Processes in an Automated Reasoning System. In M. Crocker and J. Siekmann (eds.), Resource Adaptive Cognitive Systems. Cognitive Technologies Series. Springer. 2009. In print.
• Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In C. Benzmüller, C. Brown, J. Siekmann and R. Statman (eds.), Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Studies in Logic and the Foundations of Mathematics. IFCoLog. 2009. In print.
• Cut Elimination with Xi-Functionality. In C. Benzmüller, C. Brown, J. Siekmann and R. Statman (eds.), Festschrift in Honour of Peter B. Andrews on his 70th Birthday. Studies in Logic and the Foundations of Mathematics. IFCoLog. 2009. In print.
• Jacques Herbrand: Life, Logic, and Automated Deduction. In D. Gabbay, J. Woods (eds.), The Handbook of the History of Logic, Volume 5, Logic and Sets from Russell to Church: Logic. Elsevier. Invited Chapter. 2009. In print.
• Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. Festschrift in Honour of Peter B. Andrews. 2009. To appear.
• Organisation, Transformation, and Propagation of Mathematical Knowledge in Omega, Mathematics in Computer Science, 2009. Birkhauser/Springer. In print.
• Combined Reasoning by Automated Cooperation. Journal of Applied Logic, (2008) 6(3):318-342. Elsevier.