讲座预告 | Experiments in Computational Metaphysics

教育   2024-10-29 15:19   上海  

讲座信息



主题

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.


华东师范大学哲学系
华东师范大学哲学系
 最新文章