CoLoSS：余代数逻辑可满足性求解器 统一多项式空间算法实现共代数语义模态逻辑满足性决策

理论计算机科学电子笔记231（2009）41-54www.elsevier.com/locate/entcsCoLoSS：余代数逻辑可满足性求解器乔治·卡林1德国不来梅雅各布大学Rob Myers2 Dirk Pattinson德克·帕丁森3，5为英国伦敦帝国学院LutzSchrüder4，5德国DFKILabBremen和Universita？tBremen摘要CoLoSS是Coalgebraic Logic Satifiability Solver，以通用和组合的方式决定模态公式的满足性。 它实现了一个统一的多项式空间算法，以确定符合共代数语义的模态逻辑的可满足性。这包括例如逻辑K、KD、保利联合逻辑、分级模态逻辑和概率模态逻辑。 通过以特定格式提供其共代数语义的完整公理化，逻辑很容易集成到CoLoSS中。 此外，CoLoSS是组合的：它综合了逻辑模块组合的决策过程，其中包括两个模态逻辑的融合作为特例。因此，人们自动获得推理支持，例如，对于在概率自动机上解释的逻辑，概率自动机以不同的方式结合了非确定性和概率。保留字：模态逻辑，自动证明，余代数。介绍虽然有许多具有标准Kripke语义的模态逻辑的自动证明工具，特别是在最近兴起的 模 态 逻 辑 作 为 描 述 逻 辑 的 背 景 形 式 主 义 的 情 况 下 （ 例 如 ， 颗 粒 [19]，FaCT/FaCT++[20]，1g. iu-bremen.de2rm606@doc.ic.ac.uk3dirk@doc.ic.ac.uk4Lutz. dfki.de5部分由DFG授权号SCHR 1118/5-1和EPSRC授权号EP/F031173/1支持1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.02.02842G. Calin等人/理论计算机科学电子笔记231（2009）41F和RACER [3]），几乎没有工具支持（条件逻辑证明器CondLean [11]的显着例外）越来越多的新设计的非正规模态逻辑，其语义涉及的结构是不同的，大多数比标准Kripke框架更复杂。这种逻辑的例子包括概率模态逻辑[9，5]，多数逻辑[12]，联盟逻辑[13]和Presburger模态逻辑[2]。最近，共代数模态逻辑被证明为模态逻辑提供了一个合适的通用语义框架，特别是允许设计通用的决策过程，这些决策过程可以为特定的模态逻辑实例化。 特别是，许多逻辑公理化没有嵌套的模态运算符 可以在PSPACE中使用通用满意度求解器[15]来决定在 这 里 ， 我 们 给 出 了 一 个 系 统 描 述 的 Coalgebraic 逻 辑 可 满 足 性 求 解 器（CoLoSS），实现框架，这种通用算法的实例很容易集成。CoLoSS在Haskell中实现，并利用Haskell类型类机制来方便创建新的逻辑实例;它带有（不断增长的）数量的预实现实例，包括K，KD，分级和概率模态逻辑以及联盟逻辑。 实现一个新的逻辑实例本质上只不过是定义它的语法和提供一个体现它的公理化的接口函数此外，CoLoSS支持[16]中描述的逻辑和决策过程的模块化组合这意味着，例如，通过为概率模态逻辑和多智能体K提供实例，可以自动获得复合模态逻辑的实例，第3节）或交替系统的模态逻辑[16]。材料组织如下。在第1节和第3节中，我们简要总结了用于共代数模态逻辑和逻辑组合的通用PSPACE算法的理论背景。满足性（实际上是有效性）检查的核心算法的实现在第节中描述。 2，而实现的逻辑组合机制中讨论的节。四、CoLoSS的源代码可在http://www.doc.ic.ac.uk/ ~{} dirk/COLOSS/coloss.tar.gz下获得1余代数模态逻辑的通有有效性检验我们简要回顾了作为模态逻辑的通用语义框架的共代数模态逻辑，以及基于它的通用PSPACE决策程序[15]，我们将其对偶为有效性算法。 给出了模态逻辑的语法通过包含给定的模态算子的模态签名Λ;然后由文法确定：：=|ψ1∧ψ2 |L（1，...，|L (ψ1,..., n），G. Calin等人/理论计算机科学电子笔记231（2009）4143MR∈MQ→∈FF|→M|RR{∈||}∈ ∈∈其中L∈Λ是n元的。 我们通过以下方式参数化这种模态语言的语义： 由签名函子组成的Λ-结构M（overT）的选择T：设置→设置在集合和映射的范畴Set上，给出了提升M[[L]的n元谓词对T的赋值，即一个自然变换M[[L]]：Qn→QTop其中：SetopSet表示逆变幂集，到每个n元模态算子LΛ。我们省略了提及何时这不太可能引起混淆。回想一下，一个T-余代数C=（X，X）由一个状态集X和一个转移映射X：X TX组成。该结构决定了V上T-余代数C=（X，λ）和（Λ）-公式的状态x X之间的满足关系=C.的关系=C是归纳定义的，带有布尔运算符的常用子句。n元模态算子L的子句是X|= CL（φ1，.，φ n）惠 函数（x）∈ [[L]]（[[φ1]] C，.，[[φ n]] C）其中[φ]]C= x X x = Cφ。当下标C从上下文中看得很清楚时，我们去掉下标C我们的主要兴趣是在有效性问题（及其对偶，满足性问题）：定义1.1An（Λ）-公式φ成立，如果对每个状态x，x=Cφ，T-余代数C.下面将给出结构的示例[15]中描述的满足性的决策过程依赖于一个完整的公理化w.r.t. 以上语义以一步规则φ/φ的形式，其中φ是变量a的命题组合V和V是在形式L（a1，...，a n），LΛ，a iV. 此外，这种公理化需要在规则归结下被封闭，其中两个规则的预解式是通过归结它们的结论并结合它们的前提而形成的，并且在收缩下，即。删除在识别两个变量后产生的规则结论中的重复文字给定这样一个公理化，规则，表示为C扩展通过替换等价物。然后在交替图灵机上有以下算法：算法1（判定φ∈ F（Λ）的有效性）(i) （全称）从φ 的合取范式（CNF）中 选 择 一 个子句θ。(ii) （假设）猜测θ的一个非空子子句ρ。(iii) （半势）猜想χ/σ对于某些置换σ.(iv) （全称）从χ的CNF中选择一个子句γ。(v) 递归检查γσ是否有效。|44G. Calin等人/理论计算机科学电子笔记231（2009）41M⊆MR如果在标记为universal的步骤中所有可能的选择都导致成功终止，并且对于所有标记为existential的步骤，存在导致成功终止的选择，则算法成功。注意到在步骤（iii）中，它需要取规则对前提的命题等价取模。为了确保多项式运行时间的算法，需要要求规则的编码方式，一个需要考虑的规则代码的多项式有界的大小。满足这个条件和一些小的健全性要求的规则集被称为PSPACE-可处理的。可获得定理1.2如果算法1被PSPACE-可处理的一步规则集完全公理化，并且在分解和压缩下是封闭的，则算法1在交替多项式时间内，即在多项式空间内判定Λ-公式的有效性。由于完备性，有效性与可证明性一致。 的假设 上述定理的一部分特别地由以下逻辑满足例1.3我们给出了一些在[15]中更正式讨论的共代数模态结构的非正式描述：(i) 模态逻辑K在协变幂集函子P上解释为[[Q]] XA ={B ∈ P（X）|B A}。(ii) 类似地，逻辑KD在非空幂集函子上解释(iii) 阶化模态逻辑（GML）中的模态算子Qk. . 边带有重数的图(iv) 概率模态逻辑（PML），具有概率至少为p的算子Lp. .(v) 联盟逻辑（CL）在代理的固定有限集合N上，具有运算符[C]'联盟C N可以强制。. .在[ 13 ]的意义下，在其余代数是博弈框架的类值函子上解释了“在下一图1显示了满足定理1.2假设的这些逻辑的规则集。GML和PML的规则前提中的算术表达式指的是特征函数的（命题可表达的）算术，如果r >0，则sgn（r）φ是φ，否则是<$φ2通用PSPACE算法的实现CoLoSS在Haskell中实现[14]，并使用多态类型和类型类将CoLoSS的通用方面与特定逻辑的细节分开。从这个角度来看，一个特定的逻辑实例由一个类型标识，该类型包括一组描述逻辑语法的（一元）模态运算符;为每个实例实现的类接口基本上由一个匹配函数组成，该函数包含一组管理演绎过程的单步规则G. Calin等人/理论计算机科学电子笔记231（2009）4145→K：i=1nnα→β我（n≥0）KD：K和i=1¬i=1ΣnQαi→Qβ¬GML：i=1nr α≥0我我（n≥1，ri∈Z−{ 0}，nαini=1 Qαi（n≥0）i=1 sgn（ri）Qkαi我PML：Σni=1 r α≥k我我1≤i≤n sgn（ri）Σri0 |（k i + 1）≥ 1+ 1| (k i+1) ≥ 1+ Σri>0 （rin≥1，ri∈Z−{我⎜.0}，⎞⎟客户：n⎝Σni=1 RIPI（cbox [0]（p 0））在一个infix操作符-->的帮助下，Atom的缩写p和模态46G. Calin等人/理论计算机科学电子笔记231（2009）41i=1，χ<$φi∈IKi=1I Icbox：：[Int]->LC->LC;cagphi=M（Cag）phi作为句法糖添加的。应用CoLoSS函数可证明和可满足确认了上述公式（当然）是可满足的但不可证明，而公式(cbox[1. 3]（cbox [3.. 5]（p1）/\cbox [1，2]（p2））/\cbox [4]（cbox [3]（p 2）/\cbox [1，2]（p1））-->cbox[1.. 5]（cbox [1..（（p1）/\（p2））是可以证明的通用可证明性（有效性）检查器的逻辑特定部分在算法1的步骤（iii）和（iv）中进行了说明，这些步骤从结论传递到一步规则的前提。正是这种匹配过程形成了CoLoSS中通用逻辑类接口的核心。换句话说，CoLoSS中逻辑类的每个实例（由编码模态运算符的数据类型体现）都需要提供一个返回特定子句的规则匹配集的函数。因此，类型类Logic定义如下：class（Eq a）=>逻辑a，其中match：：子句a -> [[La]]其中子句a类型的居民由两个列表组成，这两个列表分别收集形式为L（φ1，.，φ n），其中L是模态算子。匹配c的结果是一个规则前提列表，使得如果列表中的前提之一是可证明的，则c是可证明的;每个前提都被给出为表示其CNF的子句的公式列表，其中替换根据已经执行的与c的匹配（在并行实现中，算法1的两个逻辑特定步骤已被实现为单独的接口函数，而替换步骤已被通用地处理;两种方法的相对优点正在调查中。因为K的解析封闭规则集是nai→b我们有下面这个逻辑的实例声明实例逻辑K，其中match（Clause（pl，nl））=let（nls，pls）=（map neg（strip nl），strip pl）inmap（\x-> [disj（x：nls）]）pls其中strip从列表中的每个原子Qφ中移除最外面的Q，并且disj将公式列表变为析取。也就是说，给定子句的匹配集=Qj∈JQ <$j由所有公式i∈Iφ i→ <$j，j∈J组成. 请注意，在本节中-子集上的格 可以忽略J作为式i∈IJφi→ψi意味着 匹配返回的i∈Iφi→jQai→QbG. Calin等人/理论计算机科学电子笔记231（2009）4147j=1j=1算法 同样，结论中文字的排列可以忽略，因为这样的排列导致命题等价的前提。更一般地说，当置换导致的前提也是通过与原始结论匹配而出现时，它们可以被忽略。目前在CoLoSS中实现的其他逻辑的公理化类似地表示。我们对两种特殊情况进行评论：在规则集中ni=1 ai→bmcjni=1[Ci]ai→[D]bm[N]cj在联合逻辑中，我们必须注意Ci是成对的这一附带条件D的不相交子集（回想一下，N表示所有代理的集合）。我们可以通过在图中寻找其节点是具有从Ci到Cj的边的Ci的团来匹配这个条件，如果Ci和Cj不相交。(Note代理人的数量是固定的，这样就不会增加另一层NP-硬度。对于分级模态逻辑和概率模态逻辑，我们必须计算需要考虑的系数的上界，以覆盖所有规则匹配。对这些逻辑的规则前提的一般格式的一瞥表明，它可以考虑逐点极大的解。 它可以想象，整数线性规划方法可以卓有成效地应用于 以加快寻找这样的解决方案。给定一个计算特定逻辑的规则匹配的函数，决定可证明性的算法的通用部分计算输入公式的合取范式，并递归地检查合取范式的每个组件至少有一个可证明的匹配，因此算法的核心采用以下形式：probable：：（Logic a）=> La -> Bool可证明的phi=all（\c-> any（all probable）（matchc））（cnfphi）一个注释是为了说明上面的函数是否真的使用了多项式空间。 从表面上看，传递的对象似乎太大了，比如phi的CNF或给定子句的匹配列表。然 而 ，Haskell是一种非严格的语言，编译器使用惰性计算;因此，大型列表中的条目是根据需要计算的，并且可以依靠内置的内存管理来提高空间使用效率。3组合逻辑的模可满足性检验人们已经从不同的角度观察到，在逻辑和结构可以一致地组合的意义上，共代数模态逻辑适合于模块化，保持诸如可靠性和完整性的性质[1]。[16]中提出了一种改进的逻辑合成方法，在这个意义上，它也允许对算法结果进行模块化处理，例如第1节中提出的算法结果。关键的新颖性是解释复合逻辑，其公式自然是多排序的，在多排序余代数。为了实现CoLoSS，需要理解逻辑组合机制的语法方面，48G. Calin等人/理论计算机科学电子笔记231（2009）41、∗→∗ ≤≤→∗我们在下面回顾。作为一个激励性的例子，考虑Segala系统的模态逻辑[8]。回想一下，在一个（简单的）Segala系统[17，18]中，每个系统状态可以非确定性地执行导致其后继状态的概率分布的动作aa·，bsJ J vz0。2 -是的-是的-是的，0. 5.0。81.0。五、、•sJ· J· J· Jv· z[8]的逻辑区分了非确定性公式和概率性公式，它们由下式归纳给出：Ln3φ：：= T|φ1∧φ2|¬φ|Qa（非确定性公式;n∈ Lp，a∈A）Lp3：：=T|ψ1∧ψ2|¬ψ|L q φ（概率公式; φ∈ Ln，q∈ [0，1]<$Q）.这样就有了一个分层的双排序逻辑，可以认为它是由一个模态签名生成的，该签名包括排序n和p（非确定性和概率）以及两个模态算子族Qa：p → n（a ∈ A） 和Lq：n → p（q ∈ [0，1]<$Q）.这种逻辑是两个特征的结合，非决定论和不确定性，可以形式化如下（详见[16]）：n元特征F包括多排序模态签名，其中模态运算符具有轮廓L：i1，. .ik由正式输入排序1组成i1，.，Ikn和一个正式的目标排序。特征还配备了一个共代数语义，包括一个n元集函子[F]和作为适当谓词提升的模态运算符的解释，以及一步规则集，现在采用以下形式φ1：1;... ;φn：n、ψ其中，对于i= 1，.，n，φ i是一个在命题变量集Vi上的纯命题公式，φ i是一个在原子上的子句，其形式为L（a1，...， a k）与L：i1， . ，ik→n，且aj∈Vij，j=1， . ，k.在具体规则的符号中省略的前提φi默认等于T。例3.1例1.3的逻辑可以看作是一元特征K、KD、GML、PML、CL。逻辑组合中的几个典型结构可以转换为二进制特征，如图2所示。选择：在不相交的二进制和函子上解释的二进制特征Ch具有单个模态操作符+：1，2→n，读作casestatet。Fusion：二元特征Fu，在二元积函子上解释，有两个模态运算符[π i]：i，i= 1，2，对一个对的两个分量进行陈述。 具有签名Λ 1，Λ 2的两个逻辑的融合通过将Lφ转换为[π i] Lφ（对于L∈ Λ i）来编码。G. Calin等人/理论计算机科学电子笔记231（2009）4149⇒→ ∗SSQ → Q→CH：（j=1k=1j=1k=1Mα→J傅j=1k=1（Mj=1n1），1），Mγ→Jnδk）：2Mα→（α+γ）→nJJk=1（βk+δk）MnJCnd：（j=1[π]α→I jβk）：ink=1[πi]βk（i= 1，δ，δ ∈{γ，.，γ，γ，...，γ}1 2 1个月1JnJ1（ -δ））：12（Mj=1（γ）J· α）→nJk=1k（γβ）Mj=1 α→JJ·Knk=1 βk）：2（m，n≥0）图二、示例3.1的特征的规则集条件性：二元特征Cnd，在二元函子λX，Y上解释。 （X）Y（与 表示逆变幂集， 表示函数空间）具有二元模态算子·：1， 2，读作非单调广义条件。通过特征的组合来构造逻辑是通过粘合的概念来形式化的。一个胶合G是在一组基本排序符号上的一个索引项族，这些基本排序符号使用特征作为函数符号形成。这样一个项族以明显的方式在集合S上归纳出一个内函子[G]]，它的余代数充当归纳模态逻辑的语义结构。后者本身是多排序的，对于G中出现的每个真子表达式都有一个语法排序（排序s本身的完整表达式与基本排序s相同），并且公式由相当明显的类型规则生成，对于演绎也是如此。例如，上述激励示例中的逻辑被完全描述为粘合Seg=（n→HML（PML（n），其中HML是与Hennessy-Milner逻辑相关联的特征，即K的多代理版本。[16]的主要结果表明，胶接可以简化，保持公式的满足性。这里，如果一个胶合的每个特征表达式只包含一个特征，那么这个胶合被称为胶合。该构造引入了一个新的排序，每个正常的子表达式发生在一个给定的粘合。例如赛格的回归是（n→HML（p），p→PML（n）），其中p是表示子表达式PML（n）的新排序。使用双端胶接的优点是第1节的结果直接推广到双端胶接。 公式在胶合中的有效性（因此，在任何一种胶合中，胶合与其胶合的等价性）是可以判定的。通过算法1的模块化变体，其具有用于每个排序的有效性检查例程;这些例程递归地相互调用（如在算法的步骤（v）中50G. Calin等人/理论计算机科学电子笔记231（2009）41一元特征二进制特征<+>二元选择<*>融合辅助符号S形式排序变量<.>特征应用图三. 目前集成在CoLoSS根据定义逻辑的粘合的类型规则4组合逻辑为了检查组合逻辑的可证明性，CoLoSS综合了一个Haskell程序，该程序实现了手头的逻辑特征的特定组合，基于现有的 实现各个特征。需要诉诸这种看似迂回的策略的主要困难是从给定的粘合中生成良好排序的公式的相互递归数据库，这一挑战似乎使现有的多型库和Haskell扩展的表达方式负担过重（参见。例如[10]）。唯一能想到的替代代码合成的方法是使用类型规则的深层编码（而目前的方法只是使用Haskell的类型检查机制）。这是留给未来版本的工具，将纳入一个完整的逻辑定义语言。在CoLoSS中，组合逻辑被描述为上一节中讨论的胶合然后自动构造胶合的预排序（目前仅用于单排序胶合）。目前，CoLoSS支持图3中列出的功能。 图中给出的语法部分基于以下语法加糖：一种单排序胶合的数据类型，其构造函数是唯一的排序变量S和一元和二元特征应用：in fix运算符<。简化了一元特性的应用，目前实现的两个二元特性的应用分别以具有优先顺序的整数运算符<+>和<*>的形式进行了优化<。>，& lt;*>，<+>和<.> 右为右为右。因此，具有例如以下胶合Seg = HML<。> PML<。> SAlt= HML<.> S< +> PML<。> SKKD = KD<.> S< *> K<.> SPC = CL<.> PML<。> S其中Seg对应于前一节中的简单Segala系统，Alt表示交替自动机的逻辑[16]，其中非确定性和概率性转换可以任意交织[4]。 粘合KKD是K和KD的融合，PC代表概率联盟的逻辑，它允许对具有概率结果的联盟策略进行推理;我们将在本节结束时回到这个逻辑平面胶合可以使用K、KD逻辑K和KDCL联盟逻辑GML分级模态逻辑PML概率模态逻辑HML亨尼西-米尔纳逻辑G. Calin等人/理论计算机科学电子笔记231（2009）4151函数flatten;例如flattenSeg产生了粘合剂[FlatUnaryHML1，FlatUnary PML0]其中非负整数作为排序名称。我们将上面的表达式理解为胶合上一节的。（s0→HML（s1），s1→PML（s0））给定一个可证明的粘合G，函数调用gen G然后为文件MySat.hs中与G相关的逻辑生成可证明性检查器。这个文件特别定义了组合逻辑的语法，并包含了组件逻辑的匹配例程的副本，通过调整它们的类型来重新连接，以适应粘合的结构。这个过程由多参数类型类控制，这些类体现了这样一个事实，即匹配函数现在连接了潜在的不同逻辑。一般来说，每个arity需要一个这样的类型类;由于典型应用中出现的特性往往最多是二进制的，CoLoSS目前仅实现了两个类，分别用于一元和二进制特性，并具有以下接口声明：class（Logicf， Logic g）=>UnaryMatch f g |f-> g其中matchu：：条款f->[[g]]class（Logicf， Logic g，Logic h）=>BinaryMatch f g h |f-> g，f -> h，其中matchb：：条款f->[（[g]，[h]）]这里，我们使用Glasgow Haskell扩展之一，即函数依赖[7]f ->g等，其指示对于给定的源逻辑F至多存在一个实例。这特别允许在多态函数中使用类约束，例如UnaryMatchfg，其类型不提及g。我们使用这个功能来实现多态可证明性功能，根据手头的特征的arity，例如。对于二进制特征probable2：： BinaryMatchf g h =>f-> Boolprobable2 phi =设both（as，bs）=（allprobable as）（allprobablebs）inall（\c->any（\pair-> both pair）（matchbc））（cnf phi）可证明性函数的这些arity特定的实现与逻辑类接口中可证明的单个可证明性函数相关联，如上所述，在其上进行递归调用，而不必保持arity的进一步记录。注意Haskell类型推断的利用，以确保各个可证明性函数的正确连接。由于逻辑特性可以在一个实例中多次使用，CoLoSS使用运行索引来消除同一特性的潜在重复实例的歧义。对于Segala系统，CoLoSS生成以下语言定义：数据L0 =（命题连接词）|HML0字符L152G. Calin等人/理论计算机科学电子笔记231（2009）41数据L1 =（命题连接词）|PML1合理性L0（省略派生子句）。这里，Hennessy-Milner逻辑的模态算子Qa表示为HML 0如第3节所述，一个公式是可证明的，只要它的合取范式的每个组成部分允许至少一个匹配本身是可证明的。对于二进制要素，这需要匹配生成一对公式，然后必须如上所示检查其可证明性这一点得到了认可。例如，在用于上述交替系统的胶合Alt实例BinaryMatch L0 L1 L2，其中matchb（Clause（pls，nls）） =设f1=（disj$ striplst pls）\/（ndisj$ striplstnls）f2=（disj$ striplst pls）\/（ndisj$ striplst nls）在[（[f1]，[f2]）]其中NDISJ产生给定列表中注意，上面的matchb类型是：匹配b：：条款L0->[（[L1]，[L2]）]在简单的Segala系统的逻辑中，由胶合Segg定义，公式Qi（L0. 8Qip0→ L0。5Qip0）现在可以写成框(with语法糖dia c phi= neg（HML 0c（neg phi））和boxc phi= HML 0c phi（对于HML box和diamond），l= PML1（对于概率Lp算子），p1（对于命题变量）。CoLoSS正确地发现这个（公认的简单）公式是可证明的。作为第二个例子，我们考虑概率联盟的逻辑，其中代理人的联盟只能强制概率分布的事实。这通过上面的胶合PC（对于预聚物联盟）来表示我们得到了一个类似于Segala系统逻辑的双排序语言Lc3φ：：= T|φ1∧φ2|¬φ|[C]（联合公式;n∈ Lp，C<$N）Lp3：：= T|ψ1∧ψ2|¬ψ|L q φ（概率公式;φ∈ Lc，q∈[0，1]<$Q）其中N是第1节中的所有代理的集合。 使用模态算子和命题变量的语法糖，我们可以检查公式phi= cbox[0，2， 4]（l 0.5 p0）/\cbox[1，3， 5]（l0.5 p1）--> cbox[0，1，2，3，4， 5]（10.25（p0/1p1））它断言，两个不相交的联盟可以联合起来，G. Calin等人/理论计算机科学电子笔记231（2009）4153他们各自的收益与各自概率的乘积。 然而，在这方面， 由于命题变量p0和p1（的表示）通常不是独立事件，因此这个公式是不可证明的（尽管当然是可满足的）。然而，如果我们指定，在p0和p1各自概率的给定下界下，p0和p1的合取至少以概率成立0。4在战略博弈的每个后续状态中，通过公式psi= cbox[]（（l 0.5 p0）/l（l0.5 p1）-->（l 0.4（p0/lp1）那么公式φ--> psi确实是可证明的。5结论我们已经设计和实现了Coalgebraic Logic Sat-iability Solver CoLoSS，它为各种模态逻辑的满足性/有效性检查关键的实现细节包括使用Haskell类机制来支持单个逻辑的泛型，以及促进逻辑模块组合的代码生成机制。CoLoSS在其目前发展阶段的主要目的是提供概念验证。该工具的状态在很大程度上是实验性的，并且在总体设计方面正在探索替代选项，特别是关于逻辑组合的处理和模态逻辑的类接口。有一些并行的发展，这两个分支正在完全合并的过程中;特别是，一个通用的模态逻辑解析器已经可用，并将很快与该工具集成，从而取代目前直接输入公式作为Haskell代码的风格（但是请注意，将公式直接表示为代码是一种历史悠久的做法;例如，RACER [3]的默认文本界面期望公式作为LISP代码。未来开发的一个主要主题是提高工具的通用部分和特定逻辑实例的效率。 一般优化将主要关注命题方面;人们可以移动到适当的命题表格并采用启发式优化策略，如[6]中描述的策略，或者将公式中的命题层有效地表示为二元决策图。要探索的逻辑专用算法包括使用（整数）线性规划工具来减少分级和概率模态逻辑的搜索空间。一旦这种优化策略到位，基准测试将成为一个问题。预定义的基准套件，将允许评估该工具的性能在其主要的预期应用领域，即非Kripke模态逻辑，似乎很难得到。因此，这种基准的设计是未来研究的一个重要课题引用[1] 克利尔斯泰亚角 和D. 帕廷森，《现代逻辑的现代建构》，《理论》。Comput. Sci. 听我说。早期版本在P. Gardner，N. Yoshida，editors，Concurrency Theory，CONCUR 04，vol. 3170 of Lect. 注释计算Sci. ，页。25854G. Calin等人/理论计算机科学电子笔记231（2009）41[2] Demri，S. 和D. Lugiez，Presburger模态逻辑只是PSPACE-完全的，在：U. Furbach和N. Shankar，editors，Automated Reasoning，IJCAR 06，Lect. Notes Arti Official Intelligence4130（2006），pp. 541-556[3] 哈斯列夫河谷 和R. Mller，R ACER系统配置，in：R. 去吧A Leits ch和T. Nip kow，编辑，自动推理国际联合会议，IJCAR 2001，Lect。注释计算Sci. 2083（2001），pp. 701-705[4] Hansson，H.和B.琼森，一个演算通信系统的时间和概率，在：实时系统，RTSS 90（1990），pp. 278-287.[5] Heifetz ， A. 和 p.Mongin ， Probabilistic logic for type spaces ， Games and Economic Behavior35（2001），pp.31比53[6]霍罗克斯岛和p.F. 张文，描述逻辑包容的优化设计，北京大学出版社，2001。逻辑计算9（1999），pp. 267-293。[7] 琼斯，M。P.，类型类与函数依赖，在：G。Smolka，编辑，欧洲编程研讨会，ESOP 2000，Lect。注释计算Sci. 1782（2000），pp.230-244。[8] Jonsson，B.， W. Yi和K. G. Larsen，过程代数的概率扩张，在：J。伯格斯特拉，A. Ponse和S. Smolka，editors，Handbook of Process Algebra，Elsevier，2001 pp. 685-710.[9] Larsen，K.和A. Skou，通过概率测试的互模拟，通知。Comput. 94（1991），pp. 1- 28[10] 诺雷尔，美国和p.Jansson，Polytypic programming in haskell，in：P.W. Trinder，G.迈克尔森和R. Pena，编辑，函数式语言的实现，IFL 2003，Lect。注释计算Sci. 3145（2003），pp. 168-184。[11] Olivetti，N.和G. L. Pozzato，CondLean：A theorem prover for conditional logics，in：M. C. Mayer和F.Pirri， 编 辑 ， 自 动 推 理 与 分析 表 和 相 关 方 法 ， TABLEAUX 2003， Lect。 注 释 计 算 Sci. 第2796（2003）号来文，第2796（2003）页。264-270。[12] Pacuit，E.和S. Salame，Majority logic，in：D.迪布瓦角韦尔蒂和M.- A. Williams，editors，Principlesof Knowledge Representation and Reasoning，KR 04（2004）. 598-605[13] Pauly，M.博弈中联盟力量的模态逻辑，J。逻辑计算12（2002），pp.149比166[14] Peyton-Jones，S.，编辑，“Haskell 98语言和库-修订报告”，剑桥，2003年，也：J。方案编制13（2003年）。[15] 塞赫罗德湖 和D. Pattinson，PS PACErasoningforrank-1modall ogic s，in：R. 2006年，IEEE，LICS06，编辑，Logic in Computer Science，pp. 231 arxiv.org/abs/0706.4044[16] 塞赫罗德湖 和D. 张文，等.基于遗传算法的多目标优化问题的研究. 阿尔杰，A. Tarlecki和C. Cachin，编辑，自动机，语言和编程，ICALP 07，Lect. Notes Comput. Sci. 第4596（2007）号来文，第4596（2007）页。459-471[17] 塞加拉河“随机分布式实时系统的建模和验证”，博士。论文，麻省理工学院（1995年）。[18] 塞加拉河和N. Lynch，Probabilistic Simulations for Probabilistic Processes，Nordic Journal ofComputing2（1995），pp. 250-273。[19] Sirin ， E. ， B. 帕 尔 西 亚 湾 C. Grau ， A.Kalyanpur 和 Y.Katz ， Pellet ： A practical OWL-DLreasoner，J. Web Semantics.出现。[20] Tsarkov， D.和I.霍罗 克斯 ，FaCT++描述 逻辑 推理机 ：系 统描述 ， 在： U。 Furbach和N. Shankar，editors ， Int. Joint Conf. on Automated Reasoning ， IJCAR 2006 ， Lecture Notes in Arti FicialIntelligence4130（2006），pp.292-297.