PD Dr. Christoph Benzmüller

Heisenberg Fellow of the German Research Foundation

FU Berlin, Maths and Computer Science, Arnimallee 7, 14195 Berlin
Stanford U, CSLI/Cordula Hall, Stanford, CA 94305, USA

Tel.: +49(0)30 838 75406/52485   
Email: c.benzmueller@fu-berlin.de    Url: http://christoph-benzmueller.de

Biography CV Research Publications Presentations Teaching

    Professional Interests
Logic (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, Max Haslbeck, Frank Theiss, Hans-Jörg Schurr, Maximilian Claus, Kim Kern, Samuel Gfröer, Marco Ziener

    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, Detector.fm, 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 recomputation.org. Formalization sources, papers and various other related material are freely accessible via our github repository.

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

    Recommended Events (personal involvement):
CIPPMI'2016 (invited course), GCAI'2016 (co-chair), ARQNL'2016 (co-chair), PAAR'2016 (PC member), UITP'2016 (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

    Some Recent Publications   (please obey copyrights; see also DBLP, Google Scholar; my Erdös number is 3)
The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics, IJCAI, 2016, to appear (pdf)
The Modal Collapse as a Collapse of the Modal Square of Opposition, Studies in Universal Logic, 2016, to appear (pdf)
Effective Normalization Techniques for HOL, IJCAR, 2016, to appear (pdf)
Cut-Elimination for Quantified Conditional Logic. JPL, 2016, to appear, (pdf)
The Higher-Order Prover LEO-II. JAR, 2015. (pdf)
Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics. Tableaux, 2015. (pdf)
There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners. LPAR, 2015. (pdf)
Higher-Order Modal Logic: Automation and Applications. RW, 2015. (pdf)
Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP@CADE-25, 2015. (pdf)
LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners. CICM, 2015. (pdf)
Interacting with Modal Logics in the Coq Proof Assistant. CSR, 2015. (pdf)
Computer-Assisted Analysis of the Anderson-Hajek Ontological Controversy, Congress on Logic and Religion, 2015. (pdf)
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Prover. ECAI, 2014. (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). Since 2004 I am occasionally starting again in some street races; here are some recent results. Since around the same time, I have also become an enthusiastic diver. Furthermore, I like skiing.

C. Benzmüller (Last modified: Sun May 15 19:54:21 CEST 2016 )