基于On-the-y表的PDL满意度决策算法研究

∪∗理论计算机科学电子笔记231（2009）191-209www.elsevier.com/locate/entcs基于On-the-y表的PDL满意度PietroAbatea，1，RajeevGor'ea，2和FlorianWidmannb，3，4澳大利亚国立大学计算机科学实验室，堪培拉，澳大利亚b澳大利亚国立大学和NICTA计算机科学实验室和逻辑计算方案摘要我们提出了一个基于表格的算法，用于确定命题动态逻辑（PDL）的满足性，该算法构建了一个具有祖先循环的有限根树，并将额外的信息从子循环传递到子循环，以在回溯过程中分离好循环和坏循环它很容易实现，具有并行化的潜力，因为它通过独立地探索每个tableau分支来构建“在后台”的伪模型但它的最坏情况行为是2EXPTIME而不是EXPTIME。TWB（http://twb.rsise.anu.edu.au）中的原型实现是可用的。关键词：命题动态逻辑，自动推理，表演算，决策过程1介绍命题动态逻辑（Propositional Dynamic Logic，PDL）是一种用于程序推理的逻辑[14，9]。它的公式由传统的布尔公式加上“动作模态”组成，这些动作模态是由一组有限的原子程序使用顺序组合（;）、非确定性选择（）、重复（）和测试（？）构建的。PDL的可满足性问题是EXPTIME完全的[15]。与具有表现出良好的平均情况行为的算法的EXPTIME完全描述日志不同，从理论（可靠性和完整性）和实践（平均情况行为）的角度来看，PDL满足性的决策程序都不令人满意，如下所述PDL的最早决策程序是由Fischer和Ladner [9]和Pratt [15]提出的。Fischer和Ladner的方法是不切实际的，因为它首先构造了1电子邮件：Pietro. pps.jussieu.fr2电子邮件：Rajeev. rsise.anu.edu.au3电子邮件：Florian. rsise.anu.edu.au4澳大利亚国家信息和通信技术中心由澳大利亚政府通信、信息技术和艺术部以及澳大利亚研究委员会通过支持澳大利亚能力和信息和通信技术卓越中心方案提供资金1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.02.036192P. Abate等人理论计算机科学电子笔记231（2009）191给定公式的所有子公式的集合的所有相容子集的集合，在所有情况下总是需要指数时间。另一方面，Pratt [15]本质上构建了一个多遍（稍后解释）tableau方法。其他定点逻辑的大多数后续决策过程，如命题线性时态逻辑（PLTL）[18]和计算树逻辑（CTL）[5，8]可以追溯到Pratt在这些多遍过程中，第一遍构造包含公式集的节点的根tableau，但是如果将tableau构造应用于n将复制m，则允许从一个分支上的节点n到不同分支上的（先前构造的）节点m的交叉分支弧。结果是一个潜在的指数大小的循环图（而不是一个循环树，其中m必须是n的祖先）。循环图是一个“伪模型”，因为它可能无法满足钻石式公式（“可能性”）的要求，即“某个公式最终为真”。随后的通道通过修剪不一致的节点和修剪包含“未填充的可能性”的节点来检查虽然有效的模型检测技术可以及时地检测出规模为线性的“伪模型”，但这些多遍方法会不必要地构造出指数规模的循环图。一种解决方案是在构建图时检查“在图上”是否填充了均匀性 我们所知道的PDL 的多遍方法的唯一实现是在LoTRec（www.irit.fr/Lotrec）中，但它不是最佳的，因为它天真地处理了析取。Baader [4]给出了一个基于表的单遍决策过程的描述具有角色定义的逻辑，包括角色的联合、组合和传递闭包：本质上是没有测试的PDL他的方法使用PDL运算符的语义构造了一个（循环树）为了区分“好循环”和“坏循环”，Baader必须决定正则语言的相等性，这是一个PSPACE完全问题，实际上可能需要指数时间。这些问题可以简化为对一个确定性最小自动机中状态的同一性的简单检查，而不是“在初始公式中出现的正正则表达式在预处理阶段[ 4，第27页]中创建。但是由于预先计算的自动机可以是指数级的大小，因此这种替代方案可能不必要地需要指数级的时间。Baader方法在最坏情况下是双指数的。“test”结构对于表达“while”循环是必不可少的，但它在布尔语言和常规语言之间创建了一个相互递归。如何将Baader的方法扩展到“测试 ” ， 对 我 们 来 说 并 不 明 显 。 DLP （ http://www.cs.bell-labs.com/cm/cs/who/pfps/dlp）实现了这种方法，仅限于无测试公式，其中，无测试公式仅适用于原子程序。De Giacomo和Massacci [10]给出了一个最优PDL-满足性测试，使用标记的公式 如 σ ： σ 来 捕 获 “ 可 能 世 界 σ 使 公 式 σ 为 他 们 首 先 给 出 了 一 个 决 定 PDL-satisfiability的NEXPTIME算法，然后讨论了如何使用各种已知的结果来获得一个EXPTIME版本。但没有给出一个实际的EXPTIME算法及其可靠性和完备性证明。Schmidt的NEXPTIME算法的确定性实现P. Abate等人理论计算机科学电子笔记231（2009）191193Tishkovsky和Tishkovsky发现了嵌套恒星的问题，但解决方案即将到来。定点逻辑的其他决策过程使用归结演算，翻译方法，自动机理论方法和博弈论方法：参见[1]推荐信我们知道没有基于这些方法的PDL实现在这里，我们给出了一个完善的，完整的，可终止的PDL决策过程具有以下优点和缺点：One-pass性质：我们的方法构造了一个单根有限树（从叶子到祖先的循环）。由于没有交叉分支边缘，我们可以使用深度优先，从左到右的搜索，在回溯时回收每个分支使用的空间证明：可靠性和完备性的完整初等证明是可用的[2]。易于实施：我们的规则很容易实现，因为我们的表节点包含公式集和一些容易定义的额外信息，这些信息的运算只需要对集合和整数进行基本运算。然而，这些低层次的细节使得规则描述起来很麻烦优化潜力：有可能使用描述逻辑（一次通过）表格的成功技术优化我们的（树）表格[12]。生成反模型的容易性：可靠性证明立即给出了将“开放”画面转换为PDL模型的有效过程易于生成证明：与现有的固定点逻辑的Gentzen演算不同[3，13]，我们的tableau演算给出了一个无切Gentzen风格的演算，具有并行化的可能性：我们的规则独立地构建分支，但在回溯过程中合并它们的结果，从而实现并行实现。Prototype：Tableau Work Bench（www.example.com）中的（顺序）原型实现twb.rsise.anu.edu.au允许通过Web测试任意PDL公式。复杂度：我们的方法具有最坏情况下的双指数时间复杂度。通用性：我们的PDL方法适合于其他定点逻辑（如PLTL [ 17 ]和CTL [ 1 ]）的一类类似的需要进一步的实验工作来确定我们的方法是否可以优化，以使用像声音全局缓存[11]这样的技术来表现出良好的平均情况行为2语义学与欣蒂卡结构定义2.1设AFml和APrg分别是命题原子和原子程序的两个不相交且可数的有限集合。所有公式的集合Fml和所有程序的集合Prg归纳定义如下：(i) AFml和APrg(ii) 如果f，f∈ Fml，那么<$f∈ Fml，且f∈ Fml，且f ∈Fml，且f ∈Fml，且f ∈ Fml，∈Prg(iii) 若α∈ Prg，则<$α <$$> ∈ Fml，[α]<$ ∈ Fml(iv) 如果α∈ Prg且β∈ Prg，则（α;β）∈ Prg且α∈β ∈ Prg且α∈ Prg。194P. Abate等人理论计算机科学电子笔记231（2009）191↔∈/∈¬⟨ ∗ ⟩ ⟨ ∗ ⟩⟨ ⟩ ⟨ ⟩ ⟨/⟩⟨ ⟩ ⟨ ⟩⟨/ ⟩ ⟨ ⟩⟨⟩∈A-公式是任何公式α，a-公式是具有α / APrg的-公式α，a-公式是任何公式 α-是的 FML 是所有 - 公式，Fmla是所有a-公式的集合，并且Fml是所有-公式的集合。蕴涵（）、等价（）和常量Falsum和Verum不是核心语言的一部分，但可以像往常一样定义在本文的其余部分中，让p，q在AFml的成员范围内变化，a，b在APrg的成员范围内变化。定义2.2过渡框架是一个对（W，R），其中W是一个非空的世界集，R是一个将每个原子程序a映射到W上的二元关系Ra的函数。模型（W，R，V）是一个转移框架（W，R）和一个赋值函数V：AFml → 2W，它将每个原子命题p映射到一个世界集合V（p）定义2.3设M=（W，R，V）是一个模型。 函数τM：Fml → 2 W和ρM：Prg →2W×W归纳定义如下：τM（p）：=V（p）ρM（a）：=RaτM（μm）：=W\τM（μ m）τM（）：=τM（）τM（）τM（）：=τM（）τM（）τM（[α] τ）：= {w|v ∈ W。（w，v）∈ρM（α）<$v∈τM（α）}τM（τ ατ）：= {w|v ∈ W。（w，v）∈ρM（α）v∈τM（α）}ρM（α<$β）：=ρM（α）<$ρM（β）ρM（β？）：={（w，w）|w ∈ τM（τ）}ρM（α; β）：= {（w，v）|u ∈ W. （w，u）∈ρM（α）（u，v）∈ρM（β）}ρM（α）：=.（w，v）|k∈N。w0， . ，wk∈W. .w0=wwk=v&i ∈ {0，.，k − 1}。（wi，wi+1）∈ρM（α）对于w∈W和τ∈ Fml，我们记为M，wD<$i <$w∈τM（τ）。定义2.4如果存在一个模型M=（W，R，V）且w∈W使得M，wD≠ 0，则公式f∈ Fml是可满足的。如果不满足，则公式f∈ Fml有效定义2.5公式Fml是否定范式，如果它只出现在命题原子之前。对于每一个Fml，我们通过重复地向内推否定（例如使用德摩根定律）获得否定范式的公式nnf（f我们定义一个函数：= nnf（<$）。我们使用Smullyan因此，如果α（re-β）是第一行中的任何公式模式，则α1和α2（分别为β1和β2）是第二行和第三行中的对应模式命题2.6表1中的所有公式α Participa1<$a2和β Participa1 <$β2都有效。定义2.7一个结构（W，R，L）[对于f∈ Fml]是一个转移标架（W，R）和一个标号函数L：W→ 2Fml，它将每个世界w∈W与一个公式集合L（w）[并且对于某个世界v∈W具有f∈L（v）]相关联。P. Abate等人理论计算机科学电子笔记231（2009）191195∈⟨⟩⟨ ⟩Σ.Σ表1Smullyanαϕ∧ψ[αβ][中文]什么？⟩ϕβ-羟色胺[α;β]α1ϕ[α]βϕϕ⟨α ⟩⟨β⟩ϕ[α][β]βα2ψ[β] β-环己二烯[α][α]ψβϕ∨ψ⟨α ∪β ⟩ϕ⟨α ∗⟩ϕ【什么？】ϕβ1ϕ⟨α ⟩ϕϕϕβ2ψ⟨β ⟩ϕ⟨α ⟩⟨α ∗⟩ϕ∼ψ定义2.8对于给定的f ∈ Fml，（无限）集合pre（f）被定义为：pre（f）：={f ∈ Fml |k ∈ N。 α1，...， αk∈ Prg.=<$α1 <$. {\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}对于所有公式和，公式上的二元关系定义为：~i.下列条件之一为真：• Fml. α，β∈ Prg.&•XFml. α，βPrg. α = αβ χ& = α χ或α χ= β χ• Fml. χ=χ或αχ• ？χ，φ∈ Fml.？=？φ？χ&一般来说，使用表1，“~“将a 你好注意，<$∈ pre（<$）。定义2.9设H=（W，R，L）是一个结构，β∈ Fml是一个公式，β∈ Prg是一个程序，w∈W是一个状态。H中的（ω，β，w）的满填充链是有限序列（w0，ω0），...， （wn，nn）的世界公式对，其中n ≥ 0，使得：• 对于所有0 ≤i ≤n，wi ∈ W，<$i∈pre（n），<$i∈L（wi• w0=w，0=β，n=，且i/=，对于所有0 ≤i≤n− 1• 对于所有0≤i≤n−1，如果对于某个a∈ APrg且χ∈ Fml，则<$i=<$a <$χ，则<$i+1=χ并且wiRawi+1;否则wi~ wi+1并且wi= wi+1。196P. Abate等人理论计算机科学电子笔记231（2009）191每个i都在L（wi）中，链从（w0，β）开始，在（wn，）结束，没有其他wi与配对。公式i，i+1是~-相关的，对应的世界wi，wi+1是相等的，除非i= ax，在这种情况下 i+1= χ和wiRawi+1. 因此，可能性<$β<$$> ∈w 0由<$∈wn填充，且wn是从w0β-可达的。定义2.10一个前Hintikka结构H=（W，R，L）[对于f∈ Fml]是一个[对于f]满足H1-H5（如下）的结构，对于每个w∈W，其中α和β是表1中定义的公式。一个Hintikka结构H=（W，R，L）[对于H∈ Fml]P. Abate等人理论计算机科学电子笔记231（2009）191197⟨ ∗⟩∈⟨ ⟩⟨⟩⟨ ∗⟩⟨ ⟩⟨ ∗⟩联系我们|∈}联系我们⟨ ∗ ∗⟩ ⟨ ∗⟩⟨ ∗ ∗⟩ ⟨ ∗ ∗⟩⟨ ⟩⟨⟩是一个pre-Hintikka结构[对于H2]，另外满足以下H6H1：<$p∈L（w） ⇒ p/∈L（w）H2：α∈L（w）<$α1∈L（w）α2∈L（w）H3：β∈L（w）<$β1∈L（w）或β2∈L（w）H4：a∈L（w） ⇒ v ∈ W。w Rav <&$∈ L（v）H5：[a] n ∈ L（w）n n ∈ W. w Rav ∈ L（v）H6：<$α <$$ > < $ $ > ∈ L（w）<$$>存在H中（<$，α <$，w）的填充链.H3“ 局 部 展 开 ” α 的 定 点 语义 但并不保证最小定点，这需要最终为真。H6公式-已填充。H2捕捉到了[α]的最大定点语义。定理2.11如果存在一个Hintikka结构，则否定范式的公式Fml是满足的。（见[2]）3算法概述为了跟踪未填充的可能性并避免历史从父节点传递给子节点，变量从子节点传递给父节点。我们的算法从包含给定公式φ和一些默认历史值的根开始。它通过PDL的语义，反复应用α-/β-规则对公式进行分解，从而生成一棵树。 α的β-规则有一个左子项，它通过将它还原为α来满足这个可能性，而一个右子项，它通过将规则修改历史和变量适合其预期用途。但是，将α-/β-规则简单地应用到像带有嵌套星的公式中，可能会导致“在一个世界”的循环：例如a一个解决方案是使用历史来减少一个特定的α公式，直到α成为原子，通过强制规则集中在这个任务上，并阻止先前减少的钻石和盒子，如果它们导致“在一个世界”的循环。 应用当所有未阻塞的叶子只包含原子、被否定的原子，并且所有非阻塞公式和所有[]-公式只从最外层的原子程序开始时，α/β对于每个这样的叶节点l，并且对于每个这样的公式 b.在l，- 规则创建后继节点，包含 ξΔ，其中Δ = ψ[b]L. 然后，这些后继节点被饱和以使用α和β规则产生新的叶子，并且-规则创建这些新叶子的后继节点，等等。如果不加检查，这个过程可以产生无限个分支，因为相同的后继者可以在同一个分支上一次又一次地创建。为了获得终止，-rule创建一个包含ξ对于l，Δ仅当这个后继者尚未在当前分支的较高位置创建198P. Abate等人理论计算机科学电子笔记231（2009）191{}⟨ ∗⟩⟨ ∗⟩ ⟨ ∗⟩⊆∈⊥⊥/⟨ ∗⟩∗因此，如果后继分支已经存在，则当前分支被因为万一发生的事情α可能会拖延，所以α永远不会被填满。 为了跟踪这种潜在的未填充的可能性，我们通过变量uev将阻塞节点的高度分配给对（，），只要的分解。在回溯过程中，我们的规则特别地，如果它跟踪的可能性可以在以该节点为根的子表中填充，则uev条目在该节点处变为未定义的相反，如果一个高度为h的节点接收到一个值至少为h的uev条目，那么这个uev条目所跟踪的可能性绝对不能被填充，所以这个（阻塞）节点的父节点是不满意的。如果根的状态为“open”，则初始公式φ是可满足的。由于4PDL的一遍Tableau算法定义4.1表节点x的形式为（Γ：：Hcr，Nx，BD，BB：：stat，uev）其中：Γ是一组公式; Hcr是一个对列表（Hcr，Δ），其中Δ是一组公式和Hcr Δ; Nx是一个或一个被指定为应用于x的规则的主公式的公式; BD是“B锁定的Diamonds”的集合; BB是“B锁定的Boxes”的集合; stat具有unsat、open或barried中的一个值; uev是从Fml Hcr × Fml Hcr到N > 0（正自然数）的偏函数。定义4.2公式集Γ Fml和历史Hcr，Nx，BD，并且BB是具有根（r：：HCr，Nx， BD， BB：：stat， uev）的表节点的树，其中节点x的子节点通过规则对x的单次应用而获得（即，仅一个规则可以应用于节点），但是其中父节点可以从子节点继承一些信息。如果一个tableau的每个节点都有一条规则，那么这个tableau就是展开的。在tableau的任何分支上，一个节点t是一个节点s的祖先，它位于从根到s的唯一路径上的s之上。列表HCr是用于检测前级循环并保证终止的历史。如果Nx=，则主公式的选择是自由的，但否则被预先确定为Nx中的公式。当父级中的菱形公式被分解为FML A在子节点中，我们将子节点的Nx值设置为以确保接下来分解该对象。与历史BD和BB一起，这允许我们阻止α-公式和[α]-公式创建“在一个世界”的循环。变量stat和uev的值由节点的子节点确定。形式上，stat=unsat at nodex，如果x是绝对不满足的。 非正式地说，如果节点x的所有后代都不满意或导致“at a world”循环，则stat=barred。最后，stat=open表示该节点可能是可满足的，但由于它可能在循环中，因此我们只能稍后确定为我们回溯到根。定义4.3部分函数uev：Fml × Fml-N>0是对所有公式对都未定义的常数函数：即 2001年，2002年。uev（1，2）=。P. Abate等人理论计算机科学电子笔记231（2009）191199⎨⎨联系我们⟨⟩⊥⟨⟩{} ···{}···2⟨∗⟩∧你好，部分函数Nxtst：Fml- Fml和BDtst：Fml× 2Fml- 2Fml为：Nxtst（χ）：=χχ，如果χ∈Fml，则为χ/a否则，BDtst（χ，Γ）：=<$Γifχ∈Fml<$/a<$很抱歉，否则。当被测试的公式不是-formula，或者是-formula但其程序是原子的时，函数Nxtst返回函数uev跟踪未填充事件：如果uev（χ1，χ2）=h=，则当我们回溯到“高度”h时，与χ1和χ2相关的潜在未填充事件将得到解决如果一个节点有stat =unsat或stat =barred，那么它的uev是不相关的，所以它被任意设置为uev。4.1规则我们用Γ和Δ来表示公式集，并记为1，. . .，Δn，Δ 1，.，Δ m对于分区<$1<$nΔ 1Δm的公式在一个节点。为了节省空间，我们经常忽略从父节点/子节点传递到子节点/父节点的历史/变量。大多数规则只有在一些附带条件成立时才适用，而且大多数规则都涉及向下改变历史或向上改变变量的行为。第4.4节有两个例子。终端规则。（id） （Γ：：·· ·：：stat， uev）{p，<$p}<$Γ对于某些p∈ AFml针对（id）：stat：=unsat和uev：= uev的操作。（Γ：：NxBD：：statuev）（）Nx ∈ {，}∈ BD针对（2）：stat：=barred和uev：= uev的操作。一个id节点显然是不能令人满意的。 由于主公式的2-规则在BD中，它会导致一个“at a world”循环，所以这个规则会终止当前分支。注意，这两个规则都可以适用于节点。线性（α）规则。（）下一页（，：：Nx：：uev）（x，y，r：：Nx：：uev1）（[; ]） （[α;β]π， Γ：：Nx：：uev）（[α][β]π， Γ：：Nx：：uev1）公共边条件：Nx = 0。200P. Abate等人理论计算机科学电子笔记231（2009）191∪∗（[ ]中） （[ανβ]ν， Γ：：Nx：：uev）（[α]α，[β]β， Γ：：Nx：：uev1）（[ ]）（[αν]ν， Γ：：Nx，BB：：uev）（Γ1：：Nx， BB1：： uev1）公共动作：uev（χ1，χ2）：= ifχ1∈ Γ then uev1（χ1，χ2）elseP. Abate等人理论计算机科学电子笔记231（2009）191201.Σ∗ ∗ ∗∈⟨ ⟩⎪⎨⟨ ⟩⎧联系我们⊥BD1：=B.1.2.针对（[]）的额外操作：Γ1：= if [α BB大多数规则都是标准的，但是对于历史记录来说，因为它们只是捕获表1中的转换。[ ]-规则只是删除[α]如果[α]BB，因为这表明它已经在“这个世界”展开过一次否则，它将捕获[α]通过Prop的固定点性质2.6然后把[α<$]代入BB1。接下来的两个规则有各自的副条件和操作，如图所示。（;）（未显示）（α;β，Γ：：Nx， BD：：uev）（αββ，Γ：：Nx1，BD1：：uev1）Nx ∈{}针对以下方面采取的行动：Nx1：=Nxtst..⟨α⟩⟨β⟩ϕΣΣuev（χ1，χ2）：=如果χ1=α;β，则为α1（α β，χ2）uev1（χ1，χ2），若χ1∈ Γ否则的话（怎么样？ ）（你说呢？（I：：Nx，BD：：uev）（λ，λ，γ：：Nx1，BD1：：uev1）Nx ∈ {\displaystyle{\frac{Nx}，\frac{Nx}？⟩ϕ}行动（行动）（C）：Nx1：= Nxtst（）BD1：=BDtst。B.D.如果χ 1 = χ 2，则v1（χ 2，χ2）为零？⟩ϕuev（χ1，χ2）：=uev1（χ1，χ2） 若χ1∈ Γ否则的话这些规则只捕获表1中的转换，除了历史。如果Nx =，则他们对主公式的选择是自由的，否则就限于Nx中的公式。如果主公式的分解χ是一个a公式，我们把子公式的Nx1设为χ，以保证χ是子公式的主公式.针对uev的动作确保uev（χ1，χ2）（其中χ1是主公式）从子公式中的对应公式继承其值：例如，uev（βα;β，χ2）= uev1（βαβ，χ2）反向跟踪βα;β的分解。此外，uev（χ1，χ2）仅在χ1在父节点中时定义。202P. Abate等人理论计算机科学电子笔记231（2009）191∨⎪⎨BDi：=1Patientswithacutemyocardialinfarction， BD泛分支（β）规则。（）（12，Γ：：Nx：：stat， uev）（UE1，Γ：：Nx：：stat 1，uev 1）|（x2，r：：Nx：：stat 2，uev 2）（[？] ）（[？] ，Γ：：Nx：：stat， uev）（单位， Γ：：Nx：：stat 1，uev 1）|（，Γ：：Nx：：stat 2，uev 2）对（）和（[？]）采取的行动对于i=1， 2：uevJ（χ， χ）：=u∈uevi（χ1，χ2）ifχ1∈ΓNx = 0Nx = 012否则，（）（α1α2，Γ：：Nx， BD：：stat， uev）（α1，Γ：：Nx 1，BD 1：：stat1，uev 1）|（α2，Γ：：Nx 2，BD2：：stat2，uev 2）（）的边条件：Nx ∈{}对于i=1，2，对（）的操作：Nxi：=Nxtst..⟨αi⟩ϕΣΣuevJi（χ1，χ2）：=uevi（uevi（χ1，χ2）如果χ1∈ Γ否则的话（）（α，：：Nx， BD：：stat， uev）（X，I：：Nx 1，BD 1：：stat 1，uev 1）|（α，Γ：：Nx 2，BD 2：：P. Abate等人理论计算机科学电子笔记231（2009）191203stat 2，uev 2）（1）的边条件：Nx∈{}∈/BD204P. Abate等人理论计算机科学电子笔记231（2009）191- 是的Σ⎪⎪⎨⟨∗⟩⟨∗⟩α⎧⎪⎨行动（第1页）：Nx1：= Nxtst（）BD1：= BDtst， {α} BD如果χ1=χ2= χα，uevJ（χ， χ）：=uev1（χ，χ2）ifχ1=αχ211 2uev1（χ1，χ2） 若χ1∈ Γ⎪⎪⎩⊥ .BD2：=否则Nx2：=Nxtst.⟨α⟩⟨α∗⟩ϕΣΣuevJ2（χ1，χ2）：=uev2（αuev2（χ1，χ2），若χ1∈ Γ否则的话1-规则根据Prop.2.6捕获了-公式的定点性质，只要主公式没有被BD阻塞。第一子中的本金选择要么是自由的，如果本金不是一个本金/一个本金-对于mula，要么是自由的，如果本金是一个 本金/一个本金-对于mula。 在后一种情况下，我们也阻止了再生的α，并通过将α放入BD 1中来避免“在一个世界”的循环。右子项的处理方式类似，但使用αα而不是。所有β规则的操作：状态：=unsatif stat1 =unsat stat2 =unsatopenif stat1 =open or stat2 =open否则禁止使用min（f，g）（χ， χ）：=如果f（χ1，χ2）=或g（χ1，χ2）=⊥12最小值（f（χ1，χ2），g（χ1，χ2））否则uevtunif状态⎪开放如果stat1=open，则uev：=默认值vJ1状态2uevJ2if stat1⎪打开=状态2直觉是：如果stat1=open=stat2，则UEvJ1，UEvJ2uevJi：uevJi的定义确保对（χ1，χ2），其中χ1是主计算公式，从子节点中相应的计算公式中获取值P. Abate等人理论计算机科学电子笔记231（2009）191205/⟨ ∗⟩ ⟨ ∗⟩⟨∗⟩⊥.（3）[−]Δ[a]|a∈APrg&<$∈ Fml- 是的ΣΣ（七） k ∈ {n + 1，.，n + m}。j ∈ {1，...，len（Hcr）}。k，{如果{1， . ，n}。stati/=openorn在1-规则中，特殊情况将uevJ1（χ1，χ2）的值设置为如果χ1和χ2等于这一规则的主公式，因为 α当左子元素填充时，则uev j（χ 1，χ 2）不再是未填充的。注意，uev J（χ1，χ2）仅在父元素中有χ 1时才被定义。min ： min的定义确保了只有当两个函数都定义为（χ1，χ2）时，我们才取f（χ1，χ2）和g（χ1uev：如果stat=open，则uev是无关的，因此我们任意将其设置为unfined。如果只有一个孩子有stat=open，我们取它的uev J。如果两个孩子都有stat=open，我们取uev j 1和uev j 2中定义的条目的最小值。所有以前的规则修改现有的uev条目，但从不创建新的。下一条规则是唯一一条创建uev条目的规则（通过识别循环）。潜在分支规则。你好，我是一个... 你好，an+1an+m[−]Δ， Γ：：Hcr， Nx， BD， BB：：stat， uev（刘伟）其中：Δ1，Δ1：：HCr1， Nx1，BD1， BB1* 统计局1，人口普查局1HCrn，Δn：：HCrn， Nxn，BDn， BBn|* 国家|:: stat ，uev(1)n+m≥0（2）Γπ。AFmlq|q∈AFml}(4)Δ i：={|[ai]<$∈ [−]Δ}，对于i = 1，.，n + m（5）α p ∈ AFml。{p，<$p}/r（6）{1， . ，n}。 {1， . ，len（HCr）}。 .你好，{\cH00FFFF}{\3cH0} ΔiHCr[j]Actionfor（行动）： 对于i= 1，...，n： HCri：= HCr @HCri，{HCri} Δi，Nxi：= Nxtst（Nxi），BDi：=Nxst，BBi：=Nxststat：=数据⎪n206P. Abate等人理论计算机科学电子笔记231（2009）191.Σ.我的意思是，i∈pre（&/= uevi（否则，uev k（·，·）：=j∈ {1，.，len（HCr）}，使得对于k=n+1，.，n+ mP. Abate等人理论计算机科学电子笔记231（2009）191207⎪⎨⟨ ⟩∈{}{}⟨ ⟩ ≤≤≤≤∈ ⟨ ∗⟩ ⟨ ∗⟩⟨ ∗⟩uev（χ1，χ2）：=uev i&&&（n + m}否则的话一些直觉是有序的：(1) 如果n= 0，则规则的应用不会生成新节点，并且stat的计算结果为open。如果m=n= 0，则我们另外有uev：= uev。(2) 集合Γ只包含命题原子或它们的否定。(3) [-]Δ集合只包含[a]类型的公式。因此，（2）和（3）意味着，只有当节点不包含α-或β-公式时，才能应用牛顿规则(4) 集合Δi包含了所有必须属于第i个孩子的公式，它满足了aii，这样我们就可以在后面建立一个Hintikka结构。(5) 节点不能包含矛盾。(6) 如果n > 0，则对于1 ≤ i ≤ n，每个子代数aii不被祖先“阻塞”，并且具有包含公式集i Δ i的子代数，从而生成子代数a i i所需的后继代数。注意，len（Hcr）表示Hcr的长度。(7) 如果m >0，则n+1k n+m的每个a k k被“阻止”创建其所需的子节点k Δ k，因为某些祖先完成了这项工作。这个祖先不仅必须由公式kΔk组成，而且必须是为了满足某个APrg的k而创建的。请注意，在查找循环时会忽略值a、k和a，因为我们只对所需子循环的内容感兴趣。HCri： 是父代的Hcr，扩展了一个额外的条目来记录“历史”在从根到第i个孩子的路径上使用“@”作为列表连接创建的世界。注意，我们存储的是一对（k，k<$Δk），而不仅仅是k<$Δ k。 也就是说，我们记得创建节点kΔk是为了满足a∈ APrg的akstat：如果某个子进程打开了stat，则父进程不满意。 但它也不...如果某个孩子，比如第i个孩子，以及其中的某个可能性α χ直觉上，后者告诉我们，最终的-ityαχ发生在植根于父场景的子场景中，但不能被填充。uev k：对于n + 1 kn+m，第k个孩子被更高的（代理）孩子阻止。对于每一个这样的k，我们设置uev k为常数函数，它将每一个公式对映射到其代理子的水平j。 不难看出，uevk是定义明确且唯一的。请注意，uevk只是用于定义uev的临时函数，如下所述blocking child本身必须已经被创建来填充一个由Hcr[j]的第一个分量所指示的表达式-公式Hcruev（χ1，χ2）：如果stat =unsat，则uev在任何地方都是unfined否则，对于每个χ1=i ∈ {1，.，n + m}，且每个χ2，其中<$ai <$i∈ pre（χ2），我们从对应的（实数）的公式对（i，χ2）中取uev（i208P. Abate等人理论计算机科学电子笔记231（2009）191⟨ ⟩⟨ ⟩⟨⟩⟨⟩∈ ⊆ ∈⊆⟨⟩⟨⟩⟨⟩如果一个代理i是对于所有其他公式对，uev是unfined。直觉上，一个定义的uev（χ1，χ2）标记了一个“循环”，它从父节点开始，最终“循环”到某个阻塞代理。uev（χ1，χ2）的值告诉我们代理的级别，因为我们不能将这个“循环”分类每个ai的uev取自专门为包含ai而创造的孩子，这是证明中至关重要的事实BDi， BBi， Nxi：每个子元素都没有封闭的菱形公式或盒形公式，其主公式由BDI的形式决定。- 和id-规则通过它们的副条件是互斥的，并且规则被设计为使得至少一个规则适用于任何节点。4.2Tableau过程如下一节所示，我们只需要构建一个完全展开的tableau，这意味着每个节点都有一个规则应用于它。因此，如果多个规则适用于一个节点，那么规则的选择是无关紧要的，因此任何规则应用策略都是好的。 当然，在我们的实现中，我们优先考虑id- 规则和-规则，因为他们可能会关闭一个分支机构更快。其他的规则，比如优先选择线性规则而不是分支规则，也是有用的。4.3终止性、可靠性和完整性定义4.4设x =（Γ：：Hcr，Nx，BD，BB：：stat，uev）是一个表节点，λ是一个公式，Δ是一组公式。 我们写为x[Δ x]表示Γ [Δ I]。x的各部分写为Hcrx、Nxx、BDx、BBx、statx和uevx。节点x是关闭的i statx =unsat，打开的istatx =open，禁止的i statx =禁止的。定义4.5设x是表T中的一个-节点（即对x应用了一个-规则）。 则x也称为状态，x的子节点称为核心节点。利用正则规则的表示法，公式<$ai <$$>i∈ x是阻塞的i<$n + 1≤i≤n+m。对于每一个非阻塞的子节点，子节点的后继节点是子节点规则的第i 对于每个阻塞的n a in ai∈ x，在从T的根到x的路径上存在唯一的核心节点y，使得{ni} nΔ i是y的公式集，y是y的父公式n aJ n ai的后继。我们称y为aii的虚后继，也称aii的（可能是虚的）后继中的公式i为核心公式。状态只是一个节点的另一个术语，但核心节点可以是任何类型的节点（甚至是状态）。通过反复应用α和β规则，一个状态从一个核心节点产生。 请注意，核心节点y中的核心公式是定义良好且唯一的：如果x1和x2是状态，y是a1 1 ∈x1和a2 2 ∈x2的（可能是虚拟的）后继，则1= 2。设φ是一个否定范式的公式，T是一个展开表，其根r=（{φ}：：[]， n，n，n：：stat， uev），其中stat和uev由rP. Abate等人理论计算机科学电子笔记231（2009）191209∧⟨∗⟩⟨∗⟩⟨ ∗⟩ ∧ ¬⟨ ∗⟩ ∧ ¬⟨ ∗⟩∗⟨ ∗⟩ ∧ ¬∗ ∧ ⟨∗⟩¬∗ →∗⟨ ⟩⟨ ∗⟩ ∧ ¬ ⟨ ⟩⟨ ∗⟩ ∧¬⟨∗⟩⟨ ∗⟩ ∧¬⟨ ⟩⟨ ∗⟩ ∧ ¬⟨∗⟩⟨ ⟩⟨ ∗⟩ ∧ ¬ ⟨∗⟩ ∧ ¬⟨ ⟩ ⟨ ∗ ⟩ ∧ ¬ ⟨/ ⟩⟨ ∗⟩定理4.6T是有限树。定理4.7若根r ∈ T是开的，则φ存在Hintikka结构。定理4.8如果根r ∈ T不开，则φ不满足。定理4.9如果|φ|= n，最坏情况下的时间复杂度为O（2 2n）。详细的证明可以在本文的扩展版本中找到[2]。4.4两个充分发挥作用的例子第一个简单的例子说明了该过程如何通过阻止α-和[ α ]-公式重新生成来避免由于“在一个世界”循环而导致的无限循环公式（q？） （p）显然是不满意的。 因此，任何具有根（q？） （p （3）不应开放。 图1显示了这样一个画面， 如果规则ρ应用于表中的每个节点，则该节点被分类为ρ-节点初始公式ψ（q？）将节点（1）中的子节点（p<$$>p）分解为β1-子节点p<$$>p和β2-子节点p <$<$p q？（q？）（pP）根据1-规则。 公式p然后根据-规则分解节点（2）中的p，并且节点（3）被标记为闭合的，因为它包含矛盾。节点（2）继承了节点（3）的状态，根据α规则，节点（3）没有改变，因此也是关闭的。因为β2公式 q？ （q？） （pp）是a a-公式，1-规则看跌期权 这个公式到它的Nx2，节点（4）的Nx值，从而迫使节点（4）有q？ （q？） （pP）作为其主要公式。 以相同理由1-rule把它自己的主公式（q？）（p p）到其BD2中，即节点（4）的BD值。因此，节点（4）分解q？（q？）（pP）根据 ？- 规则。 我再次重申， 所得到的节点（5）被迫具有（q？） （pp）作为其主公式，并且从节点（4）得到其BD值不变。节点（5）具有与节点（1）相同的主公式，因此应用1- 规则到节点（5）将导致过程进入“at a world”（无限）循环。因为节点（5）的历史BD包含 （q？）（pp），1-规则被阻止在节点（5）上，但是2、规则不是。 因此，分支被终止，状态将节点（5）的节点（5）设置为禁止（从而避免节点（4）继承节点（5）的状态不变，节