Professor Dr. habil.
Christoph Benzmüller

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 52485
Url: http://christoph-benzmueller.de

Bio Publications Presentations Teaching

    Professional Interests
My research activities are interfacing the areas of artificial intelligence, philosophy, mathematics, computer science, and natural language. I am particularly interested in the use of classical higher-order logic (HOL) as a universal meta-logic to automate various non-classical logics and to utilise them in topical application areas, including machine ethics & machine law (responsible AI), metaphysics (e.g. Gödel's ontological argument), mathematical foundations (e.g. category theory) and rational argumentation. My research activities also address the integration of automated reasoning, machine learning and agent-based architectures. I have a core expertise in classical higher-order logic (HOL), and I have contributed to its semantics and proof theory, and together with colleagues and students I have developed the Leo theorem provers for HOL.

    News
• Preprints: Reasonable Machines: A Research Manifesto, KI2020, and Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic, 2020 (submitted)
• Preprint: Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support, Artificial Intelligence, 2020
• Preprint: A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument, KR 2020, 2020

    Some Recommended Papers   (see also DBLP, Scholar, RG, ORBI^lu, ORCID; my Erdös number is 3)
Research Vision, Position Papers
● Reasonable Machines: A Research Manifesto, KI, 2020 [details] ● What is a proof? What should it be?, 2019 [details]
Universal Logical Reasoning, Shallow Semantical Embeddings and Computational Hermeneutics
● Universal (Meta-)Logical Reasoning: Recent Successes, Sci. Comp. Progr., 2019 [details] ● A Computational-Hermeneutic Approach for Conceptual Explicitation, SAPERE, 2019 [details] ● Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis, 2020 [details] ● Cut-Elimination for Quantified Conditional Logic, J. Phil. Log., 2017 [details] ● Quantified Multimodal Logics in Simple Type Theory , Log. Univ., 2013 [details]
Normative Reasoning and Machine Ethics
● Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support, AI Journal, 2020 [details] ● Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic, 2020 [details] ● I/O Logic in HOL, J. Appl. Log., 2019 [details] ● A Dyadic Deontic Logic in HOL, DEON, 2018 [details]
Computational Metaphysics and the Ontological Argument
● A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument, KR, 2020 [details] ● Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument, Bulletin of the Section of Logic, 2020 [details] ● Mechanizing Principia Logico-Metaphysica in Functional Type Theory, Rev. Symb. Log., 2020 [details] ● Computer Science and Metaphysics: A Cross-Fertilization, Open Philosophy, 2019 [details] ● The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics, IJCAI, 2016 [details] ● Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers, ECAI, 2014 [details]
Foundations of Maths, Category Theory
● Automating Free Logic in HOL, with an Experimental Application in Category Theory, J. Autom. Reason., 2020 [details] ● Computer-supported Exploration of a Categorical Axiomatization of Modeloids, RAMiCS, 2020 [details]
Higher-order Logic, Higher-order Automated Theorem Proving
● Church's Type Theory, Stanford Encyclopedia of Philosophy, 2019 [details] ● The Higher-Order Prover Leo-III, IJCAR, 2018 [details] ● The Higher-Order Prover Leo-II, J. Autom. Reason., 2015 [details] ● Automation of Higher-Order Logic, Handbook of the History of Logic, 2014 [details] ● Higher-Order Semantics and Extensionality, J. Symb. Log., 2004 [details]
Maths Proof Assistants, Natural Language Proof Tutoring, Agent-based Reasoning
● OMEGA: Resource-Adaptive Processes in an Automated Reasoning, Cognitive Technologies, 2010 Systems, [details] ● Computer Supported Mathematics with OMEGA, J. Appl. Log., 2006 [details] ● Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs, Cognitive Technologies, 2010 [details] ● Granularity-Adaptive Proof Presentation, AIED, 2009 [details] ● Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs, AAAI, 2005 [details] ● Proof Development in OMEGA: The Irrationality of Square Root of 2, 2003 [details]

    Computational Metaphysics and The Ontological Argument:
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. Here is more information of this line of research.
Our related 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.

    Main Projects (current and past)
CRAP: Consistent Rational Argumentation in Politics
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 (selection):
CLAIRE-AI (national contact point), Conference on Automated Deduction, Association for Automated Reasoning, Society of Deontic Logic and Normative Systems, Berlin Mathematics Research Center MATH+, Berlin Mathematical School, Fachgruppe Deduktionssysteme der GI, IFCoLog, Logic Journal of the IGPL, Journal of Applied Logics

    (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:14min (3000m), 14:13min (5000m), 30:04min (10000m).

C. Benzmüller (Last modified: Sun Jul 5 19:42:15 CEST 2020 )