Priv.-Doz. Dr. Christoph Benzmüller

University of Luxembourg, FSTC
Freie Universität Berlin, Dep. of Maths and CS
Saarland University, Dep. CS

Email:    Url:

Biography CV (short) Trackrecord Publications Presentations Teaching

    Professional Interests
My research interests are in the intersection of AI, Computer Science, Mathematics, Philosophy and Natural Language. Many of my research activities draw on Classical Higher-Order Logic (HOL), which has is roots in the work by Church and Russel. I have contributed to the semantics and proof theory of HOL, and together with colleagues and students I have developed the Leo theorem provers for HOL. I have utilised HOL as a universal meta-logic to encode and apply various non-classical logics in a wide range of applications in the mentioned research areas. In recent projects I further develop and apply this universal reasoning technique in Computational Metaphysics, Rational Argumentation, Machine Ethics/Law, Category Theory, etc.

Invited keynote, 14th International Conference on Deontic Logic and Normative Systems, Utrecht, 2018
Invited lecture, From Computational Metaphysics towards Computational (Pseudo-)Ethics, Thematic Semester on Machine Learning: Algorithms and Ethics at the Institute of Mathematical Innovation of U Bath, UK, 2018
Invited lecture, HaPoC special session, celebrating Martin Davis' 90th birthday, CiE Kiel, 2018
Conference, LuxLogAI 2018: Luxembourg Logic for AI Summit 2018 (flyer)
Conference, RuleML+RR 2018, Luxembourg
Computer-Formalisation of Ed Zalta's Principia-logico Metaphysica by Daniel Kirchner (paradox found; see Daniel's thesis).
Computer-Formalisation of (the main chapters of) Mel Fitting's Types, Tableaus, and Gödel's God by David Fuenmayor.

    Research Group / Students
Max Wisniewski, Alexander Steen, Frank Theiss, Hans-Jörg Schurr, Maximilian Claus, Daniel Kirchner, Fabian Schütz, Hanna Lachnitt, David Fuenmayor, David Streit, Marco Ziener, Irina Makarenko, Tobias Gleißner (Interested in joining the team? See here for open topics.)

    Computational Metaphysics and The Ontological Argument:
Our 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.

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. There are various articles (e.g., Spiegel Online Intl., Die Welt, Wiener Zeitung, Spiegel Online) and interviews (e.g., Telepolis, PC Zoznam,, ORF); a selection of further links to reports worldwide is available here. Unfortunately, and probably unavoidable, there are also a few ill informed, trashy reports like this one. If you want to learn more about our scientific work (and about what we did and what we didn't), then you may have a look at our (peer reviewed) papers at IJCAI-2016 and ECAI-2014 conferences, and in Logica Universalis 2017; see also the references therein. Formalization sources, papers and various other related material are freely accessible via our github repository.

    Main Projects (current and past)
CompMeta: Studies in Computational Metaphysics (DFG-Gepris)
LEO-III: Higher-Order Theorem Prover (DFG-Gepris)
ONTOLEO: Higher-Order Ontology-Reasoning with LEO-II (DFG-Gepris)
LEO-II: Higher-Order Theorem Prover
THFTPTP: An Infrastructure for Higher-order Automated Theorem Proving
OMEGA: Agent-oriented Proof Planning (DFG-Gepris)
DIALOG: NL-based Interaction with a Mathematics Assistance System (DFG-Gepris)
CALCULEMUS: Integration of Symbolic Reasoning and Symbolic Computation

    Recommended Events (personal involvement):
LuxLogAI'2018 (orga team), RuleML+RR'2018 (pc co-chair), ARQNL'2018 (pc co-chair), Deduktionstreffen'2018 (pc co-chair), IJCAR'2018 (pc member), UITP'2018 (pc member),

    Board Memberships:
Conference on Automated Deduction, Association for Automated Reasoning, Fachgruppe Deduktionssysteme der GI, IFCoLog, Logic Journal of the IGPL, Journal of Applied Logic, User Interfaces for Theorem Provers

    Recommended Recent Papers   (please obey copyrights; see also DBLP, Google Scholar; my Erdös number is 3)
Theorem Provers for Every Normal Modal Logic, LPAR, 2017. (pdf)
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic, KI, 2017. (pdf)
Universal Reasoning, Rational Argumentation and Human-Machine Interaction, arXiv, 2017. (pdf)
Computer-Assisted Analysis of the Anderson-Hajek Controversy, Logica Universalis, 2017. (pdf)
Cut-Elimination for Quantified Conditional Logic. J.Phil.Log., 2017. (pdf) (doi)
The Modal Collapse as a Collapse of the Modal Square of Opposition, Studies in Universal Logic, 2016. (pdf)
Axiomatizing Category Theory in Free Logic, arXiv, 2016. (pdf)
Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic, Logic and Logical Philosophy, 2016. (pdf)
Automating Free Logic in Isabelle/HOL. ICMS, 2016. (pdf) (doi)
The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics, IJCAI, 2016. (pdf)

I am still a 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:14 (3000m), 14:13min (5000m), 30:04min (10000m). I am still occasionally starting in some street races; here are some results. Since around the same time, I have also become an enthusiastic diver. Furthermore, I like skiing.

C. Benzmüller (Last modified: Wed Feb 21 10:30:05 CET 2018 )