Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is $Σ^1_1$-hard
本文证明带公共知识的任意公开宣告逻辑APALC在S5模型上的可满足性问题是Σ^1_1难的，由此推出其有效式与可满足公式集均非递归可枚举，且该逻辑不可有穷公理化。
2023-07-11 cs.LO
Doxastic Lukasiewicz Logic with Public Announcement
本文提出Łukasiewicz逻辑的信念扩展$BL^+$，进一步引入带公开宣告的逻辑$DL$，并用于建模模糊版泥孩子谜题，最后证明$DL$的可靠性与完备性。
2023-04-17 cs.LO math.LO
A Logic for Global and Local Announcements
Labortoire IBISC, UEVE（UEVE IBISC实验室）；IRIT Toulouse（图卢兹IRIT研究所）；LORIA – CNRS（洛林计算机及其应用研究实验室（CNRS））；Université de Lorraine（洛林大学）；Department of Computing（计算系）；University of Liverpool（利物浦大学）
在本文中，我们介绍{ \em全球和本地公告逻辑}（GLAL），一个动态的认知逻辑与两个不同的公告运营商- $[ϕ]^+_A$和$[ϕ]^-_A$索引到一个子集$A$的集合$Ag$的所有代理-分别为全球和本地公告。边界情况$[ϕ]^+_{Ag}$对应于$ϕ$的公告，如从文献中已知的。与标准公共公告不同，标准公共公告是{ \em模型Transformers}，全局和局部公告是{ \em指向模型Transformers}。特别地，由通告引起的更新在模型的不同状态中可能不同。因此，所得到的计算是模型树，而不是典型的序列。我们的语义的一个结果是，模态双相似状态可以在我们的逻辑区分。然后，我们提供了一个更强的双相似性的概念，我们表明，它保留了模态等价GLAL。此外，我们表明，GLAL是严格更具表现力的公共公告逻辑与常识。我们证明了广泛的有效性GLAL涉及动态和知识之间的相互作用，并表明GLAL的可满足性问题是可判定的。我们通过详细的认知场景来说明正式的机器。
2017-07-27 cs.AI cs.LO
Announcement as effort on topological spaces
我们提出了一个多智能体逻辑的知识，公共和任意公告，这是解释拓扑空间的子集空间语义的风格。任意公告模态的功能与子集空间逻辑中的努力模态类似，然而，它具有直观和语义差异。我们提供公理化的三个逻辑的基础上，这种设置，并证明其完整性。
2016-06-24 cs.LO
Axiomatisation for an asynchronous epistemic logic with sending and receiving messages
IRIT, CNRS—INPT—UT（IRIT，法国国家科学研究中心-国立高等矿业电信学校联盟-图卢兹大学）；IHPST University Paris 1 Panthéon Sorbonne（巴黎第一先贤祠-索邦大学历史哲学科学研究所）
本文研究了一种异步公告逻辑，其中环境发送信息与个体代理接收信息分离，分别有不同的模态。通过Kripke模型的历史公告和接收记录解释公式，并提出新的公理化AA*扩展原有公理化AA，适用于任意历史记录。
2026-09-16 cs.LO cs.MA
Quantifying over Boolean announcements
本研究提出布尔任意公共公告逻辑（BAPAL），限制公告量词于布尔公式，证明其具有有限公理化且表达力不弱于APAL，可判定性留待后续论文。
2022-01-20 cs.CC cs.LO
A Constructive Epistemic Logic with Public Announcement (Non-Predetermined Possibilities)
我们认为，建构主义（直觉主义）中的认知\emph{possible worlds}的概念是不一样的，它是在经典的观点，并有可能性，所谓的非预定世界，这是被忽视的（经典）认知逻辑。对于非预定的可能性，我们提出了一个构造性的认知逻辑，证明了它的可靠性和完备性定理，并通过增加一个公共宣告算子对所提出的逻辑进行了扩展。为了说明我们工作的重要性，我们通过所提出的建构性认知逻辑，构造了著名的惊奇考试悖论$\mathbf{SEP}$，并提出了解决该悖论的方法。我们澄清，在$\mathbf{SEP}$的困惑是因为学生的（错误）假设，考试的日子一定是预先确定的。
2013-02-05 cs.LO
The Undecidability of Quantified Announcements
本文证明APAL、GAL和CAL三种量化公告逻辑在多智能体情形下不可判定，单智能体情形下可判定，并修正了此前版本中公式cga(X)的定义错误。
2024-06-06 cs.LO
How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions
在标准的认知逻辑中，知道p等于知道p是真的，但它并没有说理解p或知道它的意义。在本文中，我们提出了一个保守的公共公告逻辑（PAL）的扩展，其中代理人有知识或信念的真值和命题的意义。我们给出了一个完整的公理化PAL布尔定义，并讨论了各种例子。一个主体可能理解一个命题而不知道它的真值，或者反过来。此外，多个代理人可以就某件事达成一致，但不同意其含义，反之亦然。
2019-07-22 cs.LO
True Lies
University of Bergen（卑尔根大学）；Zhejiang University（浙江大学）；University of Lorraine（洛林大学）；Peking University（北京大学）
一个真正的谎言是一个谎言，当宣布成为真实。在宣告的逻辑中，宣告的代理人没有被建模，真正的谎言是一个公式（它是假的），当宣告时变成真的。我们调查真实的谎言和其他类型的相互作用之间宣布的公式，他们的先决条件和后置条件，在设置Gerbrandy的逻辑相信公告，其中代理人可能有或获得不正确的信念。我们的结果是满足性和有效性的实例化这些语义定义的类别，迭代公告，包括任意经常迭代公告，和句法表征。我们关闭的结果迭代公告的逻辑知识（而不是信仰），并撒谎作为私人公告（而不是公共公告）不同的代理。详细的例子说明了我们说谎的概念。
2017-04-27 cs.AI cs.LO cs.MA
Asynchronous Announcements
IRIT（图卢兹计算机研究所）；CNRS（法国国家科学研究中心）；University of Toulouse（图卢兹大学）；LORIA（洛林计算机科学及其应用实验室）；University of Lorraine（洛林大学）
我们提出了一个多代理认知逻辑的异步公告，真实的公告是公开发送，但单独接收的代理，并在他们被发送的顺序。除了认知模态外，逻辑还包含了发出和接收公告的动态模态。一个代理人所相信的是她最初的不确定性和她收到的通知的函数。信念不一定是真实的，因为已经发布的公告可能还没有被收到。由于在发送时声明为真，因此可以排除某些消息序列，就像分布式计算中的不一致切割一样。我们提供了一个完整的公理化的\emph{asynchronous announcement logic}（AA）。这是一个归约系统，它还证明了$AA$中的任何公式都等价于没有动态模态的公式，就像公共声明逻辑一样。一个详细的例子建模的消息交换过程中的分布式计算在$AA$关闭我们的调查。
2021-01-18 cs.AI cs.DC cs.LO
Dynamic Hypersequents for Public Announcement Logic
IRIT, CNRS—INP—UT（IRIT，法国国家科学研究中心-国立理工学院）；IHPST, CNRS—Paris 1 Panthéon Sorbonne（IHPST，法国国家科学研究中心-巴黎第一先贤祠-索邦大学）
本文提出动态超序列，用于在公共公告逻辑中建模知识的动态演变，通过扩展S5的超序列演算，实现了对知识模型转换的语法表示，展示了其良好的性质。
2026-06-22 cs.LO
Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
University of Bamberg（班贝格大学）；FU Berlin（柏林自由大学）
提出了相对化公共知识的公告逻辑的一种浅语义嵌入。这种嵌入使这个逻辑的第一次自动化与现成的定理证明经典高阶逻辑。它演示了（i）元理论研究如何可以自动化的方式，以及（ii）如何在目标逻辑（公告逻辑）的非平凡的推理，例如，需要获得一个令人信服的编码和自动化的智者之谜，可以实现。所提出的语义嵌入的关键是，评价域被明确建模，并被视为一个额外的参数，在编码的组成部分的嵌入式目标逻辑;在以前的相关工作，例如正常模态逻辑的嵌入，评价域之间的元逻辑和目标逻辑隐式共享。本文中介绍的工作构成了对多元LogiKEy知识工程方法的重要补充，该方法可以同时进行逻辑及其组合，一般和领域知识以及具体用例的实验。
2022-01-27 cs.AI cs.LO math.LO
Satisfiability of Quantified Boolean Announcements
本文研究布尔任意公共公告逻辑（BAPAL）的可满足性问题，证明其可判定性，并指出该逻辑不具备有限模型性质。
2025-01-30 cs.LO
Anonymous Public Announcements
University of Bergen（卑尔根大学）；Shanxi University（山西大学）；Center for Juris-Informatics（法学信息中心）；Asia University（亚洲大学）
本文在公共公告逻辑框架下形式化匿名公共公告，区分无意图假设与意图匿名公共知识两种情况，证明前者可归约为认知逻辑，后者与安全公告相关，并给出表达性与完备性结果。
2025-04-21 cs.AI cs.CR cs.LO
Topological Subset Space Models for Public Announcements
我们重新定义了Wang和Agotnes（2013）给出的键定义，为子集空间中的公共声明提供语义。更确切地说，我们解释的先决条件，为公共公告的“本地真理”的“本地”的“，语义上呈现通过内部运营商。这与“可知”的概念密切相关。我们认为，这些修订后的语义改善了原来的，并提供了几个激励的例子，这种效果。出现的一个关键见解是拓扑结构在这种情况下的关键作用。最后，我们提供了一个简单的公理化的结果逻辑和证明的完整性。
2016-12-06 cs.LO math.LO
Eventual and Strong Eventual Notions in Public Announcements
Institute of Science Tokyo（东京科学大学）
本文在公开宣告的背景下引入最终与强最终（含超限）版本的成功、自我反驳等概念，并给出它们与其他条件及不动点观点之间的关系。
2026-09-22 cs.LO cs.MA math.LO
Muddy Waters
University of Toulouse, CNRS, IRIT（图卢兹大学，法国国家科学研究中心，IRIT）
本文提出一个新颖的帽子问题，通过公共公告逻辑和固定点扩展，探讨在信息不足的情况下如何通过特定规则使参与者推断出自身颜色。
2025-11-27 cs.LO
The Dynamic Turn in Paraconsistency
Institute of Philosophy and Human Sciences, UNICAMP（坎皮纳斯州立大学哲学与人文科学学院）；University of Toulouse, IRIT-CNRS（图卢兹大学IRIT-CNRS）；Indian Institut of Technology (IIT)（印度理工学院）
该研究提出弗协调逻辑的动态转向，引入AMLFI1及其特殊情况PALFI1，还有带事实变化的UMLFI1，证明了这些逻辑的可靠性和完全性，它们扩展了已知认知弗协调逻辑，可形式化临时矛盾的获取与解决。
2026-07-23 cs.LO cs.MA
Lower Bound for the Communication Complexity of the Russian Cards Problem
在本文中，它表明，没有公告计划，可以在动态认知逻辑（DEL）建模可以解决俄罗斯卡问题（RCP）在一个公告。由于DEL是一个通用模型的任何公告计划，我们得出结论，有没有单一的公告解决方案的RCP。证明演示了DEL在证明通信协议的下界的效用。研究还表明，当对手拥有足够多的卡时，一般版本的RCP没有两个公告解决方案。
2008-12-24 cs.LO
Dynamic Logic of Trust-Based Beliefs
Institute of Logic and Intelligence, Southwest University, China（逻辑与智能研究所，西南大学，中国）；University of Southampton, United Kingdom（南安普顿大学，英国）；Independent Scholar, United States（独立学者，美国）
本文研究融合数据公开宣告的智能体信念动态逻辑，提出可靠完备的公理化系统并给出多项式模型检测算法。
2025-11-02 cs.AI cs.LO math.LO
A simple proof of the completeness of APAL
给出了任意公告逻辑APAL的完备性的一个简单证明.该证明是对出版物Knowable as Known after an Announcement中的证明的改进。
2014-09-10 cs.LO
(Arbitrary) Partial Communication
Agent群体间的通信是近年来动态认知逻辑研究的热点。本文研究了一种最近引入的部分（更准确地说，基于主题的）通信形式。这种类型的通信允许对多智能体协作和协商的场景进行建模，并且特别适合于共享所有信息不可行/不可取的情况。在介绍了模型检验的不变性和复杂性的结果后，本文将部分通信与公告进行了比较，这可能是DEL中最知名的通信类型。它示出的设置是，更新明智的，无与伦比的：有一个公告的效果不能被部分通信复制的情况下，反之亦然。然后，本文将注意力转移到基于策略性话题的交际上。它通过扩展语言的模态，量化的主题代理可以“谈论”。对于这个新的框架，它提供了一个完整的axiomatisation，也表明，新的语言的模型检验问题是PSPACE完全的。本文最后表明，在表现力方面，这种新的语言的任意部分通信是不可比拟的任意公告。
2023-02-23 cs.LO
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
我们提出了一个通用的框架，建模和验证的认识属性参数化的多智能体系统，通过真实的公告进行通信。在我们的框架中，代理的数量或某些资源的数量被参数化（即先验未知），相应的验证问题询问给定的认知属性是否为真，而不管参数的实例化。例如，在一个泥泞的儿童拼图中，人们可以问每个孩子是否最终都会发现他是否泥泞，而不管孩子的数量。我们的框架是定期模型检验（RMC）为基础的，其中同步有限状态自动机（相当于一元二阶逻辑的话）被用来指定系统。我们提出了一个公共声明逻辑的扩展作为规约语言。特别感兴趣的是增加了所谓的迭代公共公告运营商，这是至关重要的推理知识参数化系统。虽然运营商的模型检验问题不可判定的，我们表明，这成为一个适当的“消失关系”时，可判定的。此外，我们展示了如何Angluin的L* 算法学习有限自动机可以应用到找到一个消失的关系，这是保证终止，如果它是正规的。我们已经实现了该算法，并将其应用于这样的例子，如泥泞的儿童拼图，俄罗斯卡问题，大数挑战。
2021-03-08 cs.FL cs.LO cs.MA
Knowing Values and Public Inspection
我们提出了一个基本的动态认识逻辑的“知道的价值”。类似于标准DEL中的公告，我们研究了“公共检查”，一个新的动态算子，它更新了代理关于常数值的知识。我们提供了一个健全的和强完整的公理化的单和多代理的情况下，利用著名的阿姆斯特朗公理的依赖关系在数据库中。
2016-11-23 cs.LO
Dynamic Epistemic Logic Games with Epistemic Temporal Goals
Université de Rennes（雷恩大学）；ENS Rennes（雷恩高等师范学校）
动态认知逻辑（英语：Dynamic Epistemic Logic，DEL）是一个逻辑框架，在这个框架中，人们可以非常详细地描述行为是如何被代理感知的，以及它们如何影响世界。DEL游戏最近被引入作为一种定义具有不完美信息的游戏类别的方法，其中玩家可用的动作被非常精确地描述。这个框架可以很容易地定义，例如，玩家只能使用公共行动或公共公告的游戏类别。这些游戏已被研究的可达性目标，其目的是达到一种情况下，满足一些认知属性表示在认知逻辑，几个（UN）decidability结果已经建立。在这项工作中，我们表明，可达性目标获得的可判定性结果扩展到一个更一般的类获胜的条件，即那些表达在认知时序逻辑LTLK。要做到这一点，我们建立的DEL公共行动所产生的无限博弈结构是经常的，我们描述了如何获得有限的表示，我们依赖于解决这些问题。
2020-01-20 cs.AI cs.LO cs.MA
Reachability Games in Dynamic Epistemic Logic
我们定义的可达性游戏的基础上动态认知逻辑（DEL），玩家的行动被精细描述为DEL行动模型。我们首先考虑设置一个外部控制器与完美的信息与环境的相互作用，并旨在达到一些认识的目标状态关于系统的被动代理。我们研究了控制器的策略存在性问题，它概括了经典的认知规划问题，我们解决了几种类型的行动，如公共公告和公共行动。然后，我们考虑一个更丰富的设置，代理人本身是球员，其策略必须基于他们的观察。我们建立了几个（联合国）的分布式策略的存在问题的可判定性结果，根据玩家可以使用的行动类型，并将它们与文献中的结果与不完美信息的多人游戏。
2019-05-29 cs.LO
Reasoning About Knowledge on Regular Expressions is 2EXPTIME-complete
Chennai Mathematical Institute Chennai, India（钦奈数学研究所（钦奈，印度））；Indian Statistical Institute Chennai, India（印度统计研究所（钦奈，印度））；ENS De Lyon France（里昂高等师范学院（法国））
本文研究了多智能体认知规划中基于公开观察更新知识的逻辑，证明了 Public Observation Logic (POL) 的可满足性问题是 2EXPTIME 完全的。
2025-08-13 cs.AI cs.CC cs.LO
On simple expectations and observations of intelligent agents: A complexity study
Indian Statistical Institute（印度统计研究所）；Unive Rennes（雷恩大学）；IRISA（法国国家信息与自动化研究所雷恩分院）
本文研究公开观察逻辑 POL 各片段可满足性问题的计算复杂性，并揭示其与公开宣告逻辑之间的内在联系。
2023-06-05 cs.AI cs.CC cs.LO
Group Knowledge of Hypothetical Values
University of Amsterdam（阿姆斯特丹大学）
本文研究了半公开数据交换事件中群体知识的动态逻辑，引入了分布式知识和条件知识的操作符，并给出了完整的公理化和可判定性证明。
2025-11-27 cs.LO
Dynamic Epistemic Logic of Resource Bounded Information Mining Agents
本文提出资源受限智能体半公开查询的动态认知逻辑，刻画付费私密答案、预算约束与群体共享资源查询，并证明其完备性、可判定性及高效模型检测。
2024-01-24 cs.LO
A logical reconstruction of SPKI
SPKI/SDSI是一个建议的公钥基础设施标准，它包含了SDSI公钥基础设施。SDSI的主要创新是使用当地名称。我们之前介绍了本地名称包含逻辑，它具有清晰的语义，并被证明可以完全表征SDSI名称解析。在这里，我们将展示如何扩展我们以前的方法来处理SPKI的一些关键功能，包括撤销，到期日期和元组减少。我们表明，这些扩展添加相对较小的复杂性的逻辑。特别是，我们不需要非单调逻辑来捕获撤销。然后，我们使用我们的语义检查SPKI的元组减少规则。我们的分析突出的地方SPKI的元组减少的非正式描述是有点模糊，并表明，额外的减少规则是必要的，以捕捉有关绑定和授权的一般信息。
2002-08-19 cs.CR cs.LO
First-Order Modular Logic Programs and their Conservative Extensions
模块化逻辑程序提供了一种将逻辑程序视为由许多独立的、有意义的模块组成的方法。本文介绍了一阶模逻辑程序，它可以捕获许多答案集程序的含义。我们还介绍了保守的扩展，这样的程序。这个概念有助于识别模块化程序之间以及传统程序之间的强关系。我们展示了如何保守扩展的概念可以用来证明常见的投影重写。这篇笔记正在考虑发表在《逻辑程序设计的理论与实践》上。
2017-02-17 cs.LO
