讲座信息
主题
Experiments in Computational Metaphysics Using the Logic-Pluralistic Logikey Methodology
主讲人
Christoph Benzmüller
Chair of Artificial Intelligence Systems Engineering at the University of Bamberg
Freie Universität Berlin
与谈人
Andrew Joseph McCarthy
Assistant Professor, Department of Philosophy, ECNU
主持人
Xudong Hao
Associate Professor, Department of Philosophy, ECNU
讲座时间
2024年11月7日(周四)
15:30-17:00
讲座地点
腾讯会议: 589907422
密码:554332
作者简介
Prof. 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.
Benzmüller has conducted research as a visiting professor/scholar at numerous prestigious universities in Germany and abroad, and has established a close research network. Stations in his career include: BITS Pilani Dubai, Zhejiang University, University of Luxembourg, Stanford University, International University in Germany, Cambridge University, University of Birmingham, University of Edinburgh and Carnegie Mellon University. Benzmüller studied Computer Science and AI at the University of Saarland, Germany, where he also received his Ph.D. and habilitation.
Benzmüller教授是班贝格大学人工智能系统工程系主任,也是柏林自由大学Universität数学和计算机科学系的兼职教授。他的研究兴趣包括计算机中理性和规范推理的自动化、通用知识表示、计算形而上学和数学推理的机械化;高阶交互和自动化定理证明是其特别的研究重点,也是上述研究工作的重要支柱。
内容简介
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.