动态认知逻辑：tableau方法与DEL序列的理论计算机科学电子笔记

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）17-30www.elsevier.com/locate/entcsTableau方法与DEL序列Guillaume Aucher纪尧姆·奥歇1，2伊瑞莎INRIA - University of Rennes 1雷恩，法国BastienMaubert3FrancoisSchwarzentruber4伊瑞莎ENS CachanRennes，法国摘要动态认知逻辑（DEL）处理多智能体和动态环境中的情况表示它可以以统一的方式表达关于以下内容的声明：(i) 初始情况(ii) 在这种情况(iii) 事件发生后的结果是什么。在证明了我们可以推断的关于（ii）的给定（i）和（iii）以及我们可以推断的关于（i）的给定(ii)和（iii）都可约化为我们可以推断的关于（iii）的情况，给定（i）和（ii），我们提供了一个tableau方法来决定这样的推断是否有效。我们实现了它在LOTREC计划，并证明了这个决策问题是NEXPTIME完全的。这有助于DEL的证明理论和计算复杂性的研究，而一直被忽视。保留字：动态认知逻辑，tableau方法，计算复杂性1引言动态认知逻辑（英语：DynamicEpistemic Logic）（DEL）处理知识和信念变化的多主体环境中的逻辑研究，以及更一般的信息变化。为了解释这些逻辑动态，DEL的核心思想是将1我们感谢Sophie Pinchinat的有益讨论和三位评论者的评论。2电子邮件：guillaume. irisa.fr3电子邮件：bastien. irisa.fr4电子邮件：francois. bretagne.ens-cachan.fr1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.00318G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17将智能体的信念表示因此，可以在DEL语句的逻辑框架内统一表示：(i) 关于初始情况的真实(ii) 在这种情况下发生的事件的真实性(iii) 事件发生后的结果是什么从逻辑的角度来看，这种分裂回避了以下三个问题。给定（i）和（ii），我们可以对（iii）推断出什么？给定（i）和（iii），我们可以推断（ii）什么？给定（ii）和（iii），关于（i）我们可以推断出什么？提供可用于回答这些问题的正式工具肯定会引起人类或人工智能的兴趣。事实上，他们不仅可以用它们来计划自己的行动以实现给定的认识目标（第一和第二个问题实际上分别对应于情境演算中的演绎和溯因计划问题），而且他们还可以用它们来解释和确定导致给定情境的后验原因。然而，为了适用，这些正式工具应导致可执行的决策程序。为此，我们提供了一个tableau方法来回答第一个问题。这是足够的，因为我们证明了另外两个问题实际上都可以形式上还原为第一个问题。本文的结构如下。在第2节中，我们定义了对应于上述三个问题的三个DEL-序列，并且我们证明了这些DEL-序列是可互定义的。在第3节中，我们提供了两个终止，健全和完整的tableau方法。这使我们在第4节中定义了NEXPTIME中的一个算法，我们通过减少已知的平铺问题来证明它是最优的。我们的决策问题是NEXPTIME完全的。在第5节中提供了一个在LOTRECscheme中实现我们的tableau方法的链接。最后，我们在第6节中通过讨论相关的工作来结束。2动态认知逻辑：DEL-sequents2.1初始状态的表示：L-模型在本文的其余部分，Φ是一组可数的命题字母（可能是无限的），称为原子事实，描述静态情况，而Agt是一组有限的代理人。L模型是元组M=（W，R，V），其中：• W是可能世界的非空集合，• R：Agt→2W×W是一个函数，它为每个代理j∈Agt分配一个W上的可达性关系，• V：Φ→ 2W是一个函数，它给Φ的每个命题字母分配W的一个子集。函数V称为赋值。G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1719.××对于w∈W，我们记为w∈M，并且（M，w）称为点L-模型（-10的w表示实际世界）。如果w，v∈W，我们写为wR j v，对于R（j）（w，v）和Rj （ w）={v∈W|wRjv}。因此，wRjv意味着在世界上wj认为世界v可能对应于实际世界。然后，我们定义了下面的认知语言L，它可以用来描述和陈述L-模型的属性：L：φ：：=p|¬φ|φ∧φ|Bjφ其中p在Φ上变化，j在Agt上变化。我们定义φ=def），<$Bj<$φ=def<$Bj<$φ。 TesymbolT是p∈Φ的缩写。设M是L-模型，w∈ M，φ∈ L. M，w| = φ的归纳定义如下：M，w| = pi <$w∈ V（p）M，w| = φ i M，w| = φ和M，w|=M， w|=<$φi≠M， w|= φM， w|= Bjφi∈Rj（w），M， v|= φ公式Bjφ读作“age n t j belie v es φ“。它的真值条件以这样一种方式重新定义，即当φ在代理j认为可能的所有世界中成立时，代理j相信φ2.2事件的记录：L×-模型描述事件的命题字母p×n称为原子事件，其范围在e r Φ × = { p ×n范围超过L}。p×n的读数是“前提条件n发生的一个事件”。L×-模型是元组M×=（W×，R×， V×），其中：• W×是可能事件的非空集合，• R×：Agt→2W′×W′是一个函数，它赋予每个智能体j∈Agt一个W上的可达性关系，• V×：Φ×→ 2W′是一个函数，它给Φ×的每个命题字母分配W×的一个子集，使得对所有w×∈W×，至多有一个p×n，使得w×∈V（p×n）（排他性）.对于w× ∈ W × ， 我 们 设 w ×∈M×，d（M×，w×）称为点L×-模型（w×常表示实际值）. 若w×，v×∈W× ， 则 对 R× （ j ） （ w× ， v× ） ， w ∈ w × Rj × v × ， 且 Rj× （ w× ）={v×∈W×|w×Rj×v×}。 v×∈Rj （w×）是指当w表示的可能事件发生时，智能体j认为yv×表示的可能事件实际上发生的可能性。 我们对L×-模型的定义等价于在[ 3 ]的逻辑框架中对动作签名的定义。[5]正如我们为L-models定义了语言L，我们也为L×-models定义了语言L×L×：φ×：：=p×φ |¬φ×|φ×∧φ× |Bjφ×5If=（W′，R′，（w1′， . ，wn′））是动作签名，并且φ1， . ，φn∈L，则L′-模为（n，φ1， . ，φn）是元组M′=（W′，R′， V′），其中V′（p′n） ={wi′}，如 果 n=φi，V′（p′n） ={w1′， . ，wn′}，否则V′（p′n）=n.20G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17.L⊗ ⊗ ⊗×∈ L其中，p×n的范围超过Φ×={p×n且joverA gt. 在文献[ 5 ]中，L×W被引入. 其次，对于L×的模，都用引号×来表示，而对于L ×的模，则不一样。语言L ×的真值条件与语言L的真值条件相同。L∈M×是一个L×-模型，w×∈M×，φ×∈L×. M×，w×|=φ×的定义如下：M×，w×|=p×iw×∈V×（p×）M×，w×|=<$φ×i≠M×，w×|=φ×M×，w×|=φ××iM×，w×|=φ×和M×，w×|=×M×，w×|=Bjφ×i，对于所有v×∈Rj（w×），M×，v×|=φ×2.3按事件更新初始情况：产品更新一个×-模型导出了一个前提函数的定义。可能事件w×的前提条件Pre（w×）对应于应该为真的性质在一个L-模型的世界w上，使得可能的事件w×可以在这个世界w中“物理地”发生。条件函数Pre：W×→ Li由L×-模型M×导出 =（W×，R×， V×）定义如下：Pre（W×）=P如果存在p×∞，使得M×，W×|=p×n;Pre（w×）=T，否则。然后，我们在[ 4 ]的BMS产品更新设置中等效地重新定义如下。 设（M，w） =（W，R，V，w）是 一个L×-模型，（M×，w×） =（W×，R×， V×，w×）是一个L×-模型，满足M， w|=Pre（w×）。（M，w）和（M×，w×）的生成日期是有限L-模型（M×M×，（w，w×））=（W，R，V，（w，w）），定义如下：• W={（v，v×）∈W×W×|M， v|= Pre（v×）}，• Rj<$（v，v×）={（u，u×）∈W<$|u∈Rj（v）anddu×∈Rj×（v×）}，•V（p）={（v，v×）∈W|M，v| = p}。本文给出了一个新的L-模型（M，w）→（M×，w ×），它描述了在y （ M × ， w ×）所代表的事件发生之后，年龄n如何感知先前由（M，w）所代表的新情况.2.4我们的DEL序列设φ、φ××和φ××。我们定义逻辑结果关系φ，φ×φ××、φ、φ××2φ×和φ×、φ××3φ如下。第二种和第三种关系可分别用于认知规划和目标回归φ，φ×φ××i∈L ×-模del（M×，w×），且L×-模del（M×，w×）满足M， w|= Pre（w×），M， w|= φ和M×，w×|=φ×，则（M，w）<$（M×，w×）|= φ××φ、φ××2 φ×i∈L-模（M，w），（M× ×，w× ×），使得M， w|=φ和M× ×，w××|=φ× ×，若（M×，w×）是L×-模上一个点，则M， w|=Pre（w×）and（M，w）<$（M×，w×）与（M× ×，w× ×）双相似，则M×，w×|=φ×G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1721φ×、φ××3 φi∈L×-模del（M×，w×），且L-模del（M× ×，w× ×）满足M×，w×|= φ×和M× ×，w××|= φ× ×，如果（M，w）是一个点L-模型，使得M，w| = Pre（w×）and（M，w）<$（M×，w×）与（M× ×，w× ×）双相似，则M， w|=φ事实上，正如下面的命题所表明的，我们的三个DEL-S是可以相互定义的。因此，在本文的其余部分，我们将只关注于为DEL-ψφ，φ×φ××提供一个tableau方法。其他DEL序列的Tableau方法和复杂性结果可以很容易地从为这个DEL序列提供的方法和复杂性结果中改编。命题2.1对于lφ，φ××∈L和φ×∈L×，φ、φ××2 φ×iφ，<$φ× <$φ××φ×，φ××3 φi<$φ，φ× <$φ××3Tableau方法我们考虑了三个模型，φ∈L，φ×∈L×和φ××∈L，并解决了φ，φ×是否为|= φ××成立。 为此，我们等价地判定是否存在一个局部L-模del（M，w）和一个局部L×-模del（M×，w×），使得M， w|=Pre（w×），M， w|=φ，M×，w×|=φ×且M<$M×，（w，w×）|=<$φ× ×。我们把这个对偶问题称为满意度问题。3.1Tableau方法描述出现在我们的tableau方法中的公式，我们称之为tableau公式属于以下类型：• （l φ）：l是标签lw（resp. lw′），其表示模型M的世界（相应地，M×），φ是L（resp. L×），在M， w（相应地）处应为真。 M×，w×）。• （lwlw′φ× ×）：lw表示M的一个世界w，lw′表示M×的一个世界w ×，dφ××是L的一个在M<$M×，（w，w×）处为真的公式. （lwlw′0）表示（w，w×）不在M∈M×中.• （Rll×）（resp. （R×ll×））：R（resp. R×）是一些Rj（resp. Rj×），l和l×分别代表两个世界w和u（ w×和u×），则wRju（分别为 w×Rju×）。• ：表示不一致。表规则由一行上方的分子N和一个有限的冷却器D1，.，Dk在这条线之下，由竖线分隔：D1|.N. . |DK分子和分母是有限的表式集合。一个三元组（φ，φ×，φ××）的tableau是一个有限树，在每个节点上有一组tableau公式，其根是：Γ0={（lwφ），（lw′φ×），（lwlw′φ××）}22G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17⊥一个具有分子N的规则适用于一个带有集合Γ的节点，如果Γ包含N的一个实例。如果没有适用的规则，则称Γ饱和。 我们称一个节点n为端节点，如果它所携带的公式集合Γ是饱和的，或者如果n ∈Γ。 该画面按以下方式扩展：(i) 选择一个携带Γ的叶节点n，其中n不是端节点，并选择一个规则p适用于n。(ii) (a)如果ρ只有一个分母，则将适当的实例化添加到Γ。(b)如果ρ有k个算子，k >1，则为n创建k个后继节点，其中每个后继节点i携带Γ与分母Di的适当实例化的并集。画面中的分支是从根节点到结束节点的路径。 如果分支的结束节点包含，则分支是关闭的，否则分支是打开的。如果一个tableau的所有分支都是闭合的，则它是闭合的，否则它是开放的。一个三元组（φ，φ×，φ××）称为相容的，如果（φ，φ×，φ××）没有一个表是封闭的，而一个三元组（φ，φ×，φ××）是一个定理，我们写为φ，φ×φ× ×，如果存在（φ，φ×，<$φ× ×）的闭表。3.2Tableau规则M、M×和M××（l是lw、lw′或lwlw′）的通用规则（l φ）（l<$（φ））<$（l<$$> φ）<$（l p）（l<$p）（l φ）（l φ）（l<$φ）|（l<$）（lφ）⊥其中p∈ΦM和M×（l是lw或lw′）的S特殊规则（l<$Bj<$φ）<$B<$（lBjφ）（R ll×）B（lw′p×φ）（lw′p×φ）（Rl l×）（l×φ）j（l×φ）j不包括⊥其中φ/=φ适用于M××的特殊规则：（lwlw′<$Bj<$φ）<$B<$（lwlw′Bjφ）（Rlwlu）（R×lw′lu′）B⊗（R1）l）（R×l′l′）（lJl′φ）（l l′ φ）|（l）Jl′0）（lw lw′p）←1（lw lw′<$p）←2（lw p）（lw lw′0）（lw′p×n）（lw<$p）（lw lw′φ）（lw′p×φ）（lw上一页1¬ψ)（lw （1）前2其中φf= 0注3.1另一个合理而完整的表格方法可以通过用以下规则代替上述规则Pre1（lw lw′0）前×（lw′p×1）（lw<$1）|.. . . . . 你 好 。 . |（lw′p×n）（lw<$n）WuWuuuuuu⊗u1G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1723其中p×n1， . ，p×n是在表的底部的φ×中出现的比例字母的集合第二种tableau方法更加模块化，从某种意义上说，如果我们移除Rule（Excl），则所得到的tableau方法在语义方面仍然是合理和完整的，其中我们没有对L×-models施加（Exclusivity）条件。还要注意的是，用这种表方法从一个非线性方程组中得到的L-模型和L×-模型不需要像用第一个表方法证明命题3.3那样，被3.3Tableau方法的可靠性和完备性命题3.2（Tableau方法可靠性）对于所有φ，φ××∈ L，对于所有φ×∈L×，φ，φ×φ××隐含φ，φ×φ××证据而不是证明φ，φ×<$φ××意味着φ，φ×|= φ××，等价地证明了φ，φ×$φ××蕴涵φ，φ×b φ××。设存在一个点L-模型（M，w），一个L×-模型（M×，w×）满足M，w|=φ，M×，w×|=φ×，M， w|=Pre（w×）anddM<$M×，（w，w×）$φ× ×。我们必须证明（φ，φ×，<$φ××）的每一个表都有一个开分支（终止性的证明推迟到第4节）。我们说一个表公式集合是可解释的，如果存在一个L-模型M， 一个L×-模型M×，f：LABEL→W和f×：LABEL' → W ×（其中LABEL和LABEL'是表公式中表公式的集合），使得（M，M ×，f，f ×）使得表公式中的所有表公式对下列语义为真|= T：（M，M×，f， f×）|=T（lwφ）i<$M， f（lw）|=φ（M，M×，f， f×）|=T（lw′φ×）i<$M×， f×（lw′）|=φ×（M，M×，f， f×）|=T（Rlwlu）if（lw）Rf（lu）（M，M×，f， f×）|=T（R×lw′lu′）if×（lw′）R×f×（lu′）（M，M×，f， f×）|=T（lwlw′0）i <$M， f（lw）$Pre（f×（lw′））（M，M×，f， f×）|=T（lwlw′φ× ×）i<$M， f（lw）|=Pre（f×（lw′））和M<$M×，（f（lw）， f×（lw′））|=φ××（M，M×，f， f×）|=Tifalse注意，由于φ，φ×$φ××，集合Γ0={（lwφ）（lw′φ×）（lwlw′<$φ×）}是不可解释的。此外，如果一组公式是可解释的，则它不包含- 是的因此，如果我们证明，当一个规则的分子是可解释的，其中一个解释者也是，那么我们已经看到，每一个表（φ，φ×，<$φ ×）有一个openbran ch。我们为M××的特殊规则提供了它，其他规则的提供是标准的。下面，当f是一个函数时，我们让f（x→a）是将x映射到a和将y映射到f（y）的函数，如果y f=x。规则Bj：IfM，M×，f， f×|=T（lwlw′<$Bj <$φ）tenM<$M×，（f（lw）， f×（lw′））|={\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0} 所以存在（u，u×）∈W××，使得（f（lw）， f×（lw′））R× ×（u，u×）andd M∈M×，（u，u×）|=φ。 Since（f（lw）， f×（lw′））R× ×（u，u×）具有f（lw）Ru，f×（lw′）R×u×和M，u| = Pre（u×）。因此，通过令g：= f（l u′ →u）和g×：= f×（l u′→u×），我们有M，M×，g，g×|=T{（Rlwlu）（R×lw′lu′）（lulu′φ）}。24G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17规则Bj：IfM，M×，f， f×|=T{（lwlw′ Bjφ）（Rlwlu）（R×lw′ lu′）}则男、 女（女）|=Pre（f（lw′）），M<$M×，（f（lw）， f×（lw′））|=Bjφ，f（lw）Rf（lu）anddG. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1725.其中Sw′和δSw′定义如下。设Sw′={w∈ M（lw0lw′φ）∈Γf∅f×（lw′）R×f×（lu′）。所以，要么M， f（lu）$Pre（lu′）要么M， f（lu）|=Pre（lu′）。 在第一种情况下，M，M×，f， f×|=T（lulu′0）。 在第二种情况下，（f（lu）， f×（lu′））是M××的世界，且（f（lw ）， f×（lw′））R× ×（f（lu）， f×（lu′））. 因此，我们有M<$M×，（f（lu）， f×（lu′））|=φ，因此M，M×，f，f×|=T（lulu′φ）规则<$1和规则<$2 ：IfM，M× ，f ， f×|=T{lwlw′p}则M， f（lw ）|=Pre（f（lw′）和M<$M×，（f（lw）， f×（lw′））|=p。 设V× ×（f（lw）， f×（lw′））=V（f（lw）），则M， f（lw）|=p，因此M，M×，f， f×|=T{（lwp）}。 Rule←2类似地被提供。规则前1和前2：IfM，M×，f， f×|=T{（lwlw′φ）（lw′p×φ）}，其中φ=0，则M， f（lw）|=Pre（f×（lw′）），且f×（lw′）∈V×（p×V）. 所以M， f（lw）|=Pre（p×），且M，M×，f， f×|=T（lw）。 对于规则前1，ifM，M×，f， f×|=T{（lwlw′0）（lw′p×n）}，则通过定义|=T，M， f（1w）|=<$Pre（f（lw′）anddM×， f（lw′）|=p×。 因此，根据（排他性）条件，Pre（f（l w′））=π，因此M，f（l w）|=<$，即（l w<$）。Q命题3.3（Tableau方法完备性）对于所有φ，φ××∈ L，对于所有φ×∈L×，φ，φ×φ××隐含φ，φ×φ× ×。证据 证明了φ，φ×b φ××蕴涵φ，φ×$φ××。 设（φ，φ×，<$φ× ×）有一个表，它有一个 约束ch， 我 们 证明存在一个 局部L-模型（M，w）和一个局部L×-模型（M×，w×），使得M， w|=Pre（w×），M， w|=φ，M×，w×|=φ×且M<$M×，（w，w×）|=<$φ× ×。设Γf是开分支的端点所携带的表公式集我们定义M和M×如下。每一步都是分两步完成的。• 设M0=（W0，R0，V0），其中W0={w|（ lw ∈）∈Γ f}， V0（p）={w|（lwp）∈Γ f}和R0={（w，u）|（Rlwlu）∈ Γ f}. 然后我们定义了点L-模型（M，w）作为f（M0，w0）的二分逼近. 6• 设M× =（W×，R×， V×）withW× ={w×（lw′）∈ Γf}，V（p×Ω）={w×|（lw′p×n）∈Γf}，且dR×={（w×，u×）|（R×lw′lu′）∈Γf}. 更多，更多w×∈M×such，不存在（lw′p×ε）∈Γf，w∈V×（p×δS.）如果Sw′ ，′对于φ1=0且w0∈w}. TenδSw′=w∈Sw′其中δ（M，w）是（M，w）的特征公式。 注意，根据规则（不包括）的合理性，M×满足排他性条件。最后，我们将M××定义为M×M×（我们将给出一个关于M， w|=Pre（w×））。下面的引理3.4和3.5建立了我们的tableau方法的完备性。Q引理3.4若（lw0φ）∈Γf则M， w|=φ，andd如果（lw′φ×）∈Γf则M×，w×|=φ×。是的。 我们只对M给出了它，对M ×也是类似的. 我们首先为M0提供它。 由于M0和M是双相似的，因此将结果传递给M. 证明已经完成6形式上，M =（W，R，V），其中W =vv与wwW双相似，R=（w，v）W26G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17{{|0}。 0 ∈0}{∈..W×W，有w0∈w和v0∈vsuch，使得v0∈R（w0）}和V（p） ={w∈W，有w0∈wsu ch使得w0∈V0（p）}. 我们写w为w0的w的集合，其中w0是双相似的。G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1727通过对φ的归纳。p，<$p：根据V的定义。对于φ φ 0 φ的情形，通过规则φ 0的饱和，Γ f也包含（lw0φ）和d（lw0φ）. 通过归纳得出：M0，w0|=φ和M0，w0|=0，soM0，w0|=φ情况φ类似地给出。<$Bj<$φ：通过规则<$Bj<$的饱和，存在lu0 满足（Rlw0lu0）∈Γf和（lu0φ）∈Γf.通过归纳得出结论M，u0|=φ，andw0Ru0由M0，soM0，w0的约束成立|=Bjφ。Bjφ：设m∈u0在W0中成立，若w0Ru0成立，则M0，u0|=φ，并得出结论，M0，w0|=Bjφ。通过对M0的证明，我们可以进一步认识到（Rlw0 lu0）在Γ f中. 因此，通过规则Bj的饱和，（lu0φ）也属于Γ f，并且通过归纳假设M0，u0|= φ。Q引理3.5If（lw0 lw′φ× ×）∈Γf，其中φ×× f=0，|=P re（w×）和M<$M×，（w，w×）|=φ××。证据 我们首先证明以下事实：F act 3.6若（lw0lw′φ）∈Γf，其中φf=0，则m∈M， w|=P re（w×）。假设M，w$Pre（w×）。于是有两种情况：要么存在（lw′p×n）∈Γf，要么不存在（ lw′p×n）∈Γf。在第一种情况下，M0，w0$，因为根据（排他性）条件，= Pre（w×），因此M，w$。然而，根据规则Pre 2，（l w0 f）∈Γf. 然后，根据引理3.4，M，w| = 0。 这不可能在第二种情况，由于（lw0 lw′ φ）∈ Γ f，对φ0，我们有M，w |= δ Sw′。此外，M×，W×|=p×δS也不可能′ 定义为V×。 因此，M，W| =前（w×）。 这是我们现在可以证明引理3.5。 我们用φ上的归纳法证明了这一点。p，<$p：根据规则<$1，（l w0p）∈Γ f，因此M，w|P = Lemma 3.4此外，通过Fact3.6，M， w|=Pre（w×）。因此，M<$M×，（w，w×）|=产品更新的定义。p的证明与p的情况类似。 证明在其他布尔情况中，φ，<$（φ）和<$φ是通过直接应用归纳假设而得到的。如果（lw0 lw′ 的y饱和，（Rlw0 lu），（R×lw′lu′）和（lu0lu′φ）都属于Γ f.现在，通过应用事实3.6，M，w |=前（w×）。此外，通过M和M×的 定 义，u∈R（w）和du×∈R×（w×）. 因此，我们认为，（u，u×）∈R（w，w×）. 此外，（l u0卢 φ）∈Γf和φ0，因此通过应用归纳推理，M， u|=Pre（u×）anddM<$M×，（u，u×）|=φ。因此，我们认为，M， w|= Pre（w×）anddM<$M×|= Bjφ。Bjφ：若（lw0lw′Bjφ）∈Γf，则由Fact3.6的应用，M， w|=Pre（w×）。设（u，u×）∈R（w，w×）.则u∈R（w），u×∈R×（w×）. 则有 u0∈u， suc h，使得 u0∈R（w0），通过M的定义. 因此，通过M和M×的定义，（Rlw0 lu0）∈Γf和（R×lw′lu′）∈Γf. 则由规则Bj的饱和性，（i）（lu0lu′0）∈Γf或（ii）（lu0lu′φ）∈Γf.W28G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17u(i) 在第一种情况下，假设存在（lu′p×n）∈Γf。然后，通过规则Pre1的饱和，（lu0<$l）∈Γf。因此，M，u|由Lemma 3.4得出。这是不可能的，因为M×，u×|=p×m，andndsoM， u|因为（u，u× ）∈M<$M× ， 所 以 也 应 该 成 立 。因此，不 存在（lu′p×n）∈Γf.(a) 如果存在u∈0∈ u，则对于mφ，（lu0<$lu′φ）=/Hy pothesis，M， u|=Pre（u×）anddM<$M×，（u，u×）|=0。0，然后通过诱导(b) 如果不存在u∈u，则（lu∈0 卢 对于φf=0，定义了Su′，u∈/Su′.因此，M， u$δSu′，因为对于M，δSu′恰好刻画了Su′的世界。因此，通过V ×的定义，M，u$Pre（u×），因为M×，u×|=p×δS′。 然而，（u，u×）∈R（w，w×），所以M，u |= Pre（u×）。有矛盾，所以这个案子不可能。(ii) 在第二种情况下，通过归纳假设，M，u| = Pre（u×）和M <$M×，（u，u×）|=φ所以，在 ny的 情况下，M<$M ， （ u， u× ） |=φ。 因此，M<$M× ， （ w ， w× ）|=Bjφ。Q4满意度问题命题4.1满足性问题在NEXPTIME中。证据在3.2节中介绍的tableau规则产生了一个在指数时间内运行的非确定性算法。我们说一个标号lu的深度为k，如果 有一个序列w=u1，.，u k= u，使得（Rl，w，l wi+1）对于所有i和Bj <$ ）。所以当i> δ（φ××）时，在τ ×× / = 0的Γ i中不再有（lulu′<$××）形式的表式。因此当i >δ（φ× ×）时，Pre2，φBj和Bj 规则不再适用.同样地，公式的最大深度分别为：×）在形式为（lu （lu′<$×）随i严格递减。 此⊗G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）1729外，出现在形式为（l u）的表公式中的公式的深度较小30G. Aucher et al. /Electronic Notes in Theoretical Computer Science 278（2011）17i=0.Σ¬则max{δ（φ），maxk∈{1，.，n}δ（φ k）}，且出现在形式为（lu ′ φ×）的表公式中的公式φ ×的深度小于δ（φ×）.最后，ΓN+1=π，并且算法应用规则直到饱和，是，表公式集NΓi是饱和的。现在让我们看看执行算法所需的时间。设x为输入的大小，即φ、φ×、φ××和Pre（pk）的大小步骤1饱和出现在Γi中的表公式中的世界u，u×和（u，u×）。对于每一个世界，饱和度在x上都是线性的。步骤3为出现在Γ × i中的每个B j-公式创建新的tableau公式。对于一个新的单词，它最多会产生2个新单词。 如果我们注意到yi是Γ i中的最大w数，则我们有yi+1=2x yi。 Soyi=（2x）i。所创建的world的数目由y（2x）x+1绑定，并且该构造花费指数量的时间。Q为了证明满足性问题的NEXPTIME-困难性，我们将把一个NEXPTIME-完全平铺问题归结为它[6]。k是自然数。图块类型t是颜色t =（左（t）、右（t）、上（t）、下（t））的4元组。我们考虑的平铺问题定义如下。• 输入：瓦片类型的有限集合T，at0∈T和以其二进制形式书写的自然数k• 输出：是的，我们可以平铺一个k×k网格，将T和t0放置在（0， 0）上。在其他世界中，问题是决定是否存在函数τ，{1，. k}2至T满足以下约束：(i)τ（0， 0）=t0;(ii) up（τ（x，y））= down（τ（x，y + 1））对于所有x∈ {1，.，k}，y∈{1，...，k− 1};(iii) right（τ（x，y））= left（τ（x + 1，y））对于所有x∈ {1，.，k− 1}，y∈{1，...， k}。命题4.2满足性问题是NEXPTIME困难的。证据不失一般性，我们可以假定k=2n。让我们考虑平铺问题的一个实例（T，t0，k） 我们现在定义三个公式φ，φ×，φ××，它们可以在多项式时间内计算，|不|和n，使得可以将a在（0， 0）i ∈（φ，φ×，φ××）上放置T和t0瓦片类型的k×k有一个长度为O（n2）的模态公式χ，它在一个框架i中得到满足，该模型包含一个深度为2n的二叉树作为子模型，例如：χ=l<2nBjl（<$Bj<$pl<$$>Bj<$$>pl）<$i

下载后可阅读完整内容，剩余1页未读，立即下载