CoLoSS中的优化条件逻辑推理：动态规划策略在条件逻辑中的应用

理论计算机科学电子笔记262（2010）157-171www.elsevier.com/locate/entcs在CoLoSS中优化条件逻辑推理DanielHausmanna，1LutzSchroüdera，b，2aDFKI Bremen，SKSb德国柏林大学数学与计算机科学系摘要通用模态推理机CoLoSS涵盖了从分级和概率模态逻辑到联合逻辑和条件逻辑的各种逻辑，基于广泛适用的共代数语义和随后的模态分析和表演算的一般处理。在这里，我们提出的研究优化的推理策略中采用的CoLoSS。具体地说，我们讨论了基于短序列在许多研究中的逻辑中起核心作用的观察的动态规划和动态规划的策略。这些优化似乎对条件逻辑的情况特别有用，对于其中一些，动态规划甚至提高了条件逻辑的理论复杂性。了算法这些策略已经在CoLoSS中实现;我们对不同的逻辑进行了详细的比较，观察到在条件逻辑的目标域中，实现。关键词：共代数模态逻辑，条件逻辑，自动推理，优化，算法，记忆，动态规划1引言近几十年来，模态逻辑已经看到了语义异质性的发展，见证了许多逻辑的出现，虽然仍然具有明显的模态特征，但不符合标准的Kripke语义。例子包括概率模态逻辑[4]，联盟逻辑[11]和条件逻辑[2]，仅举几例。 超越Kripke语义的举动，反映在句法方面正态性的失败，给tableau和mosaic系统带来了额外的挑战，因为tableaux和模型之间的对应关系变得更松散- tableaux仍然是图形，但模型通常是更复杂的结构。这个问题在理论方面通过引入余代数模态逻辑的语义框架来解决[8，12]，它涵盖了上述所有逻辑1电子邮件：Daniel. dfki.de2电子邮件：Lutz. dfki.de1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.012158D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157{|{\fn方正粗倩简体\fs12\b1\bord1\shad1\3cH2F2F2F}和更多. 事实证明，共代数模态逻辑确实允许设计通用推理算法，包括源自[15]的通用tableau方法;这种通用方法实际上可以从语义中分离出来，纯粹按语法开发，如[9，10]中所执行的共代数模态逻辑的一般表算法，特别是[15]中描述的算法，已经在推理工具CoLoSS [1]3中实现。如上所述，通用tableau系统的一个必要特征是，它们可能为给定的模态需求生成多个后继节点，因此除了典型的深度问题之外，证明搜索还面临相当明显的广度问题。因此，寻找优化策略以提高推理效率变得更加迫切。在这里，我们提出了一个这样的策略，这是普遍适用的，但特别是有效的减少深度和分支的条件逻辑类。我们利用这个类的一个显着的特点，即许多相关的规则相当严重地依赖于前提声明公式之间的等价性，因此，条件逻辑是一 个 很 好 的 候 选 人 memoising 策 略 ， 明 智 地 适 用 于 短 序 列 。 我 们 描 述 的implement- mentation的memoising和动态编程策略内CoLoSS，并讨论各种比较实验的结果2余代数模态逻辑的一般序列演算共代数模态逻辑最初是作为coalgebras的一种规范语言引入的，被视为通用反应系统[8]，此后已经发展成为超越Kripke语义的模态逻辑的通用框架[3]。其基本思想是封装与特定模态逻辑的语义相关的系统的分支类型，比如概率或博弈论分支，在集合函子、符号函子（例如，在所提到的例子中的分布函子和博弈函子）的选择中，并根据所谓的谓词提升来捕获模态算子的语义。 为了本工作的目的，语义的细节与我们现在要回顾的证明论方面相比，它们的相关性更小。共代数方法所涵盖的逻辑范围非常广泛，除了标准的Kripke和邻域语义之外，还包括例如分级模态逻辑[5]，概率模态逻辑[4]，联盟逻辑[11]，配备选择函数语义的各种条件逻辑[2]等等。在句法上，逻辑通过选择模态相似性类型Λ来参数化，即一组具有相关有限性的模态算子。 这一选择决定了 公式φ，φ的集合通过文法φ，φ：：= p |φ ∧ ψ |¬φ|（φ1，.， φ n）其中是Λ中的n 示例为Λ= L pp[0， 1] Q的概率模态逻辑的一元算子Lp读作“概率至少为p”; Λ = { Qk|k ∈ N}，分次模态逻辑的算子Qk在k以上读3可在http://www.informatik.uni-bremen.de/cofi/CoLoSS/上查阅D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157159{|}♥{}∪{¬|∈ }{|∈∈SCSCSCSCT¬⊥SCSC（<$F）Γ，<$F（AX）Γ，p，<$p（）Γ、AΓ、Γ，AB（）Γ，AΓ，（<$）Γ，<$（A<$B）Γ，<$A，<$Bsuccessors’; Λ = [ 二元模态算子 条件逻辑读作. .然后正常。. .余代数模态逻辑最初局限于所谓的秩1逻辑，由模态算子的嵌套深度一致等于1的公式公理化[12]。它已经被扩展到更一般的非迭代逻辑[14]，并在一定程度上扩展到迭代逻辑，由嵌套模态的公式公理化[13]。这里考虑的例子都是rank-1，所以我们关注这种情况。在秩为1的情况下，已经证明[12]，所有逻辑都可以通过一步规则φ/φ来公理化，其中φ是纯命题的，φ是形式为（a1，...，a n），其中a i是命题变量。在微积分的上下文中，它采用以下形式[9]。定义2.1如果S是（公式或变量的）集合，则Λ（S）表示集合（s1，.， s n）n是n元，s1，.， s nS的公式，包含一个模态对S的元素的一个应用。一个S-ε，或者在S是所有公式的集合的情况下只是一个ε，是S A A S的有限子集。然后，一步规则Γ 1，…，在变量集V上的Γ n/Γ 0由V-序列Γ 1，.，Γn是前提，a Λ（S）-<$Γ0是结论。一个目标是一组序列，通常作为规则应用的实例化前提的集合而出现一个给定的一步规则集，然后归纳出一个通用微积分的实例化[9]，该实例化由一组规则Rsc给出，该规则由finishing和分支规则Rb（即没有前提或有一个以上前提的规则），线性规则Rl（即，规则只有一个前提）和模态规则Rm，即一步到位的规则。完成和分支规则如图1所示（其中=p是原子），线性规则如图2所示。到目前为止，所有这些规则都是纯粹的命题。作为一组模态一步规则的例子，考虑标准模态逻辑K的模态规则Rm，图3。Fig. 1. 终止和分支规则Rb图二、 线性规划规则R1160D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157⇒（CK）A0=A1;. ; A n= A0<$B1，.，<$Bn，B0Γ，<$（A1<$B1），.，<$（An<$Bn），（A0<$B0）（K） <$A1，.， An，A0I，<$QA1，...，<$QAn，QA0图三. K的模态规则在规则集和共代数语义的适当一致性假设下，这种演算已经被证明是完备的，只要规则集在精确的意义上吸收切割和收缩[9]。 我们说一个公式是可证明的，如果它可以在微积分的相关实例中导出;下面给出的算法涉及可证明性问题，即决定是否一个给定的可证性是可证的。这是因为微积分不包含切割规则，因此可以自动进行证明搜索。对于秩1逻辑，证明搜索可以在PSPACE中在规则集的表示上进行适当的假设[15，9]。相应的算法已在CoLoSS [1]系统中实现，该系统仍在继续开发中。特别注意寻找启发式优化，以实现实际有效的证明搜索，如这里所述我们在下面的优化策略演示中使用的运行示例是上面提到的条件逻辑。最基本的条件逻辑是CK[2]（我们将在下面考虑一个稍微扩展的逻辑），其特征在于假设非单调条件的右手参数的正规性。，但仅替换左侧参数中的等价物。 吸收截和缩需要一个统一的规则集，它由图4所示的规则组成，其中A=C表示一对数列<$A，C和<$C，A。 这个插图-见图4。 CK的模态规则在下面描述的优化策略中起作用的两个要点。首先，这个规则在存在性和泛在性上都有很大的分支度-第二，许多前提是短序。这将在我们的备忘录战略中得到利用。我们注意到，条件逻辑的带标签演算已经在以前设计过[7]，并且已经在CondLean证明器中实现过[6];相比之下，我们的演算是无标签的，并且在概念上更简单。 标记和未标记结石的相对效率的比较目前仍是一个悬而未决的问题D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157161RR--⇒ ∨ ⇒ ¬（CKCEM）A0= A1;. ; A n= A0Γ，（A0<$B0）， . ，（Aj<$Bj），<$（Aj+1<$Bj+1）， . ，<$（An<$Bn）B0， . ，Bj，<$Bj+1， . ，<$Bn存在。3该算法根据上面介绍的框架，我们现在设计一个通用算法 决定公式的可证明性，这很容易被实例化为特定的逻辑 通过实现相关的模态规则。算法1以以下方式使用了所有的规则：为了证明公式φ的可证明性，算法从公式φ开始，并不断尝试应用所有的规则，sc给它，给予优先 线性规则。下面，我们指的是一个尚未被检查可证明性的开放式数据库。在[15，9]中对规则集的适当易处理性假设下，该算法实现了理论上界PSPACE。它是CoLoSS中采用的证明搜索算法的起点，本质上是[ 1 ]中描述的算法的重新表述，其中很容易验证算法的正确性和终止性通过这种重新表述得到保留;该算法的优化是本工作的主题。算法1（判定一个矩阵的可证明性）1.尝试从sc到Γ的所有可能的规则应用，优先考虑线性规则。对于每个这样的规则应用程序，执行以下步骤，如果这些步骤对其中一个规则应用程序成功，则回答2. 令Λ表示由规则应用产生的前提集合。3. 递归地检查Λ中的每一个都是可证明的。3.1条件逻辑实例引入的微积分的通用性允许我们为各种模态逻辑快速创建算法1的例如，在[10]中已经表明，CKCEM的复杂性是coNP，使用[16]精神的动态规划方法;事实上，这是探索这里追求的优化策略的原始动机。由于这个原因，我们在本节的剩余部分仅限于示例条件逻辑CKCEM;稍微修改的优化版本将适用于其他条件逻辑。CKCEM的特点是附加公理的条件排除中间（A B）（A B），其中吸收削减和收缩是集成在规则CK如图5所示。图五、条件逻辑的模态规则CKCEM162D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157−联系我们联系我们−−K K→ {T}在下文中，我们使用条件前件和条件后件的概念来指代条件逻辑的模态算子的参数为了使用算法1决定是否存在条件逻辑的模态规则的实例，其可以应用于实际的当前谓词，有必要为该谓词中的模态算子的所有前提的等式的每个可能组合创建初步前提。 这将导致在2n 1新的前提下，一个有n个顶级模态算子。例3.1对于∑ r=（A0B0），（A1B1），（A2B2），则有2 3 = 8个可能的规则实例，对应于目标的非空子项;对于I <${1，2，3}，要检查的前提由Ai= A j（对于i，j∈I）和{B i|i∈ I}。这似乎是一个更聪明的方法，首先将当前表达式中的顶级模态运算符的所有前因的集合划分为关于逻辑相等的等价类。 这种划分可以大大减少要尝试的规则数量和每个规则实际证明的前提数量。例3.2再次考虑例3.1中的矩阵。利用考试-如果知道A0=A1，A1/=A2和A0A2，则立即存在只是模态规则的两个合理的情况，导致两个前提B0，B1和B2。对于这两个前提中的第一个，注意没有必要再次证明A0和A1的等价性。在条件逻辑的情况下，观察以下情况：由于公式中出现的模态前件不被任何微积分规则改变，甚至在应用实际的微积分之前，提取公式的所有可能相关的前提是可能的。这使我们能够首先计算所有相关前因的等价类，然后将这些知识输入到实际的微积分中，如下所示。4优化定义4.1模态嵌套深度i的条件前件是包含至少一个模态嵌套深度i 1的前件并且不包含模态嵌套深度大于i 1的前件的条件前件。嵌套深度为0的条件先行项是不包含任何其他模态运算符的先行项。令ai表示模态嵌套深度i的所有条件先行项的集合。进一步地，令prems（n）表示模嵌套深度至多为n的所有条件项的集合（即，prems（n）=j=1.. naj）。最后，设深度（φ）表示公式φ中的最大模态嵌套。定义4.2集合一个函数eval：，称为知识库。我们现在可以构造一个优化算法，它允许我们在某些情况下更有效地确定公式的可证明性（和可满足性）优化算法D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157163RORRO···ROROKKK（C KCE Mm）B0， . . . ，Bj，<$Bj+1， . ，<$BnΓ，（A0<$B0）， . ，（Aj<$Bj），<$（Aj+1<$Bj+1）， . ，<$（An<$Bn）图第六章条件逻辑的修正模态规则CKCEMm（i，j ∈ {1..n}eval（A i=A j）= T）Rithm由两个函数构造（即，由实际证明函数和由所谓的预证明函数构造）：算法2（使用知识库（K，eval）判定φ的可证明性）1. 如果r∈ K，如果eval（r）= T，回答否则：2.尝试从sc到Γ的所有可能的规则应用，优先考虑线性规则，其中sc是考虑知识库的优化规则集，如下所述。 对于每个这样的规则应用程序，执行以下步骤，如果这些步骤对其中一个规则应用程序成功，则回答3. 令Λ表示由规则应用产生的前提集合。4. 递归地检查Λ中的每一个都是可证明的。算法2与算法1非常相似，但依赖于传递的知识库 并且使用修改后的规则集SC。规则集sc适当地使用知识库。它是通过用图6中的修改后的模态规则替换图5中的模态规则而从sc得到的。关键是前提A0==A n被表示在知识库中查找的边条件所取代。这改进了由上述算法的步骤1中的查找操作所体现的标准记忆，因为减少了潜在适用规则上的存在性分支：规则甚至不匹配目标对象，除非等价前提已经在知识库中。由于memoising的组织方式，这仍然是一个完整的系统，如下所述算法2中使用的知识库在算法3中计算。根据[16]的精神，该算法通过动态编程进行，其阶段对应于模态嵌套深度因此，为了证明嵌套深度最多为i的两个条件前件的等价性，我们假设嵌套深度小于i的模态前件之间的等价性i已经被计算，并且结果存储在evali中;因此，如果算法2仅使用知识库（Ki，evali）可证明它们的等价性，则两个前件是相等的算法3步骤1：对于作为输入的m ula φ，Takea。 设i=0，K0=0，eval0=0。步骤2：生成嵌套深度为i的φ的所有条件前件的集合前提i。 如果i 600.000s0.217s0.092s8600.000s1.944s0.761s9600.000s17.826s6.929s见图8。 混合物（i）的结果• 公式explode（i）包含等价的但在句法上不相等的并且相互嵌套的模态先行词，其深度最多为i：explode（i）= X i. XiX i=（A i）（. （A i（c1. （c i））. . ））Xi=（Ai（. （A icj）. . . ））jjmodi（j+（i−1））modiAi=pj mod i...p（j+（i1））modi这个类包含复杂的公式，未优化的算法不再有效： 只有关于所有出现的模态前件Ai允许证明算法达到所有模态结论，而只有组合的n（c1... c i），c1，.， c i（含每一个出现的结果）都是可证明的。对于此类公式（专门设计用于显示动态编程优化的优点），优化算法大大优于未优化算法（见图9）。测试在Linux PC（双核AMD Opteron 2220S（2800MHZ），16GB RAM）上进行。很明显，通过所提出的优化可以获得性能的显著提高。 总的来说，性能 在通用推理机CoLoSS中实现所提出的算法与CondLean等专用条件逻辑证明器相当;由于用于评估CondLean的基准公式未在[6]中明确列出，6广义优化如前所述，所展示的优化不限于条件模态逻辑的情况。定义6.1如果Γ是一个实数，我们表示顶层168D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157S联系我们--（可选）S1...SnΓS我算法1算法3算法410.004s0.004s0.004s20.005s0.005s0.005s30.006s0.006s0.006s40.014s0.007s0.007s50.130s0.009s0.008s60.302s0.011s0.012s7430.684s0.015s0.016s8600.000s0.021s0.019s9600.000s0.029s0.022s见图9。 爆炸结果（一）由arg（Γ）从Γ导出模态。一个短公式是由一个公式组成的一个公式，这个公式本身是一个固定的最大数上的命题公式。从arg（r）中提取模态参数。在下文中，我们将短序列中模态参数的最大数量固定为2。然后，优化的一般方法采用以下形式：设S1，...，S n是短序列，并假设存在图10中描述的通用规则的合理实例（相对于手头的逻辑）（其中是任何序列集）。图10. 可以应用优化的一般规则方案然后，我们设计了优化算法的最终版本（算法5）：我们现在将注意力扩展到任何模态参数上的任何短序列，而这个新算法5可以用来决定公式的可证明性，其中所采用的规则集必须由图11给出的通用修改规则扩展。例6.2以下两种情况是一般优化的实例(i) （经典模态逻辑/邻域语义学）设Γ =QA=QB，n= 1，S1=A=B且= . 然后，只要下面的同余规则在手头的逻辑中是合理的，就可以应用算法5D. 豪斯曼湖Schröder/Electronic Notes in Theoretical Computer Science 262（2010）157169KKKS联系我们Mon→TSCRO（可选）SΓ见图11。 通用优化规则（i∈{1.. n}eval（Si）= T）算法5步骤1：取公式φ作为输入。 设置i = 0，0=，eval0=。步骤2：生成φ的所有模态参数的集合args i，这些模态参数的嵌套深度最多为i。 如果i

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