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
● Keynote speaker of FLAIRS-36
● Co-organizer and lecturer 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 with Springer: What follows from the non-existence of time? Selected contributions to the Kurt-Gödel essay competition 2021
● New preprint: Who Finds the Short Proof?
● 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
● PCs: CLAR (co-chair), ESSLLI (area co-chair, 2022), CADE, DEON, FroCoS, ITP, KI, LNGAI, ARCADE, PhDsInLogic

    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)
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: 2:25min (1000m), 3:49min (1500m), 8:14min (3000m), 14:13min (5000m), 30:04min (10000m).


C. Benzmüller (Last modified: Wed Sep 14 10:46:08 CEST 2022 )