Christoph Benzmüller, Prof. Dr. habil.

Freie Universität Berlin, Dep. of Maths and CS
Scientific Advisor Startup Industry

Arnimallee 7, 14195 Berlin    Tel.: +49(0)30 838 52485

Bio CV Publications Presentations Teaching

    Professional Interests
My research activities are interfacing the areas of artificial intelligence, philosophy, mathematics, computer science, and natural language. Current research focuses on the use of formal argumentation & explanation to achieve trustworthy AI systems, that is reasonable machines. 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, 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.

Keynote at the Inauguaration Ceremony of ZLAIRE, the Zhejiang U--U Luxembourg Joint Lab on Advanced Intelligent Systems and REasoning, 2021
● Winner of the Wissensstadt Berlin 2021 Science Slam of FU Berlin with my contribution on Trustworthy AI
● Event: First German National CLAIRE Meeting on Trusted AI
● New book: Logic and Argumentation, Springer Lecture Notes in AI
● New book: Wider den Reduktionismus, Springer Spektrum
● Research Manifesto: Reasonable Machines and Träumen vernünftige Maschinen von Gründen? Eine reale Utopie
● PCs: CLAR (co-chair), ESSLLI (area co-chair, 2022), CADE, DEON, FroCoS, ITP, KI, LNGAI, ARCADE, PhDsInLogic
● New paper: Value-oriented Legal Argumentation in Isabelle/HOL, ITP 2021
● New article: Extensional Higher-Order Paramodulation in Leo-III, J. Autom. Reason. (preprint)
Encoding Legal Balancing, extended version of MLR'2020 contribution; cf. also this related preprint
● 4th International Conference on Logic and Argumentation (CLAR 2021), PC co-chair, website
● Course on Ethical and Legal Challenges in AI and Data Science: website, flyer
● Conference on Intelligent Computer Mathematics (CICM 2020), PC co-chair: proceedings, website
● New article: Designing Normative Theories for Ethical and Legal Reasoning, Artif. Intell., 2020
Cover article in Science & Vie on my work in Computational Metaphysics

    Books/Proceedings (selection):

    Some Recommended Papers   (see also DBLP, Scholar, RG, ORBI^lu, ORCID; Erdös number: 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] ● Value-oriented Legal Argumentation in Isabelle/HOL, 2021 [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.

    Projects (current and past, selection)
PetraKIP: Persönliches transparentes KI-basiertes Portfolio für die Lehrerbildung (BMBF)
DELIGHT: Deontic Logic for Epistemic Rights (FNR, Luxembourg)
7Markets: AI-supported Financial Brokering (BMBF Exist)
CRAP: Consistent Rational Argumentation in Politics (VolkswagenStiftung)
LEO-III: Higher-Order Theorem Prover (DFG)
CompMeta: Studies in Computational Metaphysics (DFG)
ONTOLEO: Higher-Order Ontology-Reasoning with LEO-II (DFG)
LEO-II: Higher-Order Theorem Prover (EPSRC, UK)
THFTPTP: An Infrastructure for Higher-order Automated Theorem Proving (ERC)
OMEGA: Agent-oriented Proof Planning (DFG)
DIALOG: NL-based Interaction with a Mathematics Assistance System (DFG)
CALCULEMUS: Integration of Symbolic Reasoning and Symbolic Computation (ERC)

    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: Tue Dec 7 09:47:54 CET 2021 )