Christoph Benzmüller, Dr. habil.
Professor

Freie Universität Berlin, Dep. of Maths and CS
University of Luxembourg, FSTC (Visiting Scholar)
Saarland University, Dep. of CS (Privatdozent)

Arnimallee 7, 14195 Berlin    Tel.: +49(0)30 838 75406/52485
Email: c.benzmueller@gmail.com    Url: http://christoph-benzmueller.de

Biography CV (short) Publications Presentations Teaching

    Professional Interests
My research activities are interfacing the areas of artificial intelligence, philosophy, mathematics, computer science, and natural language. Many of these activities draw on classical higher-order logic (HOL), which has is roots in the work by Russel and Church. I have contributed to the semantics and proof theory of HOL, and together with colleagues and students I have developed the Leo theorem provers for HOL. More recently I have been utilising HOL as a universal meta-logic to automate various non-classical logics in topical application areas, including machine ethics & machine law (responsible AI), rational argumentation, metaphysics, category theory, etc. Recent research also addresses the integration of automated reasoning and machine learning.

    News
PC Co-Chair of KI 2019: Advances in Artificial Intelligence -- 42th Annual German Conference on AI, Kassel, Germany
Keynote (video) at Mathematics and Reality conference (AISSQ 2018)
Keynote (video) at Intl. Conference on Deontic Logic and Normative Systems (DEON 2018)
Mentor for EXIST Business Start-up Grant '7Markets'
John-Jules Meyer Best Paper Award at the 14th International Conference on Deontic Logic and Normative Systems (DEON 2018)
Invited keynotes 2018: AISSQ 2018, SMT 2018, HaPoC@CiE 2018, DEON 2018, ML@U Bath 2018
Conference and Workshop Organisation: LuxLogAI 2018, RuleML+RR 2018, ARQNL 2018
PC Member: IJCAR 2018, GCAI 2018, Deduktionstreffen 2018, UITP 2018,
Computer-Formalisation of Ed Zalta's Principia-logico Metaphysica by Daniel Kirchner (paradox found; see Daniel's thesis).
Computer-Formalisation of (the main chapters of) Mel Fitting's Types, Tableaus, and Gödel's God by David Fuenmayor.

    Computational Metaphysics and The Ontological Argument:
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.

In a collaboration with Bruno Woltzenlogel Paleo and others, I have analysed variants of Kurt Gödel's ontological argument for the existence of God on the computer. 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, including: IJCAI-2016, ECAI-2014, Logica Universalis 2017, Savijnanam 2017, Science of Computer Programming 2018. Formalization sources, papers and various other related material are freely accessible via our github repository.

    Main Projects (current and past)
CRAP: Consistent Rational Argumentation in Politics
LuxLI: Legal Informatics Luxembourg
LEO-III: Higher-Order Theorem Prover (DFG-Gepris)
CompMeta: Studies in Computational Metaphysics (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


    Board Memberships:
Conference on Automated Deduction, Association for Automated Reasoning, Society of Deontic Logic and Normative Systems, Fachgruppe Deduktionssysteme der GI, IFCoLog, Logic Journal of the IGPL, Journal of Applied Logic, User Interfaces for Theorem Provers

    Recommended Recent Papers   (please obey copyrights; see also DBLP, Google Scholar, ORBI^lu; my Erdös number is 3)
Automating Free Logic in HOL, with an Experimental Application in Category Theory, JAR, 2019 (pdf)
Universal (Meta-)Logical Reasoning: Recent Successes, Science of Computer Programming, 2019 (pdf)
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL, AFP, 2018 (pdf)
Mechanizing Principia Logico-Metaphysica in Functional Type Theory, CoRR (submitted), 2018 (pdf)
Axiom Systems for Category Theory in Free Logic, AFP, 2018 (pdf)
A Dyadic Deontic Logic in HOL, DEON, 2018 (pdf)
The Higher-Order Theorem Prover Leo-III, IJCAR 2018 (arXiv preprints), 2018. (pdf)
A Deontic Logic Reasoning Infrastructure, CiE 2018, 2018. (pdf)
Theorem Provers for Every Normal Modal Logic, LPAR, 2017. (pdf)
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic, KI, 2017. (pdf)
Computer-Assisted Analysis of the Anderson-Hajek Controversy, Logica Universalis, 2017. (pdf)
Cut-Elimination for Quantified Conditional Logic. J.Phil.Log., 2017. (pdf) (doi)
The Modal Collapse as a Collapse of the Modal Square of Opposition, Studies in Universal Logic, 2016. (pdf)

    (Former) Hobbies
I was 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).

C. Benzmüller (Last modified: Fri Dec 7 10:15:45 CET 2018 )