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.

    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), 1st World Congress on Logic and Religion (invited speaker), LogInf 2014 (invited speaker), 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)
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Prover. ECAI, 2014 (to appear). (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)

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: Tue Sep 16 12:54:35 CEST 2014 )