多值逻辑的经典归结

可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）253-270www.elsevier.com/locate/entcs多值逻辑的经典归结若昂·马科斯1LoLITA信息学和应用数学系，UFRN，巴西克劳迪娅·纳隆巴西巴西利亚大学计算机科学系摘要我们提出了一个基于分辨率的证明方法，基于算法的减少过程，表示这些逻辑的二价语义的有限值命题逻辑。我们的方法是混合使用一些内部元素和其他外部元素的多值逻辑考虑，因为我们嵌入到一个更有表现力的元语言来处理满意度问题。与以前解决同一问题的方法相比，我们的目标语言是完全经典的，这使得为特定的多值逻辑设计基于解析的规则成为一项简单的任务。正确性的结果，这是证明在本研究中，很容易从结果的经典决议。我们举例说明了该方法的应用，并评论其实施，很容易实现直接翻译成经典的命题逻辑，利用可靠的现有自动证明。关键词：多值逻辑，二价语义，归结方法1介绍多值逻辑学刚刚庆祝了它的百年诞辰，而被称为归结的计算证明方法现在也在庆祝它的半个世纪生日。虽然在[2]中可以找到对多值逻辑的适用性的全面概述，以及其中的参考文献，但在其他地方已经深入讨论了这种逻辑的不同自动证明方法（参见[12]和[6]）。在可用于处理多值逻辑的各种证明过程中，[1]和[7]中详细描述的基于分辨率的方法特别令人感兴趣，并且与本文介绍的方法非常接近。然而，后两篇论文都提出了基于子句归结的程序，将特定多值逻辑语言中的公式作为输入，并将其转换为1本文中报告的研究属于欧盟FP 7 Marie Curie PIRSES-GA-2012- 318986项目GeTFun：概括真理功能的范围。第一作者进一步承认CNPq的部分支持。http://dx.doi.org/10.1016/j.entcs.2016.09.0011571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。254J. 马科斯角Nalon/Electronic Notes in Theoretical Computer Science 323（2016）253标签公式标签用于在句法层面上反映真值，并旨在表示满足公式的语义条件归结推理规则适用于包含互补文字的子句这些证明方法之间的主要区别在于标签的形式：在[1]中标签是单例，而在[7]中标签是符号集。在目前的调查中，我们采取了类似的路线。要测试满足性（不满足性）的公式也被转换为标记子句，也就是说，推理规则被应用于一种更有表达力的语言，在这种语言中，语义概念是明确的。然而，标签在所有情况下都采用非常简单的格式，只是两种可能的符号中的一种。因此，与[1，7]中的方法不同，标签上的统一可以很容易地被视为等同于经典比例分解的普通应用此外，对不一致性的搜索（在给定的多值逻辑语言中）采用经典元语言中的超分辨率推理规则的形式，允许在算法上构造统一的类经典方法将公式转换为标记语言依赖于作者之一[4，5]以前的结果，为了使表述自包含，在此对这些结果进行简要的综述。本文的组织结构如下。第2节从语义的角度抽象地介绍了逻辑，解释了它们都可以用二价语义来表征，然后重点讨论了有限值真值泛函逻辑。重点放在标准的（双边）概念的逻辑后果，而不是对方法的多值逻辑是基于纯粹的组合操作的有限值代数。第3节解释了一种算法，它允许人们用一种完全经典的元语言来描述有限值逻辑，在这种元语言中只使用两个提供一个证明理论的角度来看，这需要一个概括的方式，句法复杂性的测量，以允许分析演算从这样的描述中提取。下一节是我们的主要贡献。第4节致力于为任意给定的有限值逻辑建立一个通用的基于归结的证明方法。第4.1小节展示了如何将上述二价描述转换为更适合应用归结的小句格式。相应的转换增加了新的变量符号，这些符号有助于对原始语句的结构进行编码，保持并重新定义它们的可满足性。作为输出，我们获得了更好地利用上述广义复杂性概念第4.2小节介绍了超归结证明方法的推理规则，该方法适用于由后一转换产生的子句。这种方法介于内部证明系统和外部证明系统之间，内部证明系统利用原始逻辑的语法特征，外部证明系统在经典逻辑框架中对逻辑进行形式化推理。最后，我们对已经取得的成就以及如何进一步扩大目前的调查发表一些评论。J. 马科斯角Nalon/Electronic Notes in Theoretical Computer Science 323（2016）2532552每一个多值逻辑都是二价的这一部分将我们目前的研究置于语境中，并从抽象和语义的角度解释我们所说的特别关注的是真值函数的情况。我们还在这里介绍了一个适当的经典Meta语言，用于描述赋值的集合，并且在下面的部分中，我们将讨论如何使用它来实现所谓的Suszko定义2.1[1]设一个（命题的）签名是构造函数的一个家族的联合，其中每个集合的集合只包含函数集m的函数集，并且其中假设当i ≤ j时，i和j是不相交的。设A是一个可分解的符号集合，称为（原子）变量，假设与签名不相交。 空值符号有时被称为真值符号。 一 个（命题）语言S是递归生成的，在通常的方式，通过考虑它的composite为mula是形式dp0，1， . 。 ，mq，对于so md Pm`1。在后一种情况下，符号d被认为是头连接词，公式k，f或0 km，a被称为dp0，1， . 的 直 接 子 模 。 ，Amaramq. AY0中的公式被称为非复合的，没有适当的子公式. 公式复杂度cp：S N的一个规范概念可以通过设置cppq “0，如果N是非复合p o site，以及cp p q“1 ` Ma x 0 k m cp p k q，如果n是复合的，并且0 k m的k是它的直接子公式来定义。一致替换是公式集上的自同态，它将每个构造函数映射到自身;一旦语言的变量映射到公式中，它就被唯一地定义。我们用rps来表示在公式中每次出现变量p时一致代入的结果。L在本研究中，我们将只考虑由有限签名生成的语言。定义2.2[逻辑]对于一个固定的命题语言S，逻辑L在这里被定义为一个结构xS，<$Ly，其中关系<$L<$2S<$S代表以下四个抽象公理，对于任意的ΓYΔY t<$S：（C1）若P为r，则r为L，（C2）如果Γ<$L <$，则ΓY Δ<$L <$（C3）若对每一δPΔ，且Δ<$L<$， Γ <$Lδ，（C4）若Γ<$L <$，则对任意一致代换ε，εpΓq <$Lεp<$q任何关于前三个公理的关系称为塔斯基推论关系。我们称替换不变性为最后一个公理所描述的性质。我们说，公式α和β是L-等价的，并将其表示为αX：<$，如果<$是基本公式。（τ b）子句以简化形式保存，即以下简化规则适用于转换的所有步骤（其中D是子句，而D是基本公式）：σpD||X：||X：qσpD ||X：qσpD ||jqjσpD||X：||Xc：jσpD ||kqσpDq下面的引理表明转换成CNFBS是正确的。引理4.1LetL是一个有限值逻辑，S是它的语言。LetBpL，Bpθq是与L关联的二价语句的集合，并且分离等式Bpθ，nd设λ是S中的一个公式。 当且仅当τ pT：q满足时，是满足的。证据由τ给出的重写规则是基于[ 5 ]中给出的等价式（τ×d的情况），基于所有其他重写规则（τ&，τ）的经典等价式||,τùñ&,andτ ùñ), and on classical renaming for the266J. 马科斯角Nalon/Electronic Notes in Theoretical Computer Science 323（2016）253transformation rule τ ren. 由于两种类型的转换，即替换和重命名，保持满足性（参见。[9]），我们得出结论，当且仅当τp T：τ q也是可满足的，则τ p T：τ q是可满足的。 LJ. 马科斯角Nalon/Electronic Notes in Theoretical Computer Science 323（2016）253267ÝÑ1 .一、 T：t1||T：t9二、 F：t1||T：t2||T：t8||T：p3 .第三章。 F：t1||F：p四、 F：t2||T：t3||T：t65. F：t2||T：θppq第六章 F：t3||T：p第七章 F：t3||T：t4||T：t5八、 F：t4||学生 ： 第 9 页 。F：t5||θppq10。F ： t6||θppq11.F：t6||T：t712个。 F：t7||T：p13岁 F：t8||T：p14个。 F：t8||T：t715个。 F：t9||T：t3||T：t6||θppq十六岁 F：t9||F：θppq，其中图二. pppppKqqpqpq的小句形式。例4.2对于公式0“ppp p p p K q p q p q，在L - 3中是v a lid。 图图2示出了从F：θ0到CNF BS的变换产生的子句集合，其中变换函数基于L-3的具有图2中的分离序列xθ0，θay，gi ven的双变量状态集合。1.一、 自动化已经被压制。在右边，我们给出了沿着平移引入的新原子变量的定义。L4.2推理规则设BpL，λpθq是有限值逻辑L在语言S上的双值描述，对于λ P N，tUjujPλ，是该描述中的U-状态族. 设X是一个标号公式，其上有PS.令Φ是通过基 于 B pL ， θq 将X：λ变换成对应的CNF BS而获得的子句集合。L的解析演算将包括二进制解析规则（RES），其是一个语法解析规则。本文提出了一种新的超分辨推理规则（RESUj），用于处理与Uj-状态相关的赋值限制。 高分辨率（参见 [10]）是分解方法的改进，它结合了几个二进制分解步骤，从而避免了在搜索证明时生成中间子句（以及它们之间的相互作用）。回想一下，U-语句表示的是二进制序列，而这些序列是无法作为L的原始真值的二进制打印来获得的。因此，在一个U-语句中的元蕴涵的左手边的标记公式的元合取对应于元语言的语义中的逻辑荒谬。图中给出了解析规则 其中Di是子句，XiPtT，Fu，F_i，F_i是基本公式（其中1 ∈ i ∈ n j，j Pλ，n j是U_j 中元合取的个数）. 基于归结推理规则的前提称为父子句。这些规则中的结论称为预解式。此外，我们指的是tT：，F：u（分别为 tX1：101，.，X nj：nj u）发生在（RES）的父子句中（resp. （RESUj））作为不一致的公式集。在一个不一致的公式集合中的标记公式被称为是由相应的推理规则解决的。新变量重命名t1T：ppp p Kqqpq F： p&t2F：pp <$ p <$KqqT： θp pq&t3T： p F：pp Kq&t4T： p F：K&t5T： θp pq F： θpKq&t6T： θp pq F： θp p <$Kq&t7T： p F： θpKq&t8T： p F： θp p <$Kq&的t9T： θppp p Kqqpq F： θp pq&268J. 马科斯角Nalon/Electronic Notes in Theoretical Computer Science