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.
First Publications: Archive of Formal Proofs, ArXiv preprint
Media: Telepolis, Spiegel Online, Spiegel Online Intl., Die Welt, Wiener Zeitung, many more links worldwide
Formalizations: THF, THF-TPI, Isabelle, Coq

    Main Projects (current and past)
ONTOLEO: Higher-Order Ontology-Reasoning with LEO-II
LEO-II: An Effective 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), ARQNL'2014 (co-organizer), UITP'2014 (co-organizer), FOIS'2014 (PC member), ICAART'2014 (PC member), PAAR'2014 (PC member), ARWDT'2014 (PC member),

    Some Recent Publications   (please obey existing copyrights; see also DBLP, Google Scholar; my Erdös number is 3)
Automation of Higher-Order Logic. Handbook of History of Logic, 2014. (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: Tue Mar 25 13:02:21 CET 2014 )