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: see the news
page of my AISE group at U Bamberg
Computational Metaphysics and The Ontological Argument:
Projects (current and past, selection)
PetraKIP:
|
Persönliches transparentes KI-basiertes Portfolio für
die Lehrerbildung (BMBF)
|
NFDIxCS:
| National Research Data Infrastructure for and with Computer Science (DFG)
|
DFG AL2681:
|
Fairness und Effizienz in Fahrzeug-Routing-Problemen (DFG,
host of Dr. Aleksandrov)
|
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)
|
|
(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:
52,8s (400m),
1:53min (800m), 2:25min (1000m), 3:49min (1500m), 8:16min (3000m), ,
8:13min (3000m indoor), 9:11min (3000m Hi), 14:13min
(5000m),
30:52min (10000m),
30:04min (10km road run).
|
C. Benzmüller (Last modified: Mon Dec 23 13:16:58 +04 2024 )
|