理论计算机科学电子笔记262（2010）141-156www.elsevier.com/locate/entcs动态认知逻辑的Jens Ulrik Hansen延斯·乌尔里克·汉森1，2数学，逻辑和智能系统/哲学和科学研究罗斯基勒大学丹麦罗斯基勒摘要在过去的十年里，人们对各种形式的动态认知的兴趣越来越大。逻辑模型的信息流和效果，这对多智能体系统中的知识。然而，这个企业主要是应用程序和语义驱动的。这导致了动态认知逻辑的证明理论在本文中，我们试图弥补这一部分，提出终止画面系统的完整动态认知逻辑与行动模型和混合公告逻辑（都没有共同的知识）。Tableau系统是现有Tableau系统的扩展，此外，我们已经使用动态认知逻辑的归约公理来定义逻辑的动态部分的规则。使用Br aüner、Bolander和Blackburn介绍的方法进行测定。关键词：动态认知逻辑，公告逻辑，终止表系统，决策过程，混合逻辑，归约公理。1介绍经典认识逻辑在哲学和计算机科学中都发挥了重要作用。然而，近年来，也看到了在知识的动态，即如何不同的代理人的知识可以改变由于系统的发展的重要性。有两种方法可以为认知逻辑增加动态性。人们可以将它与时态逻辑结合起来，也可以将它与某些动态动作逻辑结合起来。后一种方法已经变得越来越普遍，并导致了现在所谓的动态认知逻辑（DEL），其中包括所谓的认知行为的运算符（参见。[13]）。 对DEL的兴趣主要与应用程序有关，并且主要是语义上的1感谢Torben Braner和Sine Zambach对论文草稿提 出的意见。也感谢匿名 评论者的宝贵意见。 作者通过HYLOCORE项目得到丹麦自然科学研究委员会的2jensuh@ruc.dk1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.011142J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141有动力。因此，只有很少的尝试，以发展一个丰富的证明理论DEL超出标准的希尔伯特风格的系统已经执行。 这项工作试图使 通过讨论不同类型的动态认知逻辑的终止表系统，来解决一些问题。人们可以添加到经典认知逻辑中的最简单的动态形式是公共公告算子。该语言被扩展为[]类型的公式，读作“在在语义层面上，运算符[]对应于移动到仅由为真的状态组成的子模型（因此我们在这里只关心真实的公共声明）。这个简单的扩展称为公共通告逻辑（PAL），然而，正如[13]中的许多应用所示，它非常有用。忽略了操作符3的常识，这个逻辑相当简单，并且已经存在一些tableau系统，参见[1]和[7]。本文中的方法是不同的，从这个意义上说，我们试图避免构建新的复杂和定制的tableau系统，而不是使用现有的系统。这是可能的，由于减少公理。从DEL的短暂历史开始，归约公理在显示完备性和表达性结果方面发挥了重要作用。证明了公告逻辑并不比底层的认知逻辑更具有表现力。使用归约公理，可以将公共声明公式转换为等价公式，而无需任何公共声明运算符。有很多其他可能的认知行为，超越了纯粹的公开-lic公告：对子组的公告，私人通信，秘密公告等。 Baltag、Moss和Solecki（在[2]中）的见解是，所有这些认知行为，被认为是行为模态，也可以由一种形式的Kripke模型来表示。在Kripke模型上使用一般的乘积运算，它们可以被赋予语义。更令人惊讶的是，它表明，这些更复杂的行动模态的公式也可以减少到基本的认知公式没有任何行动模态。当然，这需要比公开宣告更高级的归约公理当一个人想证明DEL的有效性时，他可以简单地翻译有效的-将一个没有动作模态的认知公式转化为一个没有动作模态的认知公式，然后使用现有的画面（或其他）系统。但是，这种转换可能会导致公式的大小呈指数级增长。如[10]所示，这种指数增长对于公开公告来说是不可避免的。这一事实提供了使用DEL的另一个动机，因为它使我们有机会表达比经典认知逻辑更紧凑的事物。在[10]中还表明，PAL的有效性检查的复杂性并不高于潜在的认知逻辑。因此，首先翻译然后使用已知的经典认知逻辑证明方法的方法可能是不可行的。这证明了[1]和[7]中给出的PAL的直接表系统。在具有任意认知行为的DEL中，问题变得复杂得多。在这里，挑战在于如何表示动作模态。由于PAL是DEL的一部分，[10]也表明翻译的放大3在本文的其余部分，至少在结论之前，我们将忽略常识。J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141143L¬ ¬ ∧ → ∨ ∧¬¬ ¬ ∧ → →∨在一般的DEL情况下可以是指数的。 然而，目前作者还不知道决定DEL有效性的复杂性是什么。[4]当将全局模态添加到底层认知逻辑时，其复杂性已经是指数级的了。 在这种情况下， 因此，转换不会破坏最坏情况的复杂性。本文的工作是基于这样一种思想，即用归约公理作为规则，对场景中的语义进行翻译。在实践中，这比在开始时执行整个翻译更有效5，但在公告的情况下，它可能没有[1]和[7]的方法那么快。然而，他们的tableau系统只适用于公告逻辑，而这里提出的方法进一步适用于全动态认知逻辑和公告逻辑的混合版本。我们在本文中的tableaux保持终止使用Br aüner，Bolander和Blac kburn（[5]，[6]和[4]）的方法。 这里的演示将基于[ 4 ]中的方法。对于基本模态逻辑，它们通过注意到最大公式复杂度随着新前缀的引入而下降来显示终止，这使得无限的tableaux不可能。在本文中，我们表明，从本质上讲，这一论点可以适应的设置中使用的减少公理作为额外的tableau规则。本文的结构如下：首先，我们介绍了公告逻辑，一个混合公告逻辑，和全动态认知逻辑（第2节）。然后，在第三节中，我们提出了一个完全动态认知逻辑的终止表系统。 在此之后，我们将演示如何使用该方法以创建用于混合公告逻辑的终止画面系统。最后，我们提出了一些结论性意见，并讨论了进一步的研究。2动态认知逻辑我们将首先给出公告逻辑的正式定义。公告被添加到正常的模态逻辑K，但它可以很容易地扩展到S5的情况下，这是经常用于建模知识。我们将忽略常识。首先，我们假设一个有限的主体集合A和一个可数的有限的命题变量集合PROP。使用[13]的术语，公共声明逻辑的语言将表示为K[]，并给出通过以下语法：：：= p | ¬ ϕ| ϕ ∧ ψ| Ka|[]，[4]在处理任意DEL公式时，问题是如何测量作用模态的大小。一方面，一个动作模态可以算作一个符号，但在决定有效性时，需要动作模态的更精细的结构。 因此，这可能导致高复杂度在这个大小的公式中进行有效性检查。另一方面，使用另一种行动方式的大小度量，可以在该大小中以较低的复杂性来决定有效性5在最坏的情况下，在地图上进行翻译可能不会更有效。但似乎至少在两种情况下，在计算机上翻译将加快决定公式的过程。的第一种情况是只需要几个翻译步骤就可以检测到不一致，例如在公式[[（qr）]Ka（pq）]（p（r）（[ [ （qr）]Ka（pq）]（p（r））。 另一种情况是对翻译的需要可能只发生在画面构建过程的最后，例如在公式Ka[p]<$$>Ka<$[q]<$q<$Ka（[q]p<$[p]q）中。144J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141⟨ ⟩M|∧ ¬ ¬ ¬¬LM∈∈ ∈ ∨ → ↔¬MM|M|∈M|L→LL其中pPROP和aA.连 接 词 和的定义通常来自于和，对偶运算符Ka和[]由K a和K y表示。Ka的解释是，“代理人a知道“，而[]的解释是，“在（真实）公开宣布之后，就是这种情况”。这些解释可以用以下形式语义来描述：克里普克框架（或仅仅是一个框架）是一个对F =W，（Ra）a∈A，由一个非空的状态集W（或可能世界）组成，对于每个a ∈ A，W上的二元关系Ra（即RaW×W）。模型M是由框架F和赋值V组成的对，赋值V将W中的一组状态分配给PROP的每个命题变量（即V：PROP → P（W））。给定K[]的公式，模型=w，（Ra）a∈A，V 在模态逻辑中，状态w W，即在w处的真值，记 法w=，被定义为标准，取Ka作为与Ra对应的盒模态。此外，我们还增加了以下条款，[编辑]M，w| =[]我的 M，w| = m表示M|2000年，w| = 0，其中模型M|=|拉斯特河|拉瓦河|电子邮件的定义如下：W|n= {v ∈ W|M，v| R a= 0|= Ra|公司简介|）V|（p）= V（p）|- 是的我们写=0 if，w = n，对于所有w我们说，如果=所有型号均适用。这种语义的逻辑用PA表示，称为公告逻辑。在这个逻辑中，不难证明以下几点的正确性（一）（二）（三）（四）（五）[2014]p参与 （→p）[]<$$> Participate（→<$[]）[]（χ）Participate（[][]χ）[]KaParticipate（→Ka[]）[][]×参与 [[]] χ.这些是公开声明的归约公理（[13]）。将这些公理与[1]的必要性一起添加到多模态K的希尔伯特式证明系统中，将导致PA的可靠且完整的证明系统（详细信息参见[13]）。请注意，在这些归约公理中，公共声明操作符范围内出现的公式的复杂性在“Participate”的左侧比右侧大这可以用来定义翻译T：K[]K，其中K是标准的多模态语言。翻译J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141145¬¬¬ → ¬除了公共通告运算符之外的所有逻辑运算符（例如， T（）=T（λ））。在这种情况下，当翻译遇到一个[]运算符，它使用约简公理来降低运算符范围内的公式的复杂性[001 pdf1st-31files] t（ （n））= T（n）T（[n] n）。这种翻译可以被证明是PA到多模态K的真值保持翻译，这表明添加公共声明运算符不会增加146J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141↔∈L语言[6]这种递归转换不是以正常方式递归的，因为在归约公理（1）因此，为了证明翻译的正确性，需要一种新的公式复杂性度量.一种可能的方法是（取自[13]）：定义2.1通过归纳子句定义一个复杂性测度c：LK[] →Nc（p）= 1c（<$）= 1+c（）c（k）= 1 + max{c（k），c（k）}c（K）= 1 +c（k）c（[]）= （4+c（））·c（）关于这个复杂性度量可以表明的是，当移动到子公式时，它会减小，而且，约简公理（1）-（5）的左手边的c在下一节我们考虑tableau系统时，这一点很重要。我们将不会为PA提供一个表系统，而是为它的混合扩展，即[8]的混合公共声明逻辑。为了获得这种新的逻辑，我们将首先扩展语言。为此，我们固定一个可数的有限集合的名词NOM不相交的命题变量。混合公告逻辑LHPA的语言定义如下：：：= p| 我| ¬ ϕ| ϕ ∧ ψ| Ka| []| @我爱你|E，其中p∈PROP，i∈NOM，a∈A。名词将作为国家的名称。公式@i表示在i表示的状态下为真，而E表示存在一个为真的状态。语义的具体化与混合逻辑中的标准有些不同原因是公共公告操作符的语义将我们带到子模型，在子模型中，由名词表示的状态可能会消失。为了解决这个问题，我们扩展了模型类，使得估值最多为每个名义分配一个状态，而不是一个状态（关于这些问题的更多信息，请参见[8]）。因此，模型M=W，（Ra）a∈A，V a的定义与PA相同，但 对 估值V：PROP_NOM → P（W）的进一步要求，|五㈠|对于所有i NOM，≤ 1。对于与K[]一致的语言部分，语义子句与PA相同。对于语言的新部分，我们定义：M，w |= ii <$ w ∈ V（i）M，w |=@ i<$ i <$i 存在一个v ∈ V（i）使得M，v |=M，w |= E <$ i <$ 存在一个v ∈ W使得M，v |= 0。[6]当底层逻辑是S5时，这也有效，然而，如果想要使用逻辑KD 45对信念进行建模，就会出现问题。问题在于，在取子模型的操作下，由KD 45的公理定义的框架属性没有被保留。因此，我们不能得到关于信念总是被解释为KD 45的模型类的完整性。换句话说，公共公告操作符的给定语义可能导致代理在公共公告之后具有不一致的信念J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141147||≡ ∧ ≡→L⟨⟩⊗这种语义产生的逻辑称为“混合公告逻辑”，用HPA表示。E和@i的对偶算子将用A和@i表示。注意，由于名词仅部分表示状态，@i不再是它自己的对偶。 我们仍然有等价@ iE（i）和@ iA（i））但是现在这些可能不再是等价的了。[7]这样，满足算子就被分成了存在性的量化器和普遍性的量化器。事实上，名义i表示模型中的某个东西（即V（i）=1），可以用公式Ei表示。关于希尔伯特式证明系统的完备性也可以使用归约公理来证明，如[8]中的以下内容（六）（七）（八）[]i Participate（→i）[]@iParticipate（→@i（[]））[]E Participate（→E（[]））由于我们扩展了K[]的语言，我们也需要扩展测度c的定义。通过在定义2.1中添加以下条款来实现：c（i）= 1c（@i）= 1 +c（）c（E）=1 + c（E）.在这种复杂性度量下，新的归约公理（6）公告只是 一 种 的 认知 行动 不过 到 为了以统一的方式处理大量的认知行为，Baltag，Moss和Solecki（[2]）引入了行为模型的概念。 认知行动模型背后的直觉是，代理人可能不确定到底发生了什么行动，每个行动都有一个先决条件，必须满足该行动才能发生。认知动作可以用Kripke结构来表示，其中每个状态都是一个事件/动作，而不是一个完整的赋值，每个事件都被分配了一个语言公式作为前提条件。现在我们来谈谈形式上的细节。一个动作模型M=S，（Qa）a∈A，pre由有限个事件集S，所有主体在S上的可达性关系Qa组成a ∈ A，以及一个前置条件函数pre：S→L，它为每个事件指定一个前置条件（对于某个逻辑语言L）。公式语言L K和动作模型语言L act必须同时使用相互递归来定义。K法动作模型语言LK的定义如下：α：：=（M，s），其中M=<$S，（Qa）a∈A，pre <$是一个行动模型，使得s ∈ S且pre：S → LK <$. 同时，公式语言LK的定义如下：：：= p| ¬ ϕ| ϕ ∧ ψ| Ka|[α] α，7这些等式还表明，在语言中我们不需要@i操作符，因为它可以用E和i来定义。 如何使[ 4 ]中的tableau系统在语148J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141言中的适应变得容易呢？J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141149⊗其中p∈PROP，a∈A，α∈ L作用。8公式[M，s]的读数是认知行为（M，s），K情况就是这样”。M代表了代理关于什么事件正在发生，而s是实际发生的事件。对于一般的认知行为，稍加思考就会发现，它们实际上可以导致克里普克模型的扩大我们在语义学中理解这一点的方式是通过定义Kripke模型和动作模型之间的产品更新对于Kripke模型M= W，（Ra）a∈A，V和动作模型M=S，（Qa）a∈A，预先定义了限制性乘积MM=WJ，（RaJ）a∈A， V Jby：WJ={（w，s）∈ M × M| M，w| = pre（s）}RaJ（（w，s），（v，t））我的Ra（w，v）和Qa（s，t）VJ（p）={（w，s）∈ WJ|w ∈ V（p）}。我们现在可以将动作模态[M，s]的语义定义为：M，w| = [M，s] ii M，w| = pre（s）意味着M <$M，（w，s）|= 0。其他逻辑运算符具有正常的语义，有效性也被定义以标准的方式。这种逻辑将被称为动态认知逻辑，并表示为AM。请注意，我们现在已经排除了混合动力机械，因为它是不清楚如何将其与行动模型结合起来。9与公告的情况一样，增加动作情态并不能增加语言的表达力。这一点再次通过提供归约公理来证明（例如参见[13]）。简化公理，现在稍微复杂一点，是：（九）（十）（十一）[男，女]p （pre（s）→p）[M，s]<$Participate（pre（s）→ <$[M，s]）[M，s]（参与者）（[M，s]参与者[M，s]）（十二）[M，s]KaParticipate（pre（s）→Ra（s，t）Ka[M，t]）（十三） [M，s] [MJ，sJ]Participate[（M;MJ），（s，sJ）]，其中，在最后一个公式中，“;”操作是对动作模型的语义操作。给定两个动作模型，M=S，（Qa） a∈A，pre和MJ=SJ，（QJa） a∈A，preJ，组合（M;MJ）=SJJ，（QJaJ）a∈A，preJ定义为：150J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141SJJ=S×SJQJaJ（（s，s），（t，tJ））i =Qa（s，t）和QJa（sJ，tJ）preJJ（（s，sJ））=<$M，s<$preJ（sJ）.[8]通过这个定义，我们给语言的语法加载了沉重的语义机器，然而，由于我们只处理有限的动作模型，所以可以列出并命名它们。关于这个问题的更多讨论见[13]。[9]当存在能够扩展状态的模态时，对名词的解释并不明显。通常，混合逻辑中的名元是一类特殊的命题变量，它们在严格意义上为真，一个国家。然而，当将认知模型的产品与动作模型一起使用时，认知模型的单个状态可以在结果产品模型中变成多个状态。因此，如果我们保持产品模型的原始估值定义，我们就打破了只有名词为真的要求。在一个州。 另一方面，估值似乎没有明显的替代定义J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141151↔¬¬¬L∧∧见[13]为有效的减少公理。至于HPA，需要一个新的复杂性度量。[13]这是一个从[13]中提取的定义2.2复杂性测度d：LK →N归纳定义为：d（p）= 1d（<$）= 1+d（）d（k）= 1 + max{d（k），d（k）}d（K）= 1 +d（k）d（[M，s]ε）= （4+d（M，s））·d（ε）d（M，s）= max{d（pre（t））|t ∈ M}。至于公开声明，可以表明，当从约简公理（9）3AM的桌面系统在本节中，我们将在现有的多模态K表系统的基础上引入一个AM表系统，其中我们添加了约简公理作为表规则。这样做不会违反原始系统的终止性或完整性。形式上，我们将tableau视为一个有限分支的三，其中每个节点都由我们语言的公式标记作为底层多模态K逻辑的基本表系统，我们将使用[4]中的表系统，这是一个标准表系统。tableau系统是一个前缀tableau系统，因此所有出现在tableaux上的公式都有形式σ，其中σ来自前缀的有限集合中的某个固定可数项前缀背后的直觉是，它们表示可能的Kripke模型中的状态 所以在σ后面的直觉是σ在σ处成立。 此外，我们在表上也有形式为σRaτ的公式，表示τ可由主体a从σ获得。这些将被称为可访问性公式。表系统的规则适用于表的分支，如图1所示。在规则（[AM]）和（[AM]）中，t是使用归约公理将公式[M，s]转换为较低d-复杂度的公式的运算。例如，t（[M，s]（λ））= [M，s]λ[M，s]λ。[10]忽略可及性公式，规则中直线以上的公式称为前提，直线以下的公式称为结论。在构建tableau时，如果公式已经在分支上出现，我们永远不会将其添加到分支中，并且我们永远不会对分支上的同一个公式应用两次（Ka 如果一个分支同时包含σ和σ对 于 某个公式和某个前缀σ，则该分支称为闭分支，否则称为开分支。闭合的画面是其中所有分支都闭合的画面。一个公式的tableau证明是一个封闭tableau，其中σ<$是根公式。10t不应与语言的完整翻译混淆如第2节所述。这里t只翻译/降低一个级别。152J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141¬不¬≤¬¬.Σ≤ ≤ ≤≤σ¬¬ϕ(σϕ¬¬）σϕ∧ψ(∧)σϕ（σ ϕ（掌声）（）σψσ¬ϕσ¬ψσ<$K一σRaττ¬ϕ（€K1一）σKa στϕσRaτ（Ka）σ[M，s]（[AM]）σt（[M，s]σ）1.前缀τ对分支来说是新的（€[AM]）σ<$t（[M，s]）σ<$[M，s]Fig. 1. Tableau规则AM。3.1Tableau系统在[ 4 ]的工作中，确保终止的两个重要性质是：出现在表上的所有公式都是子公式或子公式的否定。根公式，并且每个规则只生成公式复杂度较低的内容。这两个属性对于确保画面的有限性至关重要。然而，这些属性对于我们的tableau系统失败了，因为规则（[AM]）和（[AM]）可以生成不是前提的子公式的公式，并且可能具有更高的公式复杂度。 但是，使用d-复杂性的概念并扩展子公式的概念，我们可以保持有限性。在定义子公式的新概念之前，需要一个引理。对于一个动作模型M=S，（Qa）a∈A，pre，设D（M）表示定义域，即.D（M）=S。引理3.1设σ0<$0是表T的根公式，并假设[M，s]<$0出现在T上。然后，存在n≤d（n =0）和动作模型M1，.，Mn发生在n =0，使得D（M）= D（M1）×. × D（Mn）.证据证明是通过构造的归纳法进行的。这是一个明显的主张，因为[M，s]是0。同样明显的是，当应用任何规则时，除了（[AM]）和（[AM]）到形式为[M，s][MJ，sJ]或[M，s][MJ，sJ]的公式，结论和前提中的动作模态具有相同的域（或动作模态已被完全移除）。现在，对于应用于两个连续模态[M，s]和[MJ，sJ]的规则（[AM]）和（[AM]）。假设引理的声明对于[M，s]和[MJ，sJ]都是真的然后(14)D（M;MJ），（s，sJ）= D（M1）×... × D（Mn）× D（MJ1）×... ×D（MJm），其中，对于所有1 i，Mi和MJj都出现在{0} 中n和1JM. 因此，唯一需要证明的是，n+md（0）。注意，复杂性度量d是动作模态可以嵌套多深的上限此外，对于每一个嵌套动作模态，只能再增加一个J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141153¬不不∈ D¬¬¬由规则（[AM]）和（[AM]）到（14），这也将嵌套模态的数量减少一个。因此 ，n + m必须小于d（n =0）。Q定义3.2一个公式称为公式的d-子公式，如果• d（n）≤d（n），• 每一个出现在中的命题变量p也出现在中。• 如果动作模态[M，s]出现在[M，s]中，则存在动作模型（M1，s1），.（Mn，Sn），其中Mi出现在n中，对1 ≤i≤n≤d（n），且D（M）= D（M1）×.×D（Mn），注意，如果动作模态[M，s]出现在公式中，那么M的所有前提条件也被计为出现在公式中，并且通过定义d-复杂度，我们自动地对所有t（M）具有d（pre（t）） d（t（[M，s]s））此外，当移动到严格子公式时，d-复杂度降低。因此，我们得到以下引理，并从中得到一个子公式性质。引理3.3对于每个tableau规则，结论的d-复杂度严格小于前提的d-复杂度引理3.4（d-子公式性质）设T是一个表，其根公式为σ0<$0. 则对于T上的每个预定公式σ ∈，σ ∈是σ ∈ 0的d-子公式。证据 让是以σ0<$0为根公式的表。 这个证明是用归纳法来证明的关于场景的构建。由引理3.3可以得出，任何公式的d 小于d（0）。 此外，很明显， 规则可以引入尚未出现在根公式中的命题变量。可以引入新的动作模态的唯一规则是应用于公式[M，s]Ka，[M，s]Ka的（[AM]）和（[AM]）规则，[M，s][MJ，sJ]，和[M，s][MJ，sJ]π。对于前两种情况，可以引入形式为[M，t]的新动作模态，但M必须是与前提中相同的动作模型。因此，这些情况只是定义3.2中第三点的特殊情况。 最后一从引理3.1得出的两种情况是这两个也保持d-子公式。Q定义3.5给定一个表分支Θ和一个出现在Θ上的前缀σ，令TΘ（σ）：= {θ|σ在Θ上}，引理3.6设Θ是表的分支，σ是出现在其上的前缀，则集合TΘ（σ）是有限的。证据根据引理3.4，所有关于Θ的公式都是根公式的d-子公式。因此，如果我们能证明对于所有公式，d-子公式的集合是有限的，则引理成立。这可以通过n=d（n）上的归纳法证明，给定固定数量的命题变量N。对于n= 1：很明显，对于所有复杂度c（n）= 1的公式n，n的d-子公式只能有N个对于归纳步骤，假设只有有限个d-子公式，154J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141≤¬都用d（n）表示给定一个公式n，d（n）= n+1，很容易看出，n的任何d-子公式也是一个公式的d-子公式，该公式的d-复杂度小于或等于n，或者是由这些公式之一构造的。通过归纳，只能有有限的许多第一类。对于第二类，我们根据结构的不同分为不同的情况。 很容易看出，给定有限个公式，使用逻辑连接词和Ka运算符只能构造有限个新公式（因为只有有限个a）。在动作模态的情况下，注意定义3.2的第3点只允许有限多个动作模型域，并且对前提条件的d这就完成了引理的证明。Q定义3.7设Θ是一个表分支，σ是出现在Θ上的前缀，则定义mθ（σ）为：mΘ（σ）= max {d（σ）}| σ ∈ Θ}。注意，d-子公式属性证明了这是定义良好的。我们现在可以采用[4]的方法来证明AMtableaux总是终止。定义3.8当一个前缀τ通过规则（<$Ka）在分支Θ上被引入到公式σ τ中时，我们说τ是由σ生成的，并用στθτ表示。在此之后，我们可以很容易地证明，如在[4]中：引理3.9如果Θ是表分支，则θ是无限的当且仅当存在一个关于Θ的前缀的无限链σ1<$θσ2<$Θσ3<$θ...证据 参见[4]。Q引理3.10设Θ是一个表分支，σ和τ是出现在Θ上的两个前缀。则σθτ意味着mΘ（σ）> mΘ（τ）。证据 如[4]所述，证明是通过的，一旦注意到规则（[AM]）和（[AM]）降低了从前提到结论的d-复杂度，并且这些规则都没有引入新的前缀。Q正如在[4]中，现在可以很容易地从引理3.9和3.10得出终止：定理3.11（表系统的终止）任何为L-K-公式构造的表都是有限的。3.2Tableau系统合理性并不难证明。 底层多模态逻辑的规则是标准的，很容易被认为是合理的。通过归约公理（9）仅使用涉及语言的这一部分的规则的底层多模态逻辑的完整性已经是众所周知的（例如参见[4]）。给定J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141155M¬¬¬¬⊆¬¬一个开饱和分支Θ，由出现在Θ上的前缀构造了一个正则模型，并定义了可达性关系，由此可达性公式σRaτ出现在Θ上.命题变量p的赋值是相对于σp和σ p（如果有的话）在Θ上出现的值来定义的。然后，简单地证明一个真值引理，即：对于Θ上的所有预固定公式σ ∈M，σ| = 0。对于我们的表系统，这个构造和真值引理的公式化是相同的。然而，我们不是用公式复杂性的归纳法证明真值引理，而是用d-复杂性的归纳法证明它，并增加了两种新的情况[2019 - 01 - 19 00：00：00][2019- 01 - 19 00：00][2019 - 01 - 19 00：00] 然而，这些情况是非常简单的：假设σ[M，s]出现在Θ上。然后通过Θ的饱和，σt（[M，s]）也出现在Θ上，并且由于t（[M，s]）具有比σ [M，s]小的d -复杂度，因此通过归纳得出M，σ| = t（[M，s] m）。但是，根据归约公理（9）-（13）的有效性，也可以得出M，σ| = [M，s] [1][2][3][4][5][ 6][7][8][9][因此，我们得到：定理3.12图1的表系统相对于逻辑AM是健全和完备的。4混合公共声明逻辑在本节中，我们将介绍一个用于HPA的tableau系统。它比前一节的表系统既简单又复杂。简单化在于纯粹地看公共公告，而复杂化在于将基本的认识逻辑扩展到混合逻辑。这种简化大大缩短了引理3.4和3.6的证明，但混合机器使我们需要更高级的终止证明，如[4]所示。 我们的tableau系统将基于[4]中的一个小修改，进一步扩展为公共声明的归约公理规则。我们重复使用第3节的所有术语。tableau规则如图2所示。在规则（[]）和（[]）中，运算t是通过HPA的归约公理定义的，与上一节相同。与[4]相比，还省略了一个规则，并且规则（@）已被替换。这两个变化都是为了处理这样一个事实，即在我们的逻辑中，名词只能部分地表示状态。规则（Ka）、（@）、（@）和（E）称为前缀生成规则。tableau的构造是在这样的约束下完成的，即没有前缀生成规则被两次应用于同一分支上的同一前提，并且如果公式已经在该分支上发生，则永远不会添加到该分支。此外，为了使tableaux终止，我们引入（如[4]）循环检查机制。在此之前，我们需要一个“urfarer”的概念定义4.1给定一个分支Θ，如果τ是在Θ上最早引入的前缀，使得TΘ（σ）TΘ（τ），则前缀τ是前缀σ的原函数。我们用uΘ（σ）=τ表示。[11]这里使用的urfarer概念在[4]中称为包含urfarer156J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141σ¬¬ϕ(σϕ¬¬）σϕ∧ψ(∧)σϕσψ（σ ϕ（掌声）σ¬ϕσ¬ψ（）σ<$K一 （€K1一）σRaττ¬ϕσ@iσKa <$σRa τ（K）一τϕσE（E）1τϕσ<$Eτ<$（€E）2（@）1τi@i厄τi（€@）1σ σi τi（Id）τϕτϕσ[]（[]）σt（[]）τ¬ϕ（<$[]）σ<$t（[]）[1.前缀τ对分支来说是新的。 2.前缀τ已经在分支上了。图二. HPA的Tableau规则。HPA画面的构造受以下约束的约束前缀生成规则仅允许应用于分支上的公式σ，如果σ是该分支上的一个urfather4.1HPA表的终止与一般的动作模型一样，我们需要一个基于定义2.1的复杂性度量c的子公式的扩展概念。定义4.2一个公式称为公式的c-子公式，如果• c（n）≤c（n）• 每个命题变量和所有出现在“”中的名词也出现在- 是的在HPA表格的情况下，可以直接证明以下内容引理4.3对于每个tableau规则，结论的c-复杂度小于前提的c-复杂度引理4.4（c-子公式性质）设T是一个具有根公式σ_n的表. 如果预置公式τ出现在T上，则τ是τ的c-子公式。证据通过引理4.3和没有规则可以引入新的名词或命题变量的事实，很容易检查所有的规则，如果它们有c-子公式作为前提，结论也将是c-子公式。J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141157≺≺<$T ≤ <$T¬≤¬¬一M|| ≤注意，规则（@）只能在表格上出现一个预先固定的公式τ@iχ时才能应用，在这种情况下，通过归纳c（@iχ）c（x）。 因此，可以得出c（Ei） c（ε），因此所有的公式形式τ Ei发生在 也将是根公式的c-子公式。Q另一方面，下面的引理在HPA的情况下更容易证明。引理4.5对于所有出现在Θ上的表分支Θ和前缀σ，TΘ（σ）是有限的。证据从引理4.4可以得出TΘ（σ）是Θ的根公式的所有c因此引理如下，如果我们可以证明对于所有公式，ε的c-子公式的集合是有限的。 这个证据 类似于引理3.6的证明，但更容易，因为公共公告算子不像动作模态那样复杂。Q我们现在延长订购时间 上一节介绍的Θ 设Θ为 一个场景分支如果一个前缀τ被引入到分支中，使用一个关于形式为σ θ τ的公式的前缀生成规则，我们说τ由σ生成，记为σΘτ。在这种情况下，引理3.9终止的其余证明与定理5.4的证明相同，[4]的文件。 唯一的区别是他们的拟子公式的概念必须被我们的c-子公式的概念所因此，我们得到：定理4.6任何使用给定HPA规则构造的表都是有限的，因此逻辑HPA是可判定的。4.2HPA表系统的可靠性和完备性同样，对于AM，可靠性的证明很简单。其完整性也几乎与[4]相同。唯一需要修改的是，因为名词在HPA中只表示部分。对于AM的表系统，讨论了约简公理规则。给定开放饱和分支Θ，Θ= WΘ，RΘ，VΘ 构造如[4]所示：WΘ= {σ|σ是Θ上的一个原函数}RΘ={（σ，uΘ（τ））∈ WΘ×WΘ|σ Raτ发生在Θ上}VΘ（x）= {uΘ（σ）∈ WΘ|对于所有的x ∈ PROPNOM，σx发生在Θ}上。为了使V定义良好，我们必须确保VΘ（i）1对于所有名词I. 如果有两个不同的urfatherσ和τ和一个nominali，使得σi和τi都发生在Θ上，那么使用分支的饱和度和规则（Id），我们将得到TΘ（σ）=TΘ（τ）。然而，由于他们都是urfather，这将意味着σ=τ，这是一个矛盾。V是一个很好的定义。现在，完整性由定理得出：定理4.7设Θ是表系统的开饱和分支。对于任何出现在Θ上的公式σ ∈，以σ为原函数，我们认为M Θ，σ |= 0。158J. U. Hansen/Electronic Notes in Theoretical Computer Science 262（2010）141¬¬¬¬¬¬¬¬¬证据 证明是通过归纳法来进行的。基本情况由VΘ的定义得出。 情形如[4]中所示：=Ka，=Ka，=E，=E，=@i。在=@ i的情况下，需要做更多的工作。假设σ@i出现在Θ上，并且σ是一个原父。然后通过规则（@）的闭包，Ei或τi和τ树枝上发生了一场火灾。 在第一种情况下，不可能有一个前缀σJ使得σJi在Θ上。这是因为规则E给出了σJi也在Θ上，这与Θ是开分支的假设相矛盾。 但是在M Θ中不可能有态，i表示。因 此 ，通过语义M Θ，σ| =@ i. 如果，在一个条件下，τi和τ <$i在Θ上，则通过urfather闭包，u Θ（τ）i和uΘ（τ）<$i也在Θ上，根据归纳假设，M Θ，uΘ（τ）|= i和MΘ，uΘ（τ）|=。 因此，我们得到M Θ，σ |=@ i.Q作为这个的结果，我们得到那个。定理4.8图2的表系统对于逻辑HPA是可靠的和完备的。5结论意见和进一步研究在本文中，我们提出了两个表系统，一个动态认知逻辑与行动模型和一个混合公告逻辑（都没有共同的知识）。这些都是基于已经存在的tableau系统，我们简单地添加对应于两个逻辑的归约公理的tableau规则。在此之后，我们证明了[4]中用于证明终止性的方法也可以扩展到
