PD Dr. Christoph Benzmüller

Heisenberg Fellow of the German Research Foundation

Department of Mathematics and Computer Science
Arnimallee 7, Room 115, 14195 Berlin

Tel.: +49(0)30 838 75102/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), Automated Reasoning, Artificial Intelligence, Theoretical Computer Science, Formal Methods, Computer-supported Mathematics, Computational Linguistics and Cognitive Science.

    Research Group / Students
Max Wisniewski (PhD student), Alexander Steen (PhD student), Frank Theiss (PhD student), Benjamin Eckstein (MSc student), Maximilian Claus (MSc student), Jan Gütig (BSc student), Kim Kern (BSc student)

    Latest Research: Formalization, verification and automation of Kurt Gödel's ontological proof of God's existence.
Publications (please obey copyrights): ECAI-2014, Archive of Formal Proofs, ArXiv preprint
Media Coverage: Telepolis, Spiegel Online, Spiegel Online Intl., Die Welt, Wiener Zeitung, many more links worldwide
Formalizations: THF, THF-TPI, Isabelle, Coq
Experiments (easy recomputation): at Recomputation.org,

    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):
CADE-25 (conference chair, PC member), DT'2015 (organizer), 1st World Congress on Logic and Religion (invited speaker), LogInf 2014 (invited speaker), FroCoS'2015 (PC member), ICAART'2015 (PC member), ARQNL'2014 (co-organizer), UITP'2014 (co-organizer), WADT'2014 (invited speaker), APPA'2014 (invited speaker), FOIS'2014 (PC member), PAAR'2014 (PC member), ARWDT'2014 (PC member)

    Board Memberships:
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)
Computer-Assisted Analysis of the Anderson-Hajek Ontological Controversy, Congress on Logic and Religion, 2015 (to appear).
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Prover. ECAI, 2014. (pdf)
Higher-Order Automated Theorem Provers. Chapter in: All about Proofs, Proofs for All, College Publications, 2014 (to appear). (pdf)
Automation of Higher-Order Logic. Handbook of History of Logic, 2014 (to appear). (pdf)
HOL Based First-Order Modal Logic Provers. LPAR, 2013. (pdf)
Automating Quantified Conditional Logics in HOL. IJCAI, 2013. (pdf)
A Top-down Approach to Combining Logics, ICAART, 2013. (pdf)
Sigma: An Integrated Development Environment for Formal Ontology. AI Communications, 2013. (pdf)
Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, 2013. (pdf)
Implementing and Evaluating Provers for First-order Modal Logics. ECAI, 2012. (pdf)
Embedding and Automating Conditional Logics in Classical Higher-Order Logic. Ann Math Artif Intell, 2012. (pdf)
Higher-Order Aspects and Context in SUMO, Journal of Web Semantics, 2012. (pdf)

    Hobbies
I am still a passionate middle and long-distance runner. More than a decade ago 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. Recently, I have also become an enthusiastic diver. Furthermore, I like skiing.


C. Benzmüller (Last modified: Thu Nov 27 13:56:58 CET 2014 )