Priv.-Doz. Dr.-Ing. Christoph Benzmüller

University of Luxembourg, Faculty of Science, Technology and Communication
Freie Universität Berlin, Department of Mathematics and Computer Science
Saarland University, Department of Computer Science

Email:    Url:

Biography CV Research Publications Presentations Teaching

Invited keynote, tba, Brazilian Symposium on Formal Methods , Recife, Brazil, December 2017
Invited keynote, tba, 3. BMG Tag, Berliner Mathematische Gesellschaft e.V., Berlin, November 2017
Invited keynote, Computational Metaphysics: The Virtues of Formal Proofs Beyond Math, 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), Campinas, Brazil, July 2017
Invited tutorial, Universal Logic Theorem Proving via Semantical Embeddings in HOL, 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), Campinas, Brazil, July 2017
Invited lecture, Computational Metaphysics: The Virtues of Formal Computer Proofs Beyond Maths and Computer Science, Commission for Computing (HaPoC)---25th International Congress of History of Science and Technology (HaPoC), Rio de Janeiro, Brazil, July 2017
Invited lecture, Calculemus!: Analyse von Kurt Gödel's Gottesbeweis mit dem Computer, Urania, Berlin, June 2017
Invited lecture, Computational Metaphysics: The Virtues of Formal Proofs Beyond Math, ILIAS Distinguished Lectures, University of Luxembourg, 2017
Invited lecture, Computational Metaphysics: The Virtues of Formal Proofs Beyond Math, Colloquium of the Berlin Mathematical School, Berlin, 2016 (slides)
Invited keynote panelist, The OEB Plenary Debate, The global, cross-sector conference on technology supported learning and training, Berlin, 2016
Invited big ideas talk, Künstliche Intelligenz -- Wohin geht die Reise?, 11. Jahresforum Shared Servives & Outsourcing Woche, Berlin, 2016
Invited keynote panelist, Erwachen der Roboter -- lernende Maschinen und die Intelligenz der Zukunft, Bundeszentrale für politische Bildung, Berlin, 2016

    Professional Interests
Logic and Formal Methods (in Computer Science, Artificial Intelligence, Philosophy, and Mathematics), Computational Metaphysics, Automated Reasoning, Artificial Intelligence, Theoretical Computer Science, Formal Methods, Computer-supported Mathematics, Computational Linguistics and Cognitive Science.

    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:
News: 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.

Visitors of my website are often interested in my ongoing work (in collaboration with Bruno Woltzenlogel Paleo) on the verification and automation of variants and emendations of Kurt Gödel's ontological argument for the existence of God. 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; see also the references therein. Btw, our experiments reported can be recomputed on various computer platforms; a convenient way is to use the experiment package at 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):
GCAI'2017 (co-chair), Deduktionstreffen'2017 (co-chair), CADE'2017 (pc member), FroCoS'2017 (pc member), ARCADE'2017 (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

    New/Recent Publications   (please obey copyrights; see also DBLP, Google Scholar; my Erdös number is 3)
Computer-Assisted Analysis of the Anderson-Hajek Controversy, Logica Universalis, 2017. (pdf)
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)
Cut-Elimination for Quantified Conditional Logic. J.Phil.Log., 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: Thu Jul 20 16:37:27 CEST 2017 )