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.
|
|
News
| •
Conference on Intelligent Computer
Mathematics (CICM 2020), PC co-chair: proceedings, website
|
| •
Course on Ethical and Legal Challenges in AI and Data Science: website, flyer
|
| •
Preprints: Reasonable Machines: A Research
Manifesto, KI'2020, and Encoding Legal Balancing: Automating an
Abstract Ethico-Legal Value Ontology in Preference Logic, MLR'2020
|
| •
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
|
| •
See the recent cover article in French science magazine Science &
Vie on my work in Computational Metaphysics.
|
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]
●
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]
|
Books/Proceedings (selection):
|
Computational Metaphysics and The Ontological Argument:
Main Projects (current and past)
Board Memberships (selection):
(Former) Hobbies
C. Benzmüller (Last modified: Mon Oct 12 10:52:09 CEST 2020 )
| 
