Christoph Benzmüller

U Bamberg, Full Professor, Chair for AI Systems Engineering
FU Berlin, Professor (apl.) at the Dep. of Maths and Computer Science
Startup Industry, Scientific Advisor

 U Bamberg, An der Weberei 5, 96047 Bamberg
FU Berlin, Arnimallee 7, 14195 Berlin

http://christoph-benzmueller.de    https://www.uni-bamberg.de/aise/

Bio CV Publications Presentations Teaching

    Professional Interests
My research activities are interfacing the areas of artificial intelligence, philosophy, mathematics, computer science, and natural language. Current research focuses on the use of formal argumentation & explanation to achieve trustworthy AI systems, that is reasonable machines. I am particularly interested in the use of classical higher-order logic (HOL) as a universal meta-logic to automate various non-classical logics and to utilise them in topical application areas, including machine ethics & machine law, metaphysics (e.g. Gödel's ontological argument), mathematical foundations (e.g. category theory) and rational argumentation. My research activities also address the integration of automated reasoning, machine learning and agent-based architectures. I have a core expertise in classical higher-order logic (HOL), and I have contributed to its semantics and proof theory, and together with colleagues and students I have developed the Leo theorem provers for HOL.

    News: see the news page of my AISE group at U Bamberg


    Computational Metaphysics and The Ontological Argument:
In a collaboration with Bruno Woltzenlogel Paleo and others, I have analysed variants of Kurt Gödel's ontological argument for the existence of God on the computer. This work had a media repercussion on a global scale. Here is more information of this line of research.
Our related lecture concept on Computational Metaphysics won the central teaching award of Freie Universität Berlin. More information on the course: lecture course proposal and website/schedule.

    Projects (current and past, selection)
PetraKIP: Persönliches transparentes KI-basiertes Portfolio für die Lehrerbildung (BMBF)
NFDIxCS: National Research Data Infrastructure for and with Computer Science (DFG)
DFG AL2681: Fairness und Effizienz in Fahrzeug-Routing-Problemen (DFG, host of Dr. Aleksandrov)
DELIGHT: Deontic Logic for Epistemic Rights (FNR, Luxembourg)
7Markets: AI-supported Financial Brokering (BMBF Exist)
CRAP: Consistent Rational Argumentation in Politics (VolkswagenStiftung)
LEO-III: Higher-Order Theorem Prover (DFG)
CompMeta: Studies in Computational Metaphysics (DFG)
ONTOLEO: Higher-Order Ontology-Reasoning with LEO-II (DFG)
LEO-II: Higher-Order Theorem Prover (EPSRC, UK)
THFTPTP: An Infrastructure for Higher-order Automated Theorem Proving (ERC)
OMEGA: Agent-oriented Proof Planning (DFG)
DIALOG: NL-based Interaction with a Mathematics Assistance System (DFG)
CALCULEMUS: Integration of Symbolic Reasoning and Symbolic Computation (ERC)

    (Former) Hobbies
I was passionate middle and long-distance runner. In the early 90's I lived and trained at the Olympic Centre in Saarbrücken. In 1990 I was German Champion with the men's team in cross-country running. My personal records are: 52,8s (400m), 1:53min (800m), 2:25min (1000m), 3:49min (1500m), 8:16min (3000m), , 8:13min (3000m indoor), 9:11min (3000m Hi), 14:13min (5000m), 30:52min (10000m), 30:04min (10km road run). But these days I struggle to keep up with my children Max, Carla and Elena.

C. Benzmüller (Last modified: Thu Apr 10 10:01:10 +04 2025 )