讲座信息 - 逻辑与形而上学系列讲座第六讲

主题：命题赋值动态逻辑

（Dynamic Logic of Propositional Assignments）

主讲人：Andreas Herzig

          法国国家科学研究中心（CNRS）研究员、法国保罗·萨巴捷大学图卢兹计算机科学研究所（IRIT）教授、欧洲人工智能学会会士)

主持人：马明辉

           六合彩资料 教授

时间：2026年4月10日星期五10:00

地点：六合彩资料 锡昌堂727

主讲人简介

Andreas Herzig is a researcher of the French National Research Center(CNRS) at the Toulouse Computer Science Research Institute (IRIT) of Université Paul Sabatier. He is a fellow of the Eur. Association for AI (EurAI). He is the Editor-in-Chief of the Journal Applied Non-Classical Logics (since 2015) and a member of the editorial Board of the J. of Philosophical Logic (since 2008). He was an associated editor of Artificial Intelligence (2017-2022). He was the head of IRIT’s AI Department (2009-2020) and of the Committee on AI and Data Science of the French National Research Agency (ANR, 2022-2025).

Andreas Herzig 是法国国家科学研究中心（CNRS）研究员，任职于法国保罗·萨巴捷大学（Université Paul Sabatier）图卢兹计算机科学研究所（IRIT）。他是欧洲人工智能协会（EurAI）会士。自2015年起担任《应用非经典逻辑》（Applied Non-Classical Logics）主编，自2008年起担任《哲学逻辑杂志》（Journal of Philosophical Logic）编委会成员。2017年至2022年期间，他曾任《人工智能》（Artificial Intelligence）副主编。2009年至2020年期间，他曾任IRIT人工智能部主任；2022年至2025年期间，任法国国家科研署（ANR）人工智能与数据科学委员会主任。

讲座简介

Dynamic Logic of Propositional Assignments (DL-PA) is a variant of PDL whose atomic programs are assignments of propositional variables. In DL-PA, quantification over a propositional variable p can be expressed straightforwardly as nondeterministic choice between assigning p to true and assigning p to false. The other way round, it is less obvious to find a polynomial translation from DL-PA to QBF. We start by eliminating the Kleene star; then put formulas into a normal form where all modal operators correspond to boolean quantifiers; and finally prenex quantifiers in a polynomial way.

命题赋值动态逻辑（Dynamic Logic of Propositional Assignments, DL-PA）是命题动态逻辑（PDL）的一个变体，其原子程序由对命题变项的赋值构成。在DL-PA中，对命题变项p的量化可以直接表述为如下的非确定性选择：要么将p赋值为真，要么将p赋值为假。

反过来，要从DL-PA到 QBF（量化布尔公式）构造一个多项式翻译，则并不那么显然。本文首先消去 Kleene 星算子；接着将公式化为一种规范形式，在该形式下所有模态算子都对应于布尔量词；最后再以多项式方式将量词前束化（prenex）。