通过矩阵计算的哥德尔-达米特模型及其应用

理论计算机科学电子笔记125（2005）137-148www.elsevier.com/locate/entcs通过矩阵计算的哥德尔-达米特模型Dominique Larchey-Wendling1LORIAVanduvre-l`es-Nan cy，France摘要本文提出了一种判定哥德尔-达米特逻辑的新方法。它从一个模板开始，分三步进行。 首先根据公式的分解树构建一个条件图。然后尝试通过实例化这些布尔条件来删除这个图中的一些循环。 如果这是可能的，从这样的实例图中提取反模型。否则，初始公式是可证明的。我们强调通过矩阵计算，布尔约束求解和反模型提取循环去除。保留字：反模型，条件图和矩阵。1介绍哥德尔-达米特逻辑LC是介于经典逻辑和直觉主义逻辑之间的以线性Kripke模型为特征的中介逻辑它是由Güodel在[10]中引入的，后来由Dummett在[6]中引入。它不是研究最多的中间逻辑，原因有几个：其中，它是最简单的“多值”逻辑之一，其语义由单位区间上的它是模糊逻辑的候选者之一（以“哥德尔”逻辑的名义）。关于中间逻辑的决策过程，它证明了超演算系统的一些优点。1 电子邮件地址：larchey@loria.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.07.022138D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137GG⊥⊥LC中的证明搜索得益于直觉逻辑IL中证明搜索的发展，其中有两个重要的种子：Dyckho的无压缩演算[1，7，8]和Avron的超压缩演算[2，14]。最近的两个贡献提出了一个类似的方法，基于一组局部和强可逆的证明规则（对于微积分[12]或超微积分[2]）和一个语义标准来决定不可约（超）序列并最终建立一个反模型。我们最近提出了一个组合的证明-搜索在campical-culus和反模型的建设，以提供一个决策过程的LC，这是基于一个新的原则：我们能够收集所有有用的信息-形成所产生的所有证明-搜索分支到一个语义图，然后我们使用一个有效的反模型搜索算法的基础上循环检测。我们已经减少了LC的决策问题的布尔约束求解和循环检测的组合。 这些结果已在[13]中给出，本文是对[13]的补充，我们将简要回顾理论结果，但我们想主要集中于决策过程的描述，重点是反模型生成算法。给定LC的公式D，该过程以三个步骤进行， 最后得到一个反模型（在D不可证明的情况下）。2）第一步，在第3节中详细描述，包括基于D的分解树构建一个特定的双色图D。该图的箭头可以用布尔条件来索引。第二步是搜索箭头上布尔条件的实例化，使得实例图没有剩余的r-圈。[3]这一步在3.3节中进行了非正式的描述;然后我们在第4节中提供了一个基于条件矩阵计算的决策算法。对于第三步，在第5节中描述，给定一个特定的实例Gv，没有r-循环，我们可以从这个实例中提取D的反模型v计算一个双高度的。2哥德尔-达米特逻辑的语法与语义命题公式的集合，记为Form，是从一组由Var表示的命题变量开始，使用连接词归纳定义的。，4IL将表示在任何中可证明的公式的集合-2作为一种判定程序，它也可以在有证明的情况下证明D的有效性[3]这是一种循环，将在第6节中描述。4我们不对底部常数进行积分。 具体的治疗方法详见[12]。它可以很容易地集成到这里描述的过程中。D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137139DDL L联系我们tuitionistic命题演算（见[7]）和CL将表示经典有效的公式。通常，中间命题逻辑[1]是一组公式满足IL CL，在常现式规则和任意替换下是闭的。LC是满足公理（X<$Y）<$（Y<$X）的最小中间逻辑。在语义方面，LC的特点是线性Kripke模型。 在这在本文中，我们将使用LC[2]的代数语义表征而不是Kripke语义。代数模型是一组自然数，其自然阶≤，用一个gre检验元素∞增广。一个间-命题变量的命题[·]：Var→N被归纳推广为公式：合取式由表示为最大值函数的析取和算子的蕴涵定义为b =如果a≤b则∞，否则b。 如果等式[D]] =∞成立，则公式D对于[·]的解释是有效的。这种解释对于LC是完整的。一个公式D的反模型是一种解释[·]]，使得[D]] <∞。3信用证的决策程序在[13]中，我们描述了一个确定LC公式的过程，并在公式无效时建立一个反模型。这个过程的第一步是用两种箭头构建一个图。然后，决策问题被简化为检测该图中的特定循环3.1条件双色图的构造我们介绍了我们使用的图的确切概念，然后展示了如何建立这样一个图的LC公式。定义3.1双色图是一个（有限）有向图，有两种箭头：绿色箭头表示→，红色箭头表示。定义3.2条件双色图是一个双色图，其中箭头可以用（命题）布尔表达式索引我们指出，我们认为这些布尔表达式的经典等价，即我们认为他们作为代表的原子命题变量的布尔函数。这些变量可以通过{0，1}，赋值为v，布尔表达式为e，得到值ev0、1个以明显的方式计算。这样我们就得到了一个实例图：用布尔表达式e索引的箭头属于这个实例当且仅当ev= 1。无条件（即未索引）箭头可以处理140D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137⊃ − XXXxB−+GGVF∧ ∨⊃FVV∧−XXA−B−∧A+B+V∨−♦A−B−A+∨ ⊃XXA+B+Fig. 1. 信用证的反模型搜索系统通过考虑它具有同义反复的隐式布尔条件（并且总是值1），并且不存在的箭头具有总是值0的隐式布尔条件。定义3.3给定条件双色图G和{0， 1}中布尔变量的赋值v，我们将实例图Gv定义为双色图当一个人评估布尔表达式时得到的一个图，该布尔表达式对数组进行索引，并精确地保留那些赋值等于1的数组。给定LC公式D，我们通过以下过程构建条件双色图GD。首先，通过考虑D的分解树的节点集合，或者等价地，子公式的出现集合，来获得D• 如果F是D的一个子公式的出现，我们用XF表示相应的结点。 节点从根D-处的-开始有符号，并像往常一样传播符号。[5]我们可以写X+或X-来强调符号。• 对于这个节点集，我们为D中出现的每个命题变量V添加一个节点V。因此，V的多次出现只会生成一个节点V，但会生成多个X+或X−节点。• 我们添加一个新的节点，用表示。然后，得到D的边如下：我们描述了一组连接这些节点的绿色和红色箭头以及索引这些箭头的布尔表达式。我们从无条件箭头开始（即，箭头隐式地索引有独立于公式D的内部结构引入的重言式1）：• 我们将来自r o o t n o de的（无条件）红色owXD−o加到o。• 对于一个变量的概率V，我们得到绿色的概率wV→XV−。• 对于变量的正出现V，我们添加绿色箭头X+→V。这三条规则总结在图1的左边部分。现在我们考虑5连接词和保持符号，并保持右子公式的符号，并反转左子公式的符号。D−♦V+V−XA−x B+++D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137141GGCGG一CBCB一B一B内部节点的箭头引入规则。 第一，无条件的情况：• 对于子公式的正出现C <$A<$B，我们添加两个以下绿色箭头X +→X+和X + →X+。• 对于一个子公式的一个负出现C <$A<$B，我们添加下面两个绿项：XA−→XC−和XB−→XC−。我们继续使用条件箭头。这些箭头是用选择器索引的，即形式为x或x的布尔表达式，其中x是布尔命题变量。对于每一次出现的子公式，我们引入一个新的布尔变量。6• 对于一个子公式的负出现C <$A <$B，给定一个新的布尔变量x，我们可以导出两个条件绿数：XA−→xXC−和XB−→xXC−。• 对于子公式的正出现C<$A<$B，给定一个新的布尔变量x，我们引入两个条件绿色箭头X+→xX+和C A++XC→xXB。• 对于子公式的负出现C<$A<$B，给定一个新的布尔值变量x，我们将得出以下两个值：机翼绿弦XB−→xXC−→xX −以及后面的两个红色箭头X −和• 对于子公式的正出现C<$A<$B，给定一个新的布尔值变量x，我们引入以下两个绿色箭头X+→xX+和C BX− →xX+。所有为内部节点引入（非）条件箭头的规则（对应于对应于D的非原子的子式）总结在图1的右边部分。给定这个过程，应该清楚的是，从公式D构造图D需要线性时间，因为对于D的子公式的每个实例，最多引入四个箭头。D的有效性与在GD的例子中某些特殊圈的存在性。定义3.4双色图中的r-圈是由绿色（→）或红色（→）箭头组成的圈，其中至少包含一个红色箭头。等价地，它是形式l（→+ n）n nn l的链。定理3.5设D是LC的一个公式，D是它的一个条件双色图，由前面描述的过程建立。 则D在LC中可证明当且仅当每个实例图v至少包含一个r-圈。6用子公式出现次数为这些变量编制索引是确保唯一性的一种方法142D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137G.Σ⊃ ⊃⊃⊃1154--45361402143414这个结果在[13]中得到了证明。因此，为了反驳D，我们必须找到一个不包含任何r-圈的实例图v让我们举一个例子。3.2图构造示例我们考虑经典有效的皮尔士公式（（A B））的情况下， A）、 A.它在任何中间逻辑中都是不可证明的，但在经典逻辑中，所以特别地，它应该在LC中有一个反模型。我们将这个公式的索引如下：（A+−B−）+A+−A−。We结构其关联的条件图：• 我们加上了ow−0。• 我们有两个变量A和B，分别代表4 oc-所以我们加上A→A−2，A+→A，4+−A5→A和B→B6。• F或内部n ode−0，我们生 成 一个新的布尔变量x，并添加四个条件布尔变量A−2→x−0，→x−0，A−2x+和A−2x。• 对于内部节点+，我们选择一个新的布尔变量y，并添加两个条件变量+→yA+和−→yA+。• 对于最后一个内部n ode−3，我们选择一个新的bo oolean变量z，并添加四个条件A：B6−→z−3，→z−3，B6−zA+和B6−z。3.3r-圈的朴素消去我们现在必须在0， 1中找到一个值vx，vy和vz为此，我们确定所有的r-循环，并试图找到一个同时打破每个r-循环的估值。我们只考虑不重复节点的基本r-圈，因为任何r-圈至少包含一个基本r-圈。我们发现其中四个−0−0A−2<$x<$$> →z<$−3→yA+→A→A−2A−2<$x<$+→yA+→A→A−2z⊃−0X♦XX⊃1+X一个2−yz⊃−3yA+4zA+5zB−6B一D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137143G→0123456AB♦0 123456AByXy11z11Xz⇒0123456AB♦0 123456AB1XXzz图二、Peirce公式的条件矩阵第一个r-循环被破坏，当且仅当条件x= 0被满足，这等价于满足x。 第二个r-圈被破坏当且仅当条件z+y+x满足。[7]第三个r-循环仅在x+z+y满足的情况下被打破，最后一个r-循环在x+y满足的情况下被打破为了在一次估值中打破这四个r循环，我们寻找一个估值v，它满足x·（z+y+x）·（x+z+y）·（x+y）。这就给出了唯一的解：vx= 1，vy = 0，vz = 1。然后，读者可以验证从该估值获得的实例图v 参见第5节，了解这个图的表示和皮尔士公式的相关反模型我们描述的计算没有r-圈的赋值的朴素过程包括搜索所有可能的r-圈（没有重复节点）和求解与这些圈相关的布尔约束系统。不幸的是，这样的程序将是非常不明智的，因为可能有对于给定的公式，有许多R-圈。[8]这个问题在[13]中也得到了解决。在下一节中，我们将描述一种可能的消除r循环4条件双色图在3.1节中，我们引入了条件双色图的概念。表示有向图的一种自然方法是考虑7我们用+表示布尔析取，用·表示布尔合取。[8]例如，（（X1<$X1）<$（X1<$（X2<$X2））<$··<$（Xn−1<$（Xn<$Xn）））<$Xn有一个相关的条件双色图，包含2n+1−1个（基本）r-圈。144D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137--GS×→⇒·→ ⇒⇒条件矩阵的sum → + sum，pr o duct → sum·sum与条件矩阵的rexexi v e andtr（M）=xMx，x. 当布尔选择器在条件内实例化时，当且仅当tr（→+）0：tr（v+v）v没有R循环。--潜在的关联关系。通常，这些矩阵取布尔代数0， 1中的值，并且单元（i，j）中的1意味着从节点i到节点j有一个箭头。4.1条件矩阵为了表示条件双色图，我们使用条件矩阵：这些矩阵的单元从布尔函数集合中获取其值。这些函数由布尔表达式表示，布尔表达式是由条件图构造过程中引入的布尔选择器构建的定义4.1大小为k的集合上的条件矩阵是一个k k-数组，其值在选择器集合上的自由布尔代数中。对应于绿色（）和红色（）箭头的双色图有两个关联关系。因此，一个条件双色图可以用一对条件矩阵来表示。我们对（条件）关联关系及其相应的矩阵使用相同的表示。所以GD由一对（→，）条件矩阵表示。 图2呈现对应于图的两个矩阵当D是皮尔士公式时第3.2节。我们只写其值不同于0的单元：矩阵是稀疏的，因为非零单元的数量是线性的，而单元的总数是二次的。4.2作为迹计算的R-圈去除合取（或乘法）和析取（或和）+的布尔运算符自然地扩展到条件矩阵。 所以我们可以考虑transiti veε闭包→ε=i0→i. 我们还可以导出矩阵的迹函数矩阵，我们得到一个值在 0、 1个 也就是发病率对应实例图的视图。 此外，实例化矩阵的代数运算。 这导致以下结果：定理4.2设G =（→，n）是一个用条件点表示的条件双色图. 马特里切斯。re在Gv的每一瞬间都存在r-圈= 1保持。此外，当布尔函数tr。（→+）不是同义反复，在那里。在{ 0，1 }中的选择器上存在一个valuatio n v，使得此跟踪具有值= 0。然后，对应的实例图Gv具有D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137145××→ ⇒ ⇒ → ⇒⇒我5现在的问题是有效地计算这个轨迹。让我们固定一个大小k>0的矩阵。设I表示单位kk矩阵（否则Ix，x= 1，Ix，y=0）。 设M是任意条件kk矩阵.则M=（I+M）k（因为任何大小为k+ 1的路径都包含大小为k的子路径）。 此外，当I≤I+ M（按单元）时，I，I+ M，（I+ M）2. 是条件矩阵的（逐点）递增序列，其在至多k步中稳定。为了计算（+）β ，我们计算α = I ++和β =，然后递增序列β，αβ，α2β，α3β，. 直到它稳定在αβ。这可以在β上逐列进行。 设βi表示β的第i列，则α<$βi是α<$β的第i列。皮尔士公式第1列的计算β1αβ1α2β1α3β1α4β1α٨β1X.Y.Zx x xXxX xxxxxxxxxxx.y.z x.y.zβ的大多数列只包含0，在这种情况下不需要计算：定点就是这个零列。在Peirce的例子中，只有列1，5和10包含不同于零的值当计算迹线时，可以在β的列之间共享计算。设T是每个单元上由1组成的列矩阵我们考虑以下序列：t0= 0且ti=<$α<$（ti−1T+βi）<$，i = 1，.，K. 则tk= tr（α<$β）。例如，在皮尔士公式的情况下，我们得到t0= 0然后t1=x.y。列β2、β3和β4为空（即，包含所以t2=t3=t4=t1=x.y。则t5=，我们得到t5=x.y.那么列β6，βA和βB是空的，并且t6=tA=tB=t5=x.y。α0123456AB♦01 213456AB11XyX1X1y111z1z1z1111Xz1146D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）137GD D D D DD♦⊃1+A+5一A−2⊃−0BB6−⊃−3A+4最后我们计算t_n=α_n（x. y.T+β（？）. 设γ=x.y.T+β：α0123456ABγαγα2γα3γα٨γ0 111y2XX131y4 15 111X.YXxX.Y1x.y1x.y1x.yx.yX.YX.Y1x.yx.yx.x1公司简介1公司简介6z z 1zx.y+z x.y+zx.y+zx.y+zx.y+z的1Bxz1x.y11x.y1x.yXx.y+zx+x.yXx.y+zx+x.yXx.y+zx+x.yXx.y+zx+x.y+x.z我们得到t= x + x.y + x.z。这是α的迹，它不是重言式。唯一证伪这个迹的赋值是vx= 1，vy = 0，vz = 1。这当然与我们在3.3节中手工（通过查找r-圈）得到的估值相同。5反模型提取现在我们解释如何从相应的实例双色图v中提取反模型。读者可以很容易地检查它是否可以表示为：在这个图中，红色箭头总是严格向上爬，绿色箭头永远不会向下，所以不可能存在r循环。反模型非常容易计算：给出变量A和B在这个图中的高度。所以[A]] = 1和[B]= 0是皮尔士公式的反模型<现在我们解释如何在一般情况下从缺少r-圈的实例图中提取反模型。我们基于双高度的概念给出了缺乏r-圈的特征：♦D. Larchey-Wendling/Electronic Notes in Theoretical Computer Science 125（2005）1371471♦⊃450定义5.1设G是一个双色图。一个双高度是一个函数h：G →N使得对任意x，y∈ G，若x→y∈ G则h（x）≤h（y），且若x∈y∈G则h（x）

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