My research sits at the intersection of artificial intelligence, philosophy, mathematics, and natural language. A central theme is the use of classical higher-order logic (HOL) as a universal meta-logic for automating a wide range of non-classical logics, and deploying them in application areas such as machine ethics & law, metaphysics, and rational argumentation.
A key focus is the development of hybrid AI — combining symbolic and sub-symbolic techniques — to achieve trustworthy, explainable, and reasonable machines. Explicit, declarative knowledge representations are central to this vision, making normative and other knowledge transparent, robust, and communicable between humans and machines.
Together with colleagues and students I have developed the Leo theorem provers for classical and non-classical higher-order logics (LEO-II world champion 2010, LEO-III world champion 2019), and the LogiKEy workbench for ethical and legal reasoning (an overview on the use of LogiKEy in education is provided in LogiKEy_in_Education). Our work on Gödel's ontological argument — computer-assisted analysis of formal proofs for the existence of God — received global media coverage. The related lecture course on Computational Metaphysics was awarded the Central Teaching Award of Freie Universität Berlin.
Current news and group activities are on the AISE group news page at the University of Bamberg.
Before academia, Christoph Benzmüller was a competitive long-distance runner at German national level, training at the Olympic Centre in Saarbrücken. In 1990 he was German Champion (men's team) in cross-country running. He remains actively competing today in the M55 age group, consistently placing in the top 10 at German Masters Championships (e.g. DM Masters Gotha 2025: 9th place 800m and 6th place 1500m); see also LADV. His children Max, Carla, and Elena have taken up the running tradition.