命题逻辑证明图的正规化

可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）181-196www.elsevier.com/locate/entcs命题逻辑证明图的强正规化Marcela Quispe-Cruz1UniversidadCat'olicaSanPablo（Peru'）爱德华·豪斯勒2里约热内卢大学（巴西）Lew Gordeev3图宾根大学、根特大学摘要命题逻辑的传统证明理论处理的是规模巨大的证明。证明理论研究发现正常或切割自由证明和他们各自的非正常证明之间的指数差距。使用证明图，而不是树或列表，来表示证明在证明理论家中越来越流行。证明图是研究命题证明的复杂性和提供更有效的定理证明器的一种方法，涉及命题证明的规模FPL图最初是为最小蕴涵逻辑开发的，通过引用而不是复制来表示证明。因此，保留在图结构中的公式和子演绎可以被共享，删除不必要的子演绎，从而减少证明。在这项工作中，我们考虑充分的最小命题逻辑，并显示如何减少（消除最大公式）这些表示，强规范化定理可以证明通过简单地计数在原始推导中的最大公式的数量。在证明图中，使用这种简单的复杂性度量来获得强规范化属性的主要原因是每个公式在证明图中只出现一次，并且通常出现在树形式推导中的隐藏最大公式的情况已经在fpl图中表示。关键词：证明理论，证明图，N-图，直觉逻辑，序列演算，多结论系统。1介绍最近，使用图而不是树来表示证明已被证明是更有效的[2][1]，同时也有助于更好地解决缺乏对称性的问题1电子邮件：mquispec@ucsp.edu.pe2电子邮件地址：hermann@inf.puc-rio.br3电子邮件：lew. uni-tuebingen.dehttp://dx.doi.org/10.1016/j.entcs.2016.06.0121571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。182M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181（）（）（）（）迂回是类似于迂回的淘汰规则的特征。 据我所知，自然界...∨在经典ND逻辑[4]和证明规范化过程的复杂性。在此之前，我们已经提出了MIMP-图作为一个新的证明系统开发的最小蕴涵逻辑[6]，其推理是结构化的证明图。重点是，在MIMP-图中，很容易确定最大公式4和导致正常证明的约简序列长度的上界。通过计算原导子中极大公式的个数，证明了一个正规化定理。强规范化属性是这种规范化的直接结果，因为任何减少都会降低推导复杂性的相应度量。在本文中，我们希望更清楚地解释这一过程，并将其扩展到完整的命题逻辑。MIMP-图是其节点和边被标记的有向图。我们区分两个部分，一个代表证明的推论，另一个代表公式。对于mimp图的公式部分，我们使用有向无环图，我们称之为公式图，由mimp图构造中的基组成，并且仅包含共享公式节点的公式节点，因此每个公式节点仅需要在图中出现一次，图1的左侧示出了示例：命题P和Q在图中出现一次。对于MIMP图的推理部分，我们有规则节点（R节点），它们由推理规则的名称标记逻辑连接词和推理名称可以被索引，以实现公式（推理）和它们的表示（名称）之间的1-1对应，如图1的右侧所示：R节点E1具有公式图PQPQ作为大前提，公式图PQ作为小前提。Fig. 1. 式 PQ➔PQ以公式图（左侧）和大前提的形式描述（右）R-节点的节点1任何强规范化（SN）证明都必须考虑推导中出现的每一个可能的迂回（最大公式）。如果将规范化视为一个动态过程，则并非所有在推导中消除的弯路都从过程开始时就明确存在例如，Prawitz在直觉主义逻辑的（弱）规范化中使用的置换转换被设计为照顾隐藏的最大公式（参见下面的讨论）。隐藏着一个具有类似于-消去的规则的演绎系统使用置换转换来证明（弱）规范化。SN应该处理这些置换转换以及允许它的系统。隐藏极大公式的另一个例子是当转换（约简）后，新的极大公式可以出现。这已经4.最大公式是一个公式出现，它是一个引入规则的结果，是一个消除规则的大前提。M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181183′[客户[客户端][客户端][客户端][客户端]∨⊳在这种情况下发生的。在下面的推导中，在消除最大公式AB之后，A在作为规则消除的大前提的2由于这种情况的数量是无限的，在原始推导中的最大公式的数量不是一个很好的上限的减少应用程序的数量这是讨论SN证明时的一个关键点Π1Ar-介绍AB一Π2BAB置换转换攻击另一种情况，如下面的置换转换中所示。CD是一个隐藏的极大公式，它在置换转换后变成一个极大公式（右侧）。素八Π1D和218cΠ2D素八Π1ΠDΠ和218cΠ2DACCD CCDCCDDAB D DD图二、上面推导的fpl图及其约化。在我们的图的情况下，由于每个公式标记了图的一个且仅一个顶点，所以上面讨论的所有情况都是明确的。也就是说，每个可能出现在规范化证明中的最大公式都已经存在，并且没有隐藏的最大公式，如图2所示，其中q是R节点Ii的两倍结论，因此它已经表示了两个最大公式。图右侧所示的简化减少了最大公式的数量。因此，我们可以通过归纳极大公式的个数来证明SN。2全命题逻辑在[6]中，我们认为蕴涵是唯一的逻辑联结词。现在让我们转向命题演算的证明图的更一般的表示，包括蕴涵、合取和析取，我们称之为全命题逻辑的证明图（fpl-图）。首先，我们将标签集定义为节点和边缘，184M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181E}，r∈Nconc（finalconclusion）}，位置字母{P，Q，R，. }的情况下，∈∈{}∈⟨⟩∈∈∈ ∈ ∈∈F∈M⊕图V，E，L其中：V是节点的集合，L是LBL的子集，E′是⊕M我Q我我nnnM图，以及其R节点上的偏序，允许通过结构的节点。我们还将开发这些证明图的规范化程序。我们想强调的是，fpl图将公式图和R节点的信息放在一起。为了使它更透明，我们可以使用不同类型的线。以这种方式，F节点和它们之间的边被使用实线，而R节点和它们之间的边以及相邻的前提和/或结论被使用虚线，并且附加地，R节点已经被阴影化。定义2.1[标签类型]标签有五种类型：● R-Labels是规则nodes 的标签的集合：{● F-Label是公式nodes：{ni∈N，nj∈N，nk∈N}的标签的集合，● D-Labels是每个节点的标签集：H kN，C。● EF-Labels是公式边的标签集：{l（左），r（右）}，EM-Labels是规则边的标签集合：{piN（前提），rpjN（右前提），lpkN（左前提），rmlN（右小前提），lmmN（左小前提），mnN（小前提），M oN（大前 提 ） ， cpN（ 结 论 ） ， dqN （ disccharge ） ， ldr∈N（左 d 是charge ） ， rds∈N（rightdisccharge），hypt∈N（hypothesis），这五组标签类型的并集将被称为LBL。我们将使用项αm、βn和γr来表示公式α、β和 γ分别。定义2.2完全命题逻辑的证明图（fpl-图）G是有向的标号边vV，t E-标号，vt，用ar ow-t→v′定义。∈V<$，源v，目标v和标签Fpl-图递归定义如下：基如果G1是一个公式图，其根节点为αm，则G2定义为G1具有n个结点Hn和C，边αm-→C和H-→α，浓缩液fpl图➔如果G1和G2是fpl-图，并且通过以下步骤得到的图（中间步骤）G1<$G2包含边<$1- →α和两个节点<$1和α，LQ m图G3定义为G1G2，(i) 去除在中间步骤中生成的节点C中的进入边（参见下图，G1G2中的虚线区域）;(ii) 在顶部位置处的R-节点RNEi(iii) 边：α-m-n-ew→α-E，α-m-n-ew→α-E，α-m-n-ew → α-E，β-c-n-ew→β，β-c-o-n→c-C，其中新的是一个新的（新的）指数，其范围覆盖所有进入和/或离开公式节点αm，βn和αq的c，m和M类边;●QMM. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181185==：=inGGG）;1 23by边：α-l→α，α-r→βnJJ不不JK(ii)在顶部位置处的R节点R1iM我 n我我不不是一个fpl图（见下图）。⇒ ⇒➔如果G1是一个fpl-图，并且包含一个连接到C的节点βn和一个连接到H的节点Hk的节点αm，则定义为(i)G1G2，使得G2是根节点为F-节点αM;n不M不n 和β(ii) 去掉边：βn→C;conc(iii) 位于顶部位置的R节点R1j(iv) 边：β-pn-ew→β-I，β-Cn-ew→β-I，β-co-n→cC和β-dn-ew→H，其中新的是考虑p、d类的所有边以及公式节点αm、βn和αq的进入和/或离开的新鲜（新）指数;是一个fpl-图（见下图;αm-节点被放电）。⇒⇒如果G1和G2是命题fpl-图，且G1包含αm，G2包含βn，则定义为(i) G G1 G2G3，去掉节点C中的进入边在中间步骤中生成的（见下图，虚线区域（iii）边：α-lp-n-ew→ β-r-pn-ew →β-r-r-pn-r-pn-ew→β-r-pn-r-r-r-r-r-r-r-r-r-r-r-r-r-r 和α-co-n→cC，是一个fpl图，见下图。⇒⇒设G1，G2和G3是命题fpl-图，且∧186M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181D-no desH，则图G定义为s（GG） G，其中h为123D-nodeC（σtwice），α和β是双线性算子的子形式∨∧ ∨∨⊙一个R-节点RNI具有一个左前提和一个右前提。∨R我 R我不我我R我uH2O→H2O和σ-co-n→cC，其中w是考虑所有边的新指标我SR（G1<$G2）<$G35（中间步骤）包含节点：(i)去除在中间步骤中生成的节点C中的进入边（见下图）;(iii) 边：σ-lm-w→ σ_E，σ-rm-w→ σ_E，σ_M-w→σ_E，σ_E-cw→σ，σ_E-l-dw→H，类型p，d和公式节点αm，βn和➔问;是一个fpl图，见下图。⇒⇒➔Iv， El， Il， Ir类似于其他构造的情况（扩展版本见[5]）。在关于推理规则或R-节点的术语中，当R-节点具有多于一个的传入边时，这些边通过将它们称为左、右、大或小或这些术语的组合来区分因此，R-节点中的大前提包含被删除的连接词; R-节点中的另一个前提被称为在推理中起着或多或少相等作用的两个前提例如，一个R节点E有一个大前提，一个左小前提和一个右小前提;术语R-节点序列表示一个演绎，如果它是另一个R-节点序列（演绎）的一个较小部分，那么它被称为后者的子序列导出R节点序列中的最后一个R节点应用的前提的子序列被称为直接R节点子序列。而不是写fpl图需要符合一些限制。为了表述第一个，无环性，我们需要R-节点上的推理顺序的概念，它允许通过结构的节点，防止节点在路径中无限重复。5通过定义G1，G2将G1的R-节点与G2的具有相同前提和结论集合的R-节点进行相等或折叠，保持每个节点的推理顺序，并将G 1的F-节点与G 2的R-节点进行相等。G1与G2中具有相同标号的F-节点，并将具有相同源、目标和标号的边均衡为一。(ii)R节点Ei在顶部位置;M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181187<联系我们<∧∨→jj定义2.3设G是一个fpl-图。G的一个幂级数的一个推论是这是一个nF-node，满足n-l-bl→1f-l-bl→2n′和lbl定义2.4（1）对于ni∈V，fpl-图中的路是一个顶点和边的序列KKQ我M出边I-c→，和一个（或零的情况下Iv）出边JKnJn：H-h-yp→α1 是C和LBL 2 是m或Lb11是c我R不不Mα节点MKM.G的R-节点的偏序使得nni <$n和n是R-节点，<并且lbl2是M，或者lbl1是c并且lbl2是p。如果n是最大值，则节点n是顶位置节点w.r.t..形式：n1→1 n2-氯-2-苯并[d]噻吩→2-氯-2-苯并[d]噻吩... -k→k-−2 n−-k→1-k→1n，则n是一种假设公式节点，nk是结论公式节点，ni是规则节点之间的和公式节点。边lbli在两种边之间交替：第一种是lbljrm，lm，m，M，rp，lp，p和第二个lbljC. （2）fpl-图中的分支是路径的起始部分，该路径终止于图的结论F-节点或终止于其大（或右）前提是规则节点的结论的第一个小（或左）前提。(3)fpl-图中的可插入分支是由极大公式：fpl_I后接fpl_E分叉的分支。下面的引理2.5使我们能够证明给定的图G是fpl-图。其中，它说我们必须检查G的每个节点是生成定义2.2的构造情况的可能类型之一。为了避免索引的过载，我们将尽可能省略lm、rm、lp、rp、ld和rd类型的边的索引，记住索引的一致性是由它们所链接的规则节点的类型建立的。引理2.5G是fpl-图当且仅当以下成立：(i) 在fpl-图的(ii) G的每个节点N是以下十种类型之一PN用命题字母之一标记：{P，Q，R，. }中。N没有输出边l和r。FN有以下标签之一：i，j或k，并且恰好有两条带标签l和r的外出边。N具有带有标签p、m、M、lm、rm的输出边lp、rp;以及具有标记c和hyp的进入边缘E→N有标号<$Ei，且恰好有一条出边<$E- →β，其中βCn是节点类型P或F。N恰好有两条进入边α m- →αE，M➔ -M-→ α-E，其中α是一个不规则型P或F。这是两个向外的边缘QQMQn从节点：-l→α和-r→β。IN有标号I（或IV，如果空洞地提出一个假设），有一个J不➔I-d→H。 N只有一条进入边：β-p→βI，其中β是节点P型或F型。 有两条从节点α出发的边：α-l→α，➔t-→βn，使得有一个（或零的情况下，λIV）进入边缘的我1211n188M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181我⇒图1：通过归纳论证了G的R-结点的个数。 设为拓扑<∨对每个R-结点n，m，p，n∈G，m∈G，p∈G，nmp.<<1 23<订单，< 在G上，<在G和<在G. （GG）G可以是1 12 23 31 23联盟<和<另外<，对于每个R-n，n，m，suc，h，1，2，在构造情况I、E、I、El、Er、Il、I r或E中，我们构造新的R-节点2时，σ=A<$（A<$A）. 注意，k k−2k−1k的正规证明[客户端][客户端]≤A1<$A n从η，σ3，.，σ n的大小大于Fibonnaci（n）−σ3，...，σk−232c)去掉了两个极大公式（所有极大公式消去中的情形3）。d) 去掉了两个极大公式，但保留了公式节点，因此N max G减小（所有极大公式消去中的情形4）。e)删除极大公式，保留公式节点，重新排序R节点序列，从而减小NmaxG（所有极大公式消去中的情形5）.f) 所有最大公式都被删除。(v) 重复这个过程，直到归一化测量N max G减少到0并且G变成正常的fpl图。由于在fpl-图上消除一个极大公式的过程总是以消除至少一个极大公式而结束，并且随着图的顶点数的减少，我们可以说这个正规化定理直接是一个强正规化定理。下面是一个例子，说明了这样一个事实，即指数表示的证明是避免这种形式主义。斐波那契数的例子：考虑公式：1）η=A1<$A2，A1A1A2A1（A2A3）[A1]A1A2A1A1A2A1（A2A3）3A2A2A3A3A4A3A3（A4A5）A4A4A5A5A1A5一般来说，对于每5k，[A1]l（λ2）= 1[A1]ηηl（λ）=l（ λ）+ 1σ3，...，σk−1克-2l（k）=l（k−2）+l（k−1）+2k−1Ak−2Ak−2<$（Ak−1<$Ak）阿k1AkA1AkAk−1<$AkFibonacci（k）≤l（k）这是值得怀疑的插值将提供一个多项式证明同样的结论，这个巨大的证明。然而，使用图/dag表示，可以获得多项式证明（参见。[3]和[2]）。现在，在我们目前的图形表示的上下文中，在证明中每个公式只允许一个公式出现，我们产生以下多项式大小的图形证明M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181195[客户端][客户端]这实际上可以通过如下所示连续合并相同公式A3、A2、A1的A1A1A2A1（A2A3）[A1]A1A2A1A1A2A1（A2A3）3A2A2A3A3A4A3A3（A4A5）A4A4A5A5A1A5这个例子表明，在某些情况下，自然的类图证明压缩允许关闭类树和类图之间的指数大小的差距（在196M. Quispe-Cruz et al. /Electronic Notes in Theoretical Computer Science 323（2016）181事实匕首状）证明表示7.4结论文[6]中关于MIMP-图的结果推广到了FPL-图。因此，fpl-图是通过定义和例子引入的，保留了在自然演绎中表示证明的能力最小公式表示是fpl图结构的一个关键特征，因为正如我们前面看到的，很容易确定最大公式和归约序列长度的上界，从而导致正常的证明。通过计算原导子中极大公式的个数，证明了一个正规化定理。 强正规化性质是这种归一化的直接结果，因为任何减少都会降低推导复杂性的相应度量。这是研究基于图的定理证明器如何比通常的定理证明器更有效的初步步骤。我们建议读者，虽然斐波那契数的例子显示了树和dag-like表示之间的有证据表明，即使在dag表示有指数许多节点的大小，他们的结论。引用[1] M.手指 使用替换规则的Dag证明。 我们将向他们展示-荣誉散文Dov Gabbay 60岁生日，国王学院出版物第1卷，第671-686页。伦敦国王学院，2005年。[2] L. Gordeev，E.H. Haeusler和V.G. Costa. 证明压缩与电路结构的替代。Journal of Mathematical Sciences，158（5）：645[3] 埃德·沃德·赫尔曼·豪斯勒和瓦斯顿·贡·卡萨尔诉达科斯塔。 用证明理论技术压缩proofs的讨论。ChristianoBraga（Ed.），2012年。[4] Anjolina Grisi Oliveira和Ruy J.G.B. 奎罗斯 通过证明图的几何演绎。 在鲁伊·J·G·B Queiroz，编辑，Logic for Concurrency and Synchronisation ， Trends in Logic 第 15 卷 ， 第 3-88 页 。 SpringerNetherlands，2003年。[5] 马塞拉·基斯佩·克鲁兹命题逻辑证明图的强规范化。http：//www. tecmf.inf.puc-rio.br/MarcelaCruz?action=AttachFile& do=get& target=pmimp.pdf，2015.[6] Marcela Quispe-Cruz，Edward Hermann Haeusler，and Lew Gordeev. 最小蕴涵逻辑的证明图。第九届计算模型发展国际研讨会论文集，DCM 2013，阿根廷布宜诺斯艾利斯，2013年8月26日。，第16-29页，2014年。7.关于通过引入规则进行假设的一些附加技术也是可能的，但是这个主题超出了我们本文的范围。