Professor Christoph Benzmüller holds the Chair of Artificial Intelligence Systems Engineering at the University of Bamberg and is an Adjunct Professor at the Department of Mathematics and Computer Science at the Freie Universit?t Berlin. Benzmüller's research interests include the automation of rational and normative reasoning in computers, universal knowledge representation, computational metaphysics, and the mechanization of mathematical reasoning. A particular research focus is higher-order interactive and automated theorem proving as a backbone for the above activities.
In the first part of this talk, I will motivate and present LogiKEy, a logic-pluralistic knowledge representation and reasoning methodology that I have been developing with colleagues over the past decade. LogiKEy distinguishes between different conceptual levels on which knowledge is represented. Most relevant for this talk, LogiKEy uses a sufficiently expressive meta-logic (e.g. classical higher-order logic HOL) at its most basic level and encodes different object logics (e.g. different higher-order modal logics) on top of it. These object logics, which are negotiable in LogiKEy, are then used on higher layers to encode domain-specific languages, which can then be used in applications. The object logic encodings can generally be realized as shallow or deep logic embeddings, although the main focus in LogiKEy so far has been on shallow embeddings, since they support better proof automation and model finding using existing automated reasoning tools for HOL. The shallow embeddings are thereby designed in a compositional way, taking advantage of lambda abstraction and currying in meta-logic HOL. In the second part of the talk I will present some successful recent applications in computational metaphysics, including in particular, the analysis of different variants of Kurt G?del's ontological argument in higher-order modal logic. These experiments demonstrate the flexibility of LogiKEy, especially with respect to modifications of the precise object logic used.
