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

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 also the news page of my AISE group at U Bamberg)
● New article to appear in JANCL: Conditional Normative Reasoning as a Fragment of HOL
● Visiting professor/scholar from October 2023 until March 2024 at BITS Pilani, Dubai Campus, UAE
KI Insights and a Global Perspective on AI, online talk and discussion for/with the Association of German Scientists (VDW)
High-end foreign expert (for machine ethics in cross-cultural context) at Zheijang University, Huangzhou, China
● Keynote at CINS 2023, Dubai, UAE
● PC co-chair of IJCAR 2024, the premier conference on all aspects of automated reasoning
● New book: On Gödel and the Nonexistence of Time
● New article in LJ.IGPL: Who Finds the Short Proof?
● Keynote speaker of FLAIRS-36
● Co-organizer and speaker of the Goethe-Institute AI & Ethics Summer School at U Bamberg
● New article in Zygon: Symbolic AI and Gödel's Ontological Argument
● Jury member of the Kurt Gödel Award 2023
● Forthcoming book chapter: A Simplified Variant of Gödel's Ontological Argument
● Since 2022 I am full professor for AI systems engineering at the University of Bamberg
Keynote at the Inauguaration Ceremony of ZLAIRE, the Zhejiang U--U Luxembourg Joint Lab on Advanced Intelligent Systems and REasoning, 2021
● Winner of the Wissensstadt Berlin 2021 Science Slam of FU Berlin with my contribution on Trustworthy AI
● Event: First German National CLAIRE Meeting on Trusted AI
● New book: Logic and Argumentation, Springer Lecture Notes in AI
● New book: Wider den Reduktionismus, Springer Spektrum
● Research Manifesto: Reasonable Machines and Träumen vernünftige Maschinen von Gründen? Eine reale Utopie

    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)

    Board Memberships (selection):
CLAIRE-AI (national contact point), Conference on Automated Deduction, Association for Automated Reasoning, Society of Deontic Logic and Normative Systems, Berlin Mathematics Research Center MATH+, Berlin Mathematical School, Fachgruppe Deduktionssysteme der GI, IFCoLog, Logic Journal of the IGPL, Journal of Applied Logics

    (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. Feel free to beat some of my personal records: 52,8s (400m), 1:53min (800m), 2:25min (1000m), 3:49min (1500m), 8:14min (3000m), 9:11min (3000m Hi), 14:13min (5000m), 30:52min (10000m), 30:04min (10km).

C. Benzmüller (Last modified: Sat Jun 8 20:51:28 CEST 2024 )