Tableaux for Reasoning in Non-Classical First-Order Epistemic Logics
时间：2026年7月30日（星期四）10:00
地点：人工智能学院 A328 室
Jens Classen,副教授
罗斯基勒大学 人与技术系
摘 要
A family of non-classical logics for knowledge representation and reasoning makes use of so-called standard names, which are syntactically treated like constants, but which are also assumed to comprise the fixed universe of discourse, under a substitutional interpretation of quantification. Originally introduced and studied by Levesque and Lakemeyer in the context of epistemic modal logic, this approach not only admits interesting theoretical properties, but is also useful for devising dedicated reasoning procedures, where standard names provide a well-defined notion of the identity of individuals, similar to identifiers in database management. Somewhat surprisingly, to the best of our knowledge, no implementation of a sound and complete reasoner for the logics in question exist. Moreover, the only sound and complete proof systems are Hilbert-style axiom systems, which are not suitable for actual reasoning. In this talk, I present recent joint work with Torben Braüner that addresses to fill this gap by means of the method of analytic tableaux. After a gentle introduction to tableau systems for propositional logic, the talk proceeds to present systems for increasingly expressive formalisms that include (substitutional) first-order quantification and epistemic modalities. It concludes with a discussion of an implementation as well as philosophical considerations.
报告人简介
Dr. Jens Classen is Associate Professor at the Department of People and Technology at Roskilde University in Denmark. His research interests are in knowledge representation and logic-based AI, with a focus on reasoning about actions and change, reasoning about beliefs, planning, agent program verification, reactive synthesis, and machine ethics.欢迎参加
基本文件流程错误SQL调试
请求信息 : 2026-08-11 12:41:14 HTTP/1.1 GET : https://www.yeyulingfeng.com/a/881729.html
夜雨聆风
