条件Doxastic模型：信念修正与信念更新的动态逻辑方法

理论计算机科学电子笔记165（2006）5-21www.elsevier.com/locate/entcs条件Doxastic模型：一种动态信念修正的定性方法亚历山德鲁·巴尔塔格1英国牛津大学计算机实验室。Sonja Smets索尼娅·斯梅茨2，3智利自由大学逻辑与科学哲学中心比利时布鲁塞尔摘要在本文中，我们提出了一个语义的方法来多智能体的信念修正和信念更新。 为此，我们引入了一种关系结构，称为条件性模型（CDM's，简称）。我们表明，这种设置是等同于经典的AGM信念修正理论的认识论版本。 我们提出条件信念的逻辑是完全w.r.t. CDM的。然后移动到信念更新（有时所谓的我们展示了如何对这些类型的更新的标准我们提供了一个完整的公理化相应的动态doxastic逻辑。作为一个应用程序，我们解决了一个关键词：信念修正，信念更新，条件信念，动态认知逻辑，公告，模态逻辑，多智能体系统1介绍从前，有三个非常聪明的孩子，在花园里的大树下玩耍。尽管他们的父亲的警告，顽皮的亚当和夏娃得到了他们的额头泥，但听话的玛丽保持清洁。然后父亲来到他们面前说：1 电子邮件地址：baltag@comlab.ox.ac.uk2名博士后研究员，由佛兰芒科学研究基金资助3 电子邮件地址：sonsmets@vub.ac.be1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.0346A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5故事可能很容易走寻常路，父亲反复问他们是否（知道，或者合理地相信，他们）是肮脏的，直到孩子们通过纯粹的逻辑得出正确的答案但...美丽的夏娃是个不耐烦的女孩：在回答任何问题之前，她迅速地瞥了一眼她的袖珍镜子，甚至没有人怀疑这一点。于是她马上回答说：肮脏的女孩夏娃，的确！但是，如果这位富有同情心的父亲重复这个问题，另外两个人会怎么回答呢？亚当事实上，夏娃在镜子里偷看可以被认为是一个完全私人的声明（“夏娃是肮脏的”），只有她自己作为接收者。使用正确的逻辑，人们可以证明亚当会得出错误的（但逻辑上合理的）结论，他是干净的。这与我们的直觉一致：亚当不会怀疑任何欺骗，他会推理说，只有当夏娃是唯一一个泥泞的人时，她才能知道自己是泥泞的。此外，亚当永远无法收回他的错误答案：正当逻辑根本不允许他改变主意。可怜的淘气的亚当：肮脏的男孩注定永远是错误的;但这肯定是他应得的！可悲的是，正义逻辑预言了一个更不幸的结局：在听到夏娃的回答后，无辜的她会同时相信她事实上，根据私人和公共公告的正当语义学，她认为可能的“可能世界”集合（在夏娃的回答之后）是空的此外，玛丽注定要永远疯狂：没有未来的沟通可以治愈她的矛盾。这与我们的直觉完全相反：一个聪明的玛丽应该得出结论，夏娃以某种方式作弊，通过其他过程而不是纯粹的推理获得所需的信息因此，当父亲第二次重复这个问题时，马利亚应该回答正确的答案，而不是不一致的咕哝：多么完美的玛丽的幸福结局！本文的目的有两个：第一，开发一个基于克里普克模型的，定性的，多主体版本的经典信念修正理论，我们称之为条件4信念的逻辑;第二，我们用它来提出一个修改的语义学私人和公共公告，并公理化相应的动态doxastic逻辑，可以称之为通过将经典的信念修正理论的主要思想融入我们的基本语义结构中，仁慈的逻辑将拯救玛丽免于疯狂，将引导她走向真理，甚至可以给亚当另一个救赎自己的机会，如果父亲再次问这个问题的话。4 或A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）57第一个目标是通过用被称为“条件doxastic模型”（CDM's）的语义结构取代通常的doxastic/epistemic Kripke模型来实现的。值得注意的是，我们的方法与最近关于（动态或静态）信念修正主题的语义学文献（例如[3，10，16，22，23]）在以下意义上不同。大多数Kripke风格的多智能体信念修正模型都是基于特定的机制，这些机制依赖于定量概念，如5然而，经典（AGM）信念修正理论是一种定性理论，基于关于基本操作（修正）的简单假设，具有很大的普遍性和简单性。我们的方法保留了经典的AGM理论的定性描述。这是真的，我们也给出了一个表示定理，表明任何CDM可以表示为产生于（多代理）认知可扩展性模型（基于一个家庭的“良好的预序”）。[6]这样的模型更接近于在信念修正的标准文献中遇到的模型，是Gardenfors（全前序作为可扩展性关系）和Spohn [24]（序值可扩展性函数）首先追求的主题的简单变体。然而，CDM与可扩展性模型之间的对应关系这意味着，如果我们把条件公理结构作为基础，我们可以很容易地看到，通过比较，所有其他上述描述都有些多余：它们包括不相关的特征，例如特定的序数赋值，或者在认识上可区分的状态之间的可比较性由于这个和其他原因，我们强烈倾向于用条件doxastic映射来进行定性描述，这可以被看作是doxastic Kripke模型的标准定义的自然扩展，并且以自然的方式产生了条件信念算子，从而产生了条件doxastic逻辑CDL。 事实上，我们的CDM的语义结构从这个意义上说，我们的方法接近于Johan van Bentham最近（未发表）的论文[ 27 ]中的方法，我们只是在撰写本文的后期才意识到这一点虽然基于涉及可解释性程度的（因此，[ 27 ]中的主要“归约公理”，它在公开宣布初始信念之后计算（以[6，5]中的[5]人们可能会争辩说，信念的程度可以由一个可验证的顺序关系给出，因此可以由一个定性的、顺序理论的概念给出，但事实上，信念修正或更新的定义方式基本上使用了[24]和[3];因此，定量的。[6]这个结果可以被看作是[ 12 ]中Gardenfors表示定理的语义背景中的类似物[7]模型之间的等价性概念对定义的选择很敏感。 我们认为，8A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5与我们相应的公理相同从某种意义上说，我们的方法只是更进一步，并且在语义方面也抽象（从信念修正算子的特定量化实现的具体细节）。这导致了语法（基于条件be- liefs）和语义（根据条件doxastic模型）之间的完美匹配，使我们的逻辑具有更广泛，更一般的应用范围和更大的透明度。反过来，这又极大地促进了向更一般的语境的转移：人们可以用这种方式很容易地为私人宣告产生还原公理的适当类似物，事实上（在未发表的工作中[8]）我们获得了对任意认识/doxastic行动情况的自然推广。我们的概念的条件信念和CDM也可以看到，在CON- 关于条件概念的广泛的逻辑哲学文献的文本，参见例如[1，25，19，18，9]。当然，我们可以把我们的条件信念算子看作是非经典的（和非单调的！）影响事实上，已经有各种尝试和讨论关于使用条件来处理信念修正（参见例如[11，15，20]）。我们将表明，我们的运营商避免已知的悖论所产生的这种混合物的条件和信念修订，未能满足所谓的拉姆齐测试（除了在绝对的，无条件的情况下）。事实上，正如在[27]中所讨论的，拉姆齐检验的通常陈述是基于对具有前提φ的条件的知识（或者更确切地说，在具有φ的“静态”信念修正之间，如我们的假设信念所捕获的）和在学习φ之后所持有的知识/信念（即“动态”信念修正）之间的混淆 [21]中的方法似乎也与我们的方法密切相关：在那里考虑的信念修正和信念更新的他们考虑一些自然的语义条件，与模态公理相对应，但他们不像我们一样关注同一套假设8本文的计划如下。在下一节中，我们简要回顾了知识-信念（KB）模型和判断-认识逻辑的一些基本概念。在第3节中，我们然后，我们转换（修订）信念修订假设到语义条款的KB模型，获得（修订）AGM理论的语义对应。在第4节中，我们定义了我们的中心语义概念，条件doxastic模型（CDM），我们证明了这个设置实际上是等价的（模通常的KB条件）与上述“语义AGM”假设。我们还证明了这等价于一个“良好预序”的相容性关系的定义。在第5节中，我们通过改变公开宣布，使他们以自然的方式对清洁发展机制采取行动在学习新信息时，要“动态修正”信念。在第6节中，我们将此设置扩展到子组的私有公告，我们给出了一个完整的公理化（使用8 在[21]中考虑的更新的概念也完全不同于我们相应的概念。A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）59我们将该逻辑应用于在上述泥孩子类型的场景中从作弊者手中“拯救玛丽”的任务2知识库：KB模型与信念知识逻辑知识-信念框架（Knowledge-BeliefFrame，简称KB框架，参见[17]，第89页）是一个Kripke框架，形式为（S，→a，a）a∈A，具有一组给定的状态S和每个代理的两个二元关系;第一个关系a旨在捕获以下知识：代理A，而第二个→A捕获他的信念。KB帧需要满足以下自然条件：（1）每个k_a 是 自 反 的 ： s_A_s; （ 2 ） 如 果 s_t ， 则 我 们 有 ： s→a_w_i_t→a_w ， 并 且s_a_w_i_t_t_a_w;（3）如果s_t →a_t，则s_t_a_t;(4)对于每个s∈S，存在某个t∈S使得s→at。第一个子句表示知识的真实性，第二个子句表示完全内省（一个主体知道他相信/知道什么，不知道什么），第三个子句说主体相信他们所知道的一切，最后一个子句（序列性）说信念是一致的。知识-信念模型（Knowledge-BeliefModel，KB-模型）是一种具有底层KB-框架的Kripke模型。通过将可达性关系替换为它们的映象映射9，我们得到了一个更“共代数”的框架的等价定义满足以下条件：（一）（3）构造一个新的函数：sas（a）（二）如果t∈s（a），则s（a）=ta，s（a）=t（a）;（4）sa/=t a.映射·a和·（a）称为外观映射：sa是doxastic外观s到a（或a关于s的理论），而s（a）是s到a（或a关于s的知识）的认识论外观。知识-信念模型的两种定义之间的等价性很容易验证。给定一个知识-信念模型S，一个S-命题（或S-理论）就是S中的任何状态集合P<$S。这当然是一个纯粹的命题/理论的外延和语义概念，与“句子”和“理论”的句法和内涵概念不同对于任何S-命题P和主体a∈ A，我们可以像通常一样定义S-命题Ba P（a知道P在外观映射方面，这些定义可以以伽罗瓦对偶的形式给出（外观和知识/信念之间）：s∈Ba Pi <$sa<$P s∈Ka Pi <$s（a）<$P我们可以在S-命题上定义运算：否定<$P：=S\P，合取9 R∈S×S上的一个映象是Rb：S→P（S），Rb（s）：={t∈S：sRt}.10在eay上，通过代入g·a=→da和d·（a）=ca（其中Rb是R的图像-map），并通过代入：s→atit∈sa和satit∈s（a），运算p i t e a y.10A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5PQ：=PQ，一般真信念EbP：=a∈ABa P（“每个人都相信P”）和一般知识EkP：=a∈AK a P. 最后，我们定义共同的真实信念CbP：=n≥0（Eb）nP=P<$EbP <$Eb（EbP）<$···和常识CkP：=n≥0（Ek）nP=P<$EkP<$Ek（EkP）<$· ··.信念-知识逻辑（Belief-Knowledge Logic，BKL）是一种逻辑，其语法由下式给出：ϕ：= p|¬ϕ|ϕ∧ϕ|B a|K a|Cb|Ck语义由明显的组合子句给出：p由赋值给出，S：= S等。作为标准，我们还使用符号s| = Sfors∈S注意，一般信念和一般知识在BKL中是可以定义的。，通过把：Eb：=a∈AB a，Ek：=a∈AK a.以各种名义，BKL是一个著名的逻辑及其完备的证明系统，我们也用BKL是由熟悉的公理和规则给出的，参见例如[17]（第94页，其中这个证明系统被称为KL）。3语义的、多智能体的、认知的AGM理论经典AGM理论经 典 的信念修正采取了- ories的句法观点：我们被赋予一个所有“理论”的家族T，其成员被假设为演绎封闭的句子集（在某些给定的语言上）。设为不一致理论（包含所有句子）。 一个理论T∈T的扩展T+定义为T+：={：T<${}}。现在可以通过标准AGM假设引入信念修正算子：（*1）T是一个理论;（*5） T=i;（*2） ∈ T（*3-4）如果T=T，则T=T;（*7-8）如果<$T/∈T<$T，则T（T）=（T）+修正修正理论：认知型AGM。为了将信念重新审视应用于doxastic-epistemic语言中的理论，我们需要以一种明显的方式修改“成功”假设（*5），因为代理人对自己信念的信念或知识是确定的，因此它们不应该被修改。更一般地说，如果某事物是这导致我们（*5e）T =（即i）∈ T）。这个由假设（*1）、（*2）、（*3-4）、（*5e）、（*6）、（*7- 8）组成的修正系统被称为认知AGM。如果像通常那样，我们假设知识满足必然性规则（从“必然性”推断“必然性”），那么从这个和（*5e），我们得到一个结果是（*5）的期望的一半：如果是，则T=。多代理AGM。为了将这些假设应用于以逻辑BKL编写的理论，我们需要一个多智能体版本的认知AGM。所以我们需要对所有的主体a使用标记算子Ka来重述。但除此之外，请注意，A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）511“理论”的概念 一组句子很可能是智能体a的可能理论，但不是智能体B. AGM中的“理论”应该是对（代理人）关于世界的信念的完整描述。因此，例如，一个对Kb p是否成立（对于某个给定的事实p）没有定论的理论永远不可能是描述主体b的信念的（完全）理论所以我们需要假设，对于每个主体a，有一个“a -理论”族Ta我们假设这些是逻辑BKL中的句子的演绎闭集;如上所述，我们还需要一个最小的内省概念：一个a-理论应该解决所有关于一个人的信仰和知识的问题此外，我们还需要一个不相容的理论来代替a-theory，而且为了弥补这个缺点，我们需要要求这个不相容的理论是一个a-theory。因此，我们制定了我们的修改后的多智能体（认知）AGM假设，通过给出，对于每个智能体a∈ A：一个家庭TaP（BKL）的句子集在语言BKL，calledda-the或iess，和一个belie的revisionopera到ra：Ta×BKL→Ta，把一对a-理论和BKL-句子变成新的a-理论;并要求他们满足以下条件：（T1）T ∈ Ta（其中T：= BKL是不相容理论，包含BKL中的所有句子）;（T2）每个T∈Ta是演绎闭的，w.r.t.（T3）对于每个K∈BKL和每个T∈Ta，我们有K a∈T或（<$K a ∈）∈T;（T4）所有上述认知AGM的命题，其中我们用主体名来标记知识Ka和知识库。因此，不需要为信念查询对应于（T3）的内省条件，因为这是从以上条件，给出BKL的公理。事实上，我们可以很容易地证明，对于每一个BKL和每一个T∈ Ta，我们要么有Ba <$∈T，要么有（<$Ba <$）∈T。语义信念修正。为 了 开发多智能体（认知）AGM的语义对应物，我们假设给定KB模型S。我们需要用S -理论的语义概念（即S中的状态集）替换上述假设中作为句子集的“理论”的句法概念S-命题（也称为状态集）。观察到每个S-理论T<$S产生一个句法理论th（T）={φ ∈ BKL：t |= Sφ对于所有的t ∈ T}。除了上述假设之外，我们还必须使我们的信念修正理论与我们的信念理论（由模型S给出）：也就是说，我们必须添加一个假设（T0），要求对于每个代理a，代理最后，我们需要替换运算T+φ和a的理论与语义对应物。要做到这一点，首先观察到理论的偏序对于语义理论是颠倒的：对于S-理论T，TJ<$S，我们有T<$TJith（TJ）<$th（T）。不相容理论现在用空态集来表示。两个句法理论的联合的演绎闭包对应于相应的语义理论（状态集）的交集因此，一个语义理论TS与一个语义命题PS的扩展T+P可以简单地由交集TP给出。因此，我们得到以下定义：12A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5一一一一认知AGM假设的语义版本。给定一个KB模型S，S的AGM信念修正理论定义如 下 ： 对 于 每 个 代 理 a ， 给 出 S-theheriesTaP （ S ） 的 族 ， 称 为 a-thehe或iesoverrS，和一个非操作性函数A：Ta× P（S）→Ta，使得对于所有T∈ Ta，PS，我们有：（T0）sa∈Ta，对所有s∈S;（T1）τ ∈Ta;（T2）若T∈Ta，则对所有s，t∈T有sa=ta和s（a）=t（a）.（*1）TaP∈Ta;（*2）TaPP;（*3-4）TaS=T;（*5e）TaP=iTKa<$P（iT（a）P=）;（*6）如果P=Q，则T_aP=T_aQ;（*7-8）如果TaPQ/=Ta（PQ）=TaPQ，其中我们使用符号T（a）：={t（a）：t∈T}来表示“在T中的a的注意到，事实上，AGM假设（*6）的上述语义版本是超复杂的：由于S-理论的外延性，它总是平凡地被满足4条件Doxastic模型我们现在给出一个设置，相当于语义（多智能体认知）AGM，虽然它是更简单的制定。也就是说，我们丰富我们的知识-信念模型来捕捉条件信念的概念。一个条件doxastic框架（简称CD-框架）（S，{·P}a∈A，P<$S）由一组状态S和一族条件（doxastic）外观映射组成，每个代理a和每个可能条件P<$S对应一个条件外观映射.这些要求满足以下条件：(i)如果s∈P，则sP/=π;（ ii） 如果P≤sQ/=N，则sP ≤;aaa（三） 如果t∈sP，则sQ=tQ;（ iv） sPP;aa aa（v）sP<$Q=sP<$Q，ifsP<$Q<$。aa a一个有条件的doxastic模型（CDM，简称）是一个Kripke模型，它的非线性，主要框架是一个CD框架。 有条件的出现SP捕捉到了状态s出现在代理a面前，给出一些额外的（似乎合理的，但不一定真实的）信息P。更准确地说：无论何时s是世界的当前状态，那么在接收到新的信息P之后，主体a将开始相信，任何状态sJ∈sP可能是世界的现状（因为它是在接收信息P之前）。使用条件doxastic外观，代理人a拥有的关于状态s的知识s（a）（即s的认识外观）可以定义为联合所有有条件的doxastic外观。换句话说，有些东西是已知的，在任何条件下都成立：s（a）：=QSSQ。 使用这个，我们可以看到，第一个条件以上的定义条件doxastic框架捕捉A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）513一一→a一一a∈A一知识的真实性。第二个条件是信念修正的成功时：如果不知道某件事是假的，那么它可以作为一个假设被一致地接受。第三个条件表达了对（条件）信念的完全内省：代理人知道他们自己的条件信念，所以他们不能修改他们对这些信念的信念第四个条件是假设被假设地相信：当做出一个假设时，这个假设被认为是真的。最后一个条件描述了修正的最小性：当面对新的信息Q时，智能体尽可能多地保留他们以前的（条件）信念s P。这些要求可以被看作是对定义KB帧的条款的加强：事实上，每个CD帧都是KB帧。要看到这一点，定义sa：=sS就足够了，并检查这是否满足所有KB假设。换句话说：我们可以将无条件（“默认”）信念恢复或者，我们可以将条件doxastic框架关系地定义为元组（S，{→Pa}a∈A ，P∈S），其中re→Pareb在一个关系中，满足以下类：（1. ）如果s∈P，则存在满足s→Pa的所有元素Qt;（2.）如果s→at∈P，则有存在satew∈Ssuc hth ats→Paw;（3. ）如果s→Patthenforverystatew∈S，Q有：s→aQwit→aw;（4. ）ifs→Pa ttent∈P;（5. ）如果rexists→Pat∈Q对于所有w∈S，我们有：sP<$Q，其中s→Pw∈Q。很容易看出条件doxastic框架的这个定义相当于上面的一个11。将模态的标准Kripke关系定义应用于条件，tionaldoxast icratios→Pat，我们可能会在一个新的工作地点BP关于S-命题，表达条件信念;在外观地图方面，定义说，条件信念是条件出现：BP Q：={s∈S：sP<$Q}a a我们把这理解为，A相信Q是P的条件。更确切地说，这是说：如果智能体学习P，那么（学习后）他会相信Q是当前状态（学习前）的情况。注意，以平凡真命题S为条件的信念与通常的无条件信念一致：BSQ = BaQ。作为上述假设的结果，知识算子，定义为（如前一节所述）认知外观Ka P：={s∈S：s（a）<$P}的伽罗瓦对偶，具有以下性质：Ka P=BQ P=B<$P=B<$Pa a aQS我们还可以定义一般信念、共同真信念、知识的条件版本边缘，一般知识，共同知识，通过：EbP Q：=BP Q，D[11]在某种程度上，它们是等价的，a=→（其中R是R的图像映射），反之PP方法是：s→atit∈sa。一14A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5一一一一一一一一一一一Cb PQ：=（Eb P）nQ = Q <$Eb P Q<$Eb P（Eb P）Q<$. ，KP Q：=K（P→Q），n≥0EkQ：=KP Q，CkP Q：=aa（EkP）nQa∈Aan≥0定理4.1 CDM等价于KB模型上的语义AGM理论。我的律师。GivenAGMthoryoveraKB-模型，定义P：=saP，nd检查这是否符合CDM的条款。 相反，从CDM开始，并将Ta：={sP：s∈S，P<$S}. DefineearevisionoperatorTaQforour理论T=sP∈ Ta，由情况：如果我们有Ps（a）=（即，如果sP=），then我们输入PaQ：=;如果我们有Ps（a），但PQs（a） =，则输入s P<$Q：= s Q;否则，写s P<$Q：= s P<$Q= s P<$Q = s Q<$P。很容易检查aa a aaaa aaKB的条件。QCDM的例子aKB-modelinto aCDM，通过输入：sP=saP，其中v=aP/=p，并且s P= s（a）P否则。当然，这只是将KB模型组织为CDM是一种非常特殊的情况，对应于最琐碎的信念修正策略，编码在原则中：一个更一般的例子是：似然性模型：一个认知似然性框架是一个结构（S，a，≤a）a∈A，由一个集合S组成，S被赋予一个等价关系族a和一个“良好前序”族这里，一个一个认知可解释性框架与一个评价一起给出了一个认知可解释性模型。在[12，22]等文献中，仅针对一个智能体且没有认知关系的似然性框架已被用作AGM信念修正的模型一个更具体的例子W. Spohn在[24]中，根据序数偏好映射，将序数d（s）（在我们的认知多智能体背景下，这将给我们一个多智能体知识框架（S，α）a∈A，以及一个有序可扩展性映射组成的结构da：S→Ord（其中Ord是所有序数的族）。任何认知可解释性模型都会以规范的方式产生CDM，sP：=M in≤ {t∈P：tas}其中M in≤T ={t∈T：t≤atJfor alltJ∈T}是T中的极小元集。我们称之为与给定的可扩展性模型相关联的规范CDM。其逆命题如下：定理4.2（表示定理）每个CDM都是正则CDM一些认知的可解释性模型。证据给定一个CDMS =（S，{·P}a∈A，P<$S），对每个a取所有认知表象的族{s（a）：s ∈ S}的某个任意良序≤ a. 定义为is（a）=t（a）。定义s≤atby：或者s（a）≤at（a），或者s（a）= t（a），s∈t{s，t}。是一A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）515一一一容易检查，这是一个认知可解释性模型，其规范CDM是S本身。Q因此，我们在CDM 可扩展性模型的术语。然而，上述定理的证明表明对应关系不是一对一的：同一个CDM规范地对应于许多可扩展性模型。反过来，相同的可扩展性模型对应于许多Spohn型模型（在可扩展性程度方面）。在本文中，我们采取的条件doxastic结构的基本，因为我们感兴趣的是一个逻辑的条件信念。这意味着，对于我们的目的，不仅有序度的可扩展性的实际分配da，但甚至可扩展性关系≤a的大部分导出结构都是无关紧要的：它们包含超连续特征。重要的是相应的条件doxastic地图。条件Doxastic逻辑（CDL）我们现在将BKL更改为信念运算符被条件化的版本。CDL的语法由下式给出：：= p|¬ϕ|ϕ∧ϕ|B |Cb|去你 的 ，而其语义则由CDMS中解释映射P·S：CDL→ P（S）的明显组合子句给出。 在这种逻辑中，知识形态可以定义为一个缩写，将K φ：=Bp是一个a a不一致的句子），或等价地K φ：=B<$φφ。13.不难看出，a a在语义上与语义知识算子的先前定义(as认知表象的伽罗瓦对偶）：<$Ka φ<$S=Ka<$φ<$S。 我们也定义K θ：=K（θ→ε），Eb θ：=Bθ，Ek θ：=K θ。aaa∈Aaa∈Aa定理4.3得到了CDL的一个可靠而完整的证明系统：首先，包括经典命题逻辑的所有公理和规则，其次，包括所有模态的必然性规则：从模态中推导出模态B的必然性规则，模态Ck的必然性规则和模态Cb的必然性规则;第三，包括下列公理：正态性：<$Bθ（正态→负态）→（Bθ正态→Bθ负态）a a a► Cbθ（θ→θ）→（Cb θ→Cb θ）► Ckθ（α→β）→（Ckθ α→Ckθ β）知识的真实性知识的持久性：K→Ba a全内省：B→K Ba a a► <$B→K <$Ba a a假设被（假设性地）接受：[12]实际上，这可以通过任意选择良序≤a来证明。[13]这种用doxastic条件句来定义知识的方法可以追溯到[25]。16A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5一一一一一一最小修订：<$$>B<$$>→（B<$$>θ参与B<$（<$→θ））a a a不动点公理：<$Cbθ <$→ <$$>EbθCbθ <$► Ck θ→Ekθ Ck θ归纳公理：<$Cbθ（<$→Ebθ <$）→（<$→Cbθ <$）► Ckθ（ε→Ekθ ε）→（ε→Ckθ ε）Q与我们的主题相关的是在信念修正模型中使用条件的标准哲学问题（例如参见[11，15，20]）。在这种情况下，有趣的是，我们的条件信念算子（被理解为条件）如何避免Gardenfors这个结果是基于这样的假设，即任何这样的条件都应该满足所谓的拉姆齐检验[19]。在[20]之后，拉姆齐检验可以用语法术语表述为：（R）如果我们将条件“if P then Q“解释形式T=sR的理论，对于某个命题R），则我们得到以下Ramsey检验的语义版本：（R？） 对于每个RS：sRBPQisRaPQ。a a a很容易检验这是假的：给定我们的CDM假设，在这种解释下，（R要看到这一点，观察（R？）等同tot∈sR：tP<$Q。 但是，通过我们的postulates，t∈sRimpliestP=sP=saaP。所以，a a a a a如果R是零，则最大值为（R）的值。）是简单的等式，以用于计算PSNR，而这一切都不足以满足R&D的需求。 苏威我们可以看到，拉姆齐测试只能成功，如果我们有sa=sR在一般情况下，即如果条件信念将崩溃到无条件的：这是在某种程度上我们自己的语义版本Gardenfors另一方面，观察到（R？）在无条件的上下文中确实成立，也就是说，对于R=S（即对于对于T=sa）：saBPQiaaP=sPQ。a a拉姆齐检验的深层原理是，它对待关于信念的假设信念和对待关于事实的假设信念的方式是一样的;只有当行为人在做出假设时，会像修改他们的事实信念一样修改他们对自己信念的信念，这个检验才是正确的。但这与内省知识对信念修正的限制是不一致的：内省的代理人知道他们自己的信念，因此不能接受假设，与这些知识背道而驰一个假设的信念系统（例如，A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）517一一一上面的反例）可能包括与非一致性信念系统（s a）不同的本体陈述; 2但它包括与这个无条件信念系统完全相同的doxastic/epistemic陈述B PQ。由于内省，关于信念的信念不能被修正，不是我们这里所说的（[14]只有一种5动态信念修正：公告在上述的条件性教条模型中，信念修正是静态的，纯粹是假设性的。事实上，修正算子不能以任何方式改变模型：所有的可能性都已经存在，所以无条件信念和修正后的条件信念都指向同一个世界和同一个时刻。[15]相反，信念更新是信念修正的一种动态形式，旨在捕捉由学习（或其他形式的认识/信念行为）引起的信念的实际变化正如之前已经注意到的[13，6，5]，原始模型通常不包括足够的状态来捕获以这种方式出现的所有认知可能性。因此，与前一节相反，我们现在允许信念修正，改变原始CDM。在这一节中，我们关注的是公共公告，它以最小的方式改变了认知（和条件doxastic）模型：它们只能通过“相对化”来缩小给定一个模型（CDM）S，记为s Q，外观图和估价在S.对于任何S-命题P∈S，我们定义相对化CDMP！（S）采取：(i) P的状态集合！（S）是集合P，(ii) （sQ）：=sQ，对于每个s∈P和Q<$P，P！（S）a(iii) 噗！（S）：= pP.作为一个直接的结果，我们得到更新后的无条件信念来自于先前的条件信念：（s a）P！（S）=（s P）P！（S）= s P.a a我们解释动作P！作为从满足P的任何当前状态s∈S到状态s∈P的过渡关系！（S）。我们的公共声明逻辑的语法是通过简单地添加涉及动态模态的构造来获得的！<公司简介CDL的语法。 对于语义，我们包括以下额外子句：你<好！> S= S！（S）。为了获得一个可靠而完整的证明系统，我们在CDL的公理中添加了公共声明的归约公理：[14]记住BPQ的意思是“如果a学习了P，那么他就会相信Q（在学习之前）是这样的”。假设你碰巧相信<$P，有人问你：“如果我告诉你P是这样的，这会改变你对你目前相信<$P的事实的看法吗？”显然，正确的答案是：“不，不会。它确实会改变我对P的信念，但不会改变我对现在我相信<$P这[15]事实上，假设（*2）（以及CD框架定义中的相应子句（4））只能如果使用所谓的摩尔句子（例如，“Komi”）的修正被理解为仅在假设上是可能的，则保持不变。智能体a18A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）5A aA一一一<快！> p参与 计划！><参与吧！公司简介<快！>（θ）<参与！>你<好！> θ！>CkθParticipate< Ck！><θ！公司简介aa<快！ > Bθ参与者B<！><θ！>你好！> Cbθ参与者Cb<！><θ！公司简介aaaa其中p6对子组的在本节中，我们将讨论“私下了解一个事实”的具体A到一个代理子组 直觉是，公告被广播给A组的代理人，而局外人B/∈A并不怀疑这一点。为了简单起见，我们在这里考虑的情况下，这是常识，没有其他任何事情可以发生：（向组A的该特定句子P的）特定通告是此时可以广播的唯一消息;唯一的替代方案是不发送消息，即“什么都没有发生”的静默动作τ AP（但是其中局外人不知道这一给定一个CDMS和一个S-命题PS，我们定义了一个新的，更新的CDM在私人公告P！A（S）如下：对于每个旧状态s∈S，我们取两个不同的新拷贝P！A（s）（表示P被告知群A之后的状态）和τA P（s）（表示对应的状态，在该状态中什么都没有发生，但局外人b/∈A认为P被告知群A是可能的）。然后通过下式获得新模型SJ(i) P的新状态集！A（S）是集合SJ=P！A（P）τA P（S）(ii) 对于所有的a∈A：P！（s）Q：=P！−1（sP！A（Q））和τA P（s）Q：=τAP（sτAP−1（Q））Q QτAP−1（Q）−1(iii) 对所有b/∈A：τ A P（s）b P！A（s）b ：=τA P（sb ），如果s（b）<$τA P−1（Q）/=0;且τ P（s）Q=P！（s）Q：=P！ （sP！A（Q），否则AbAb(iv) p A（pS）τA P（pS），其中我们使用符号σ（Q）：={σ（s）：s∈Q}和σ−1（QJ）：={s∈S：σ（s）∈QJ}对于两个“动作”中的任何一个σ ∈ { P！A，τA P}，并且对于所有集合Q<$S，QJ<$SJ。我们解释了条件信念更新的子句第二条：知情人知道在任何情况下，哪个动作σ发生了（不管是P！A或τA P），因此如果在该动作之后，他们被给予一些新的信息Q，则他们应用以下算法。他们首先根据新的信息重新考虑他们关于过去状态的信念：他们可能不得不用这样一个事实来修正这些信念，即在这个特定的动作发生之后，Q变成真的;所以他们用σ−1（Q）;然后它们通过将动作σ应用于允许通过这些过去的信念：这给出了他们对行动σ后世界状态的当前信念。在第3条中，局外人基本上应用相同的算法，但是（不知道哪个动作真正发生）他们保持默认的信念，即他们所看到的，即动作τ AP（即A. Baltag，S.Smets/Electronic Notes in Theoretical Computer Science 165（2006）519我我信息Q，也就是说，除非事先已经知道Q在τA P之后不能成为真;在这种情况下，他们A正在发生，因此他们将上述算法应用于σ=P！A.对于我们的语法，我们替换<了上面的公共声明模态！>>用动态模式<来实现！A>和τ A>对应于上述两种作用类型。<[16]语义由标准PDL子句给出：σ<>S：={s∈S：σ（s）exists and σ（s）∈SJ}。为了得到一个完整的证明系统，我们将条件信念的归约公理替换为以下公理：<快！A> B θ参与者B<！A><θ！中文（简体）a a<τA> BθParticipB<τA>θ<τA>a一<快！A> B θ $>参与者B <τA>θ< τ A>参与者（K b [τ A]<$θ→B<！A><θ！A>）bB b<τ A> B θParticipB< τA>θ< τ A>（K b [τ A]<$θ→B<！A><θ！A> A），bb b对于所有的局内人a∈A和所有的局外人b/∈B。通过这些修改，并通过消除涉及共同知识和共同信念的公理和规则，我们获得了私人公告（没有共同的知识/信念）。[17]最后，这里是拉姆齐检验的承诺的R！a（s）aBa[P！QiP！a（R！a（s）回到玛丽。在介绍了这些模型之后，我们回到引言中提出的例子。因此，给定夏娃（e）、亚当（a）和玛丽（m）