可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）3-19www.elsevier.com/locate/entcs基于子N-图的安德拉德a，1鲁安卡瓦略b，2安乔利纳德奥利维拉a，3奎罗斯a，4aCentrodeInform'aticaUniversidadeFederal de PernambucoRecife，巴西bDepto。巴西累西腓联邦农村大学摘要Alves在他的博士论文中提出了N-图的规范化过程，这是de Oliveira在2001年提出的命题经典逻辑的多结论自然演绎，并以有向图的形式进行证明在这里，我们开发了一个新的规范化的N-图的启发A。Carbones在1999年工作，在那里她提出了一个组合模型来研究证明在削减消除过程中的演变关键词：N-图，正规化，有向图，重复1引言每当一个人关心的研究证明从几何的角度来看，一个很难高估的开创性工作的Statman在他的博士论文结构复杂性的证明[19]。借鉴Statman斯塔特曼1电子邮件：lsa@cin.ufpe.br2电子邮件：rvbc@deinfo.ufrpe.br3电子邮件：ago@cin.ufpe.br4电子邮件：ruy@cin.ufpe.brhttp://dx.doi.org/10.1016/j.entcs.2016.06.0021571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。4L. Andrade等人/理论计算机科学电子笔记323（2016）3即使用适当的几何工具和直觉在自然演绎（ND）中提取证明的结构属性的想法。ND中缺乏对称性对此类研究提出了挑战。当然，另一个明显的选择是看多结论演算。人们可以在文献中找到涉及此类结石的不同方法，例如Kneale[13]（由Shoesmith Smiley [18]深入研究）和Ungar但是，一个巨大的挑战仍然存在：正规形式和正规化过程。N-图系统是de Oliveira [ 14 ]在21世纪初开发的命题经典逻辑的多重结论NDN-图的动机是证明几何对象的想法，旨在研究自然演绎系统的几何。根据这一研究思路，我们提出了一个规范化过程，定义为一组图上的组合操作，可以为未来关于规范化过程中证明增长的组合研究提供一个框架。我们在本文中提出的过程也可以作为Prawitz定义的规范化的扩展，即它具有分离和子公式性质。在她对微积分证明中的切割消除后证明大小的爆炸的分析中，Carbone定义了一种称为复制的操作，并与从微积分证明中提取的逻辑图一起工作，以提出切割消除的纯组合分析[8]。我们的过程使用Alves一组新的可切换的减少，结合子N-图的复制操作的适应，以处理可切换的链接。因此，这种新的规范化与Prawitz的规范化和Gentzen的割消有更强的相似性，为研究这两个过程之间的对应关系提供了一个良好的起点，就像Zucker提出的[21 ][22][23][24][25]这也为进一步将Carbone关于切割消除过程中的证明生长的结果推广到ND系统奠定了基础2N-图由de Oliveira [14，15]提出，N-Graphs是一种对称自然演绎（ND）演算，具有结构规则，类似于C-D演算。 它 是经典逻辑的多结论证明系统，其中证明以有向图（“有向图”）的形式构建自2001年首次出版以来，已经对N-图进行了一些研究[14]，如Alves[3]和Cruz给出了经典N-图的归一化算法[1]，并给出了子公式和分离性质[2]。 此外，提出了一种线性时间证明检查算法[4]，L. Andrade等人/理论计算机科学电子笔记323（2016）35最近，提出了一种新的序列化证明[10]，使用来自证明网（proof-nets）的子N-图（sub-N-Graphs）的概念的适应来创建子N-图，并在存在散焦可切换链接而没有公理链接的情况下执行经典逻辑证明中的切割。2.1证明图该系统的定义有点像证明网。有证明图的概念，所有的图都是用有效链接构造的，其中每个节点是至多一个链接的前提和结论，以及N-图的概念，这是正确的证明图，即。表示有效证明的证明图这些构造分别类似于证明结构和证明网的定义[12]。链接表示派生中的原子步骤。聚焦链接是指具有两个前提和一个结论的链接，如图1所示（−I，−link，→ −E，T-聚焦弱和收缩）。散焦环节是有一个前提和两个结论的环节，如图1所示（−E，T−环节，→ −I，−散焦弱和扩张）。所有其他的链接都被称为简单链接，只有一个前提和一个结论（图1）。①的人。有两种边，一个顶点v的实体入度（出度）是朝向（远离）它的实体边的数量Meta入度和出度的定义类似。入度（出度）等于零的顶点的集合是证明图G的前提（结论）的集合，并且由PREMIS（G）（CONC（G））表示。实入度为零且Meta入度为1的顶点集是G的消去假设集（HY POT（G））。图1.一、聚焦，散焦和简单的链接。根据其名称，逻辑链接表示ND中的派生（T-链接充当排中律）。结构链接表达了结构规则的应用，就像在微积分中一样：它可以削弱证明 （T-聚焦弱，T-散焦弱，T-单弱和T-单弱），复制前提（扩展链接）和在等价类中分组结论（压缩链接）。没有链接来模拟交换规则，因为在证明图中，6L. Andrade等人/理论计算机科学电子笔记323（2016）3图二.循环的证明图图3.第三章。Meta edge：左侧的无效应用程序对应于CNASA和CNASB，右侧的有效应用程序对应于► （AB）→A，B.前提的顺序对于推导规则的应用并不重要。这些公理用一个顶点没有边的证明图表示。标记为A的单个节点已经是一个有效的派生：它表示微积分中的公理（A<$A）。在图2中有三个证明图。第一个是A B AB的无效其他的是AAA和AAA的正确推导（收缩和扩展边用虚线标出）。2.1.1元边和假设Ungar和Gentzen的系统都在N-Graphs中，这种引入是以一种更可控的方式进行的，这也使识别不充分证明图的任务变得复杂。例如，图中的3是不正确的，但第二个是。2.2健全性标准类似于Danos-Regnier定义2.1[切换]给定一个证明图G，与G相关的切换图S（G）是G的一个生成子图，其中删除了以下边：每个扩展链路的两条边之一和每个收缩链路的两条边之一。定义2.2[元交换，虚拟边]给定证明图G，与G相关联的元交换图S（G）是G的交换，其中具有元边{（u，w），（u，v）m}的每个链路被以下边之一替换：从u到w的边或从v到w的边，其被定义为虚拟边。5生成子图是G的一个包含G的所有顶点的子图G1.L. Andrade等人/理论计算机科学电子笔记323（2016）37定 义 2.3[N-Graph derivation] 证 明图 G是 一个 N-Graph derivation （ 或简 称 N-Graph），如果与G相关联的每个元交换图都是非循环和连通的。收缩和膨胀环节是可靠性准则的基础：在证明图中由它们连接的公式必须已经以某种其他方式连接→−I也起着重要的作用：链接的前提（B）和被取消的假设（A）需要在证明中已经因此，元交换必须选择将A→B连接到A或B，并且无论选择如何，所得到的子图都必须是连通的和非循环的。 在图3的第一个证明图中，结论 of→ −I是A→（A<$B），所以这个公式已经带有对A的依赖性，并且元边从证明的前提集合中删除了节点。然而，A的另一次出现来自相同的初始节点，这被→ −E链路用来获得当元交换选择连接A→（A→B）和A的虚边，并且结果不是树时，可靠性准则捕捉到这一点图3中的另一个证明图并没有出现这种情况：所有的两个元交换都是非循环的，并且是连通的。系统的可靠性和完备性通过N-Graphs和LK（经典逻辑的微积分）之间的映射得到证明[14，15，10]。3N-图的正规化Alves在他的博士论文[2]中提出了一个N-图的规范化过程。在Statman [19]，Bluteet. [5]和其他创建图形和拓扑框架来研究自然演绎的规范化的人，他设计了一组分为两个阶段的操作：第一阶段处理一般的证明图，即树和一些特定的循环，第二阶段是为了彻底处理循环结构而构建的。最后，所提出的程序有四组转换，消除最大的公式/段和算法（命名为3CA），旨在确定一个周期是否有绕道或没有。在这里，我们提出了一个不同的归一化过程，其中一些由Alves定义的约简（β和置换弱化约简）略有修改，以及置换可切换约简的新方法。拓扑框架设计检查和转换循环结构，以消除弯路被放弃，但分离和子公式性质仍然可以证明规范化的N-图。这种新的更简单的规范化也使用了Carbone [8]定义的称为重复的操作，这导致了她的工作的扩展，可以生成一个组合模型，用于研究N-图规范化过程中的证明大小。我们称主公式为两个链接之间的约简中的公式，外围公式为两个链接中的所有其他公式。约简图像是说明性的，并且由Gi，i∈[1， 4]表示的图可以是连接的（或者，在可切换约简中，它们中的一些必须是连接的）。可切换链路8L. Andrade等人/理论计算机科学电子笔记323（2016）3（收缩和扩展）用虚线无向边缘示出，以保持图像更清晰，并且还突出它们的出现。这个过程的轮廓很简单：在N图中，考虑到由有向边定义的自然的连续性，主要目标是去除所有的β还原，即所有的I-β还原连接之后是E-β还原连接。应用此过程得到的N-图将具有与正常ND推导类似的属性：范式和子公式属性。作为补充，该过程比N-图的原始过程更简单，并且应用了与[8]中定义的操作类似的操作，这可以将我们带到一个熟悉的组合微积分研究领域3.1β约化定义3.1【最大公式】一个公式出现A是N-图G中的一个最大公式，如果它是一个I-隐式环的结论和一个E-隐式环的前提。事实上，N-图是一个多重结论演算，它以一种结构化的方式改变了归约的性质，而这在Prawitz [16]为自然演绎引入的归约中是不会发生的。一旦证明用图来表示，而不仅仅是树，在消除A/B型最大公式时，在证明中发生的修剪，例如，不能在多结论系统中复制，其中证明的几何结构（连通性）是其正确性的基础。消除最大值公式的β约减则具有“保守”方面，如图4所示。此外，T和T环的存在提出了一种新的最大值公式，其中非原子公式是T环的结论（前提），并遵循（之前）消除（引入）规则。最大值公式的这些方面已由Ungar在[20]中提出然后，我们把所有的引入链接和上链接称为I-上链接，把消除链接和上链接称为E-上链接[2]。最后一种β归约去掉了一个T-环后的一个T-环，从证明中去掉了阿尔维斯所说的3.2置换弱化约化在Prawitz的自然演绎法中，定义了“最大段”的概念，以解决可能隐藏在证明中的最大公式，通过在树中传播公式。它只发生在使用副公式C来执行连接词的消除的X1和X2消除规则中。多结论自然演绎系统通常不需要这样的公式来创建一个系统，其中引入和消除规则是对称的，有点像微积分。N-图是没有什么不同的，但这些段仍然可能出现在一个证明中，通过应用结构规则来执行弱化。定义3.2[段、最大段、结构段]L. Andrade等人/理论计算机科学电子笔记323（2016）39图四、β减少：引入环节后进行淘汰。N-图G中的顶点u到顶点v是有向边序列（u0，v0），（u1，v1），.，（un，vn），其中u0=u，vn=v，vi=ui+1。 N-图G中从公式A的出现点u到公式A的出现点v的一段是最大段，如果u是I-连通环的结论，v是E-连通环的前提，且该段中每隔一条边都是结构环的一部分.如果u是弱化环节的结论，v是I-扩张/扩张环节的前提，或者如果u是E-扩张/收缩环节的结论，v是弱化环节的结论，则同一节段是结构节段。这里进入弱化公式的置换约简。这些转换的重点是向下移动I-Bavour链接和向上移动E-Bavour链接（这里上下移动遵循有向图中的边的方向）。 可能隐藏在证明中的最大值公式将变得显式，然后它们可以通过β约简去除。在图5中，我们可以看到引入规则和聚焦弱化链接的减少。其他减少量见附录A。3.3置换可切换约简可切换的归约是负责在标准化过程中证明的指数爆炸的归约。膨胀和收缩可以是10L. Andrade等人/理论计算机科学电子笔记323（2016）3图五、置换还原：介绍链接，然后是重点弱化。最大线段的一部分，因为它们也是结构链接，因此需要 用I/E-最大值规则排列，以显示可能的隐藏最大值公式。由于这些链接的可切换方面，需要小心地进行置换，以避免将有效的证明图转换为无效的证明图。在我们提出约简之前，我们需要定义证明图的重复操作[8]：定义3.3[复制]复制D是应用于证明图G和G的子图GJ的二元运算，具有以下性质：(i) 若GJ的一个顶点是G中的一个焦点，则它的直接前趋顶点要么都在GJ中，要么都不在Gj中;(ii) 若GJ的一个顶点是G中的一个离焦点，则它的直接后继顶点要么都在GJ中，要么都不在Gj中;(iii) GJ中至少有一个前提或结论是可切换链路的前提和结论或→-I。GJ在G中的复制是一个图D（G，GJ）定义为G，除了在GJ上，它将被它的两个副本和以下额外的顶点所取代(i) 设u是G j中的前提（即，在G j中没有朝向它的边）和u1，u2是它在D（G，GJ）中的拷贝。然后创建一个新的顶点uJ，并通过展开将其链接到u1和u2。如果G中有朝向u的边，则将这些边连接到D（G，GJ）中的u j。(ii) 设v是G j中的结论（即，在G j中没有边）和v1，v2是它在D（G，GJ）中的拷贝。 然后，将创建一个新的顶点vJ，并将其链接到v1和v2，宫缩如果G中有来自v的边，则将这些边连接到D（G，GJ）中的v j。上述程序的例外是第3项的链接。在这种情况下，我们将用GJ中v的副本v1和v2折叠G−GJ中的顶点u1和u2。这种操作与为光学流图定义的Carbone操作略有不同。 区别在于GJ的两个副本，即GJ1和GJ2，被连接到G中的原始顶点。在图6中，我们有一个证明图的复制操作的说明。定义3.4[边界[8]，溶解边，折叠顶点]设G是一个图，GJ是它的一个子图，我们说G中的一个点是边界点，如果它是L. Andrade等人/理论计算机科学电子笔记323（2016）311∈−见图6。复制一个证明图：白色和1，2顶点是边界点，链接到1和2的虚线边是溶解边，左侧的1和2是折叠顶点。不属于GJ，但链接到GJ的点。溶解边（u，v）G是从D（G，GJ）中移除的u（在边界中）和v（在GJ中）之间的边，其中u被折叠为GJi中的折叠顶点vi。换句话说，折叠的顶点是属于GJi的边界中的顶点。定理3.5（子N-图的复制）设G是N-图，GJ是G的子N-图。则D（G，GJ）是一个N-图。证据矛盾的证明。假设D（G，GJ）不是一个N-图。那么我们有两种情况：(i) 存在断开的元交换S（D（G，GJ））：我们知道G和GJ是N-图，S（D（G，GJ））在任何一个重复的分支中都是不连通的。此外，在S（G-GJ）中，折叠的顶点之间总是有一条路径，因为这些顶点在G中通过可切换链路连接。设u和v是S（D（G，GJ））中的两个不连通点，πS（G）中从u到v的路。 那么，π∈GJ∈，否则，π将是存在于S（D（G，GJ））中。 当这些顶点在S（D（G，GJ））中不连通时，πJ(the根据重复定义的π的转换）必须将u连接到GJ1中的顶点w1，并将v连接到GJ2中的副本w2。但是，由于每个副本GJi在S（GJi）中连接，它们也连接到相应的折叠顶点，因此通过S（G-GJ）连接。(ii) 存在具有周期c的元切换S（D（G，GJ））：我们知道G和GJ是N-图，S（D（G，GJ））在任何重复分支GJ和G-Gj中都没有圈.那么G−GJ和副本之间的连接必须创建c。我们有两个案例：(a) c在G中GJ和GJi，GJ的一个函数：我们可以在S（G）中构造相应的圈cj，复制过程的基本步骤是：移除G j中添加的顶点并将边界节点连接到GJ中的原始节点;将c中折叠的顶点vi分离为原始顶点u，v并添加回溶解的边（u，v）。由于G是一个N-图，这个圈不可能存在，因此我们得出了一个矛盾。(b) c在 G-GJ中，并且 Gj和 G j都是GJ的1和2个拷贝：12L. Andrade等人/理论计算机科学电子笔记323（2016）3JJ由于c经过GJ1和GJ2，而这两个副本之间的唯一联系是通过G−GJ，因此必须存在从u到v的路径π1∈c<$G−GJ，两者都在边界内。当G是一个N-图时，GJ中必有一条从uJ到vJ的路π2，其中（u，uJ）∈G，（v，vJ）∈G（如果u=v，即π1=c）。然后，我们可以在S（G）中创建一个圈c，通过将这两条路与边（u，uJ），（v，vJ）连接起来，再次达到矛盾。Q Q图7我们可以看到引入规则的置换与收缩的约 所有其他置换可转换还原见附录A。见图7。可切换的缩减：先收缩后消去（第一列和第二列），先收缩后扩张（第三列）。临界约化是指收缩或→-I链紧接着扩张的约化。在这种情况下，我们需要复制北（南）帝国的主要公式，以消除扩张（收缩）。这些操作在图像中由 * 表示。3.4正常化定义3.6[割公式] N-图G中的公式A是割公式，如果它是约简的主公式定义3.7[正规N-图] N-图G是正规的，如果没有最大公式，也没有最大或结构段。换句话说，G中没有割公式。定理3.8（N-图范式）正规N-图G的从前提或放电假设A到结论B的段可以被划分为三个唯一的部分：(i) 消除部分，其中每条边是消除链接或扩展的一部分。L. Andrade等人/理论计算机科学电子笔记323（2016）313(ii) 薄弱部分，其中每条边都是薄弱环节的一部分。(iii) 引入部分，其中每个边缘是引入链路或合同的一部分。弱部分也被分成树部分，第一部分是E-散焦链接，第二部分是聚焦和散焦链接，第三部分是I-散焦链接。证据证明是对本文中提出的所有约简的彻底检查，考虑所有可能的反演：(i) 结构链接后的扩展：图 A.5和A.7。(ii) E-结构连接后的附着力：图 A.2、A.4和A.3。(iii) 收缩后的扩张：图。第七章(iv) E-收缩后的收缩：图。第七章(v) 扩张后，I-Escherichia：Fig. A.6和A.7。(vi) I-E-Bracavour之后：图。四、(vii) 收缩后的结构：图。 A.5和A.7。(viii) 结构后，I-Escherichia：Fig. 5，A.1.检查每个约简将N-图G约简为另一个N-图GJ是简单的。定理3.5足以验证帝国复制的归约。所有其他的约简都可以通过仔细检查每个开关S（GJ）来验证，使用原始S（G）是非循环和连通的事实QQ推论3.9（子公式性质）正规N-图G是G的前提集合或结论集合中的公式的子公式子公式属性是范式的扩展，一旦我们注意到没有公式被引入，然后在N-Graph中的任何片段中被消除通过前面给出的约简，我们可以证明规范化定理，它比规范形定理强，但比强规范化定理弱，遵循Prawitz [16]给出的定义。定理3.10（正规化）每个N-图导子都可归约为正规形式。证据我 们 可以通过归纳法来证明正规化定理，归纳法是关于切割公式的次数、证明中具有最大次数的切割的数量以及最大/结构段的反演的数量（反演如定理3.8的证明中所示）。当一个N-图G被简化为GJ时，一个最大值公式被移除，或者一个最大值/结构路径中的反转数减少。即使通过某种约简添加新的切割公式，我们也可以选择应用约简的顺序，以便公式在顶点处的次数总是更小。对于简单归约，这14L. Andrade等人/理论计算机科学电子笔记323（2016）3有重约简稍微复杂一点，只要它能证明一个与主公式次数相同的割公式。在这种情况下，可以创建无限还原序列。为了避免这种情况，我们不仅需要选择最大程度的约简，而且还需要选择一个北方（或南方）帝国，以便仅用较低程度的约简公式进行复制。为了证明总是有可能找到这样的切割公式，我们只需要证明不可能有一个如图1所示的循环八、图八、循环切公式，但南北帝国的联系可以任意。这种循环的不可能性来自于[10]定义的嵌套引理的应用，对于循环中的所有公式A，得出结论eAeA，∈ {，}Q在图9中，我们可以看到AAA的N-图的规范化示例。在这个例子中，我们有一个扩展，然后是一个收缩，它可能隐藏了一个最大值公式。在应用可切换归约（需要重复操作）之后，结果是一个正常形式的N-Graph。这个例子也说明了我们的过程不是一个强规范化的过程：我们可以选择复制子N-图A<$A<$A，结果将是一个不同的N-图，也是它的规范形式。4结论我们提出了一种新的N-图规范化方法，它只基于割公式约简来去除最大公式和最大/结构段。经过一系列的归约，我们得到的范式与普拉维茨在[16]中定义的范式非常相似，它的分析和综合部分由消去部分和引入部分代表，但更强，因为它也固定了范式的薄弱部分中的薄弱环节这种范式更接近于N图证明之间等价关系的定义。Prawitz建议，推导之间的恒等关系可以用归约来表征[17]，并且它在不削弱ND等规则的情况下适用于证明系统。弱化本质上是一种将推导组合在一起并省略某些前提或结论的方法，因此它在本质上与其他演绎规则是置换的，并且可以使其难以L. Andrade等人/理论计算机科学电子笔记323（2016）315见图9。N-图表示A<$A<$A <$A的证明，右边是规范化的证明定义这样的等价关系。我们通过规范化得到的规范形式为弱化规则确定了一个位置，从而便于恒等式关系的定义。有删节的校样比没有删节的校样要短。在我们的过程中，当一个割被一个顶点隐藏时，这种增长就会发生，这个顶点既是可切换链接（收缩，扩展和→-I）的结论也是前提我们需要重复一个子证明，以使最大公式明确。这表明了N-图中的结构链接如何将割消的一些性质带入自然演绎系统。由于我们使用Carbone [8]开发的组合运算的修改版本来研究在微积分中具有压缩的切割规则的置换，因此其在N-图中的行为在组合方面是相似的，并且也反映了Prawtiz [17]的假设替换。然后，这项工作是在自然演绎证明系统中证明大小爆炸的组合研究的第一步引用[1] 阿尔维斯湾五、de Oliveira，A. G.，德凯罗斯河J. G.乙：证明图：一个彻底的循环处理，规范化和子公式属性。Fundamenta Informaticae106，119[2] 阿尔维斯湾五、de Oliveira，A. G.，德凯罗斯河J. G.乙：通过几何透视技术的变换与循环归一化增强。第16届逻辑、语言、信息和计算研讨会- WoLLIC 2009，2009年，东京，逻辑、语言、信息和计算，第16届国际研讨会，WoLLIC 2009。Berlin：Springer，2009，v. 1，84[3] 阿尔维斯湾五、de Oliveira，A.G.，德凯罗斯河J. G. 乙：走向规范化的Logic Cooloquium，2005，Torino，Bulletin of Symbolic Logic。美利坚合众国：2005年，v。11，302[4] 安德拉德湖，卡瓦略河de Oliveira，A.，de Queiroz，R.：N-图上的线性时间证明验证第20届逻辑、语言、信息和计算研讨会- WoLLIC 2013，2013，达姆施塔特，逻辑、语言、信息和计算，第20届国际研讨会，WoLLIC 2013。Berlin：Springer，2013，v. 1，34[5] 布鲁特河F.、Cockett，J. R. B、锡利河A. G.，Trimble，T. H.：弱分配范畴的自然演绎与凝聚。Journal ofPure and Applied Algebra113（3），22916L. Andrade等人/理论计算机科学电子笔记323（2016）3[6] 巴斯，S.：k-可证明性的不可判定性纯逻辑与应用逻辑年鉴。53，72[7] Carbone，A.，塞姆斯，S.：没有前件推理的证明：组合学和割消的复杂性介绍Bulletin of the AmericanMathematical Society34，131[8] Carbone，A.：有向图的复制与证明的指数爆破。Annals of Pure and Applied Logic100，1[9] Cruz，M.问：de Oliveira，A. G.，德凯罗斯河J. G. B、de Paiva，V.：直觉N图Logic Journal of theIGPL，Print（2013）[10] 卡瓦略河安德拉德湖，de Oliveira，A.，de Queiroz，R.：基于子N-图的N-图序列化。第21届逻辑，语言，信息和计算研讨会- WoLLIC 2014，2014年，智利，逻辑，语言，信息和计算，第21届国际工作室，WoLLIC2014。Berlin：Springer，2014，v. 8652，94[11] 达诺斯，五，Regnier，L.：乘法的结构。数学逻辑28，181-203（1989）[12] Girard，J.- Y.：线性逻辑Theoretical Computer Science50，1[13] Kneale，W.：逻辑省。《当代英国哲学》（1958）[14] de Oliveira，A. G.从几何学角度证明。Pernambuco联邦大学博士论文（2001年）[15] de Oliveira，A.德凯罗斯河J. G.乙：几何演绎通过图形的证明。并发与同步逻辑。de Queiroz（ed.），Kluwer，3[16] Prawitz，D.：自然演绎。理论研究的证明。《斯德哥尔摩大学学报》第三卷。Almqvist和Wiksell，斯德哥尔摩（1965年）[17] Prawitz，D.：证明理论中的思想和结果。第二届北欧逻辑研讨会论文集。03 The Dog（1965）[18] Shoesmith，D.J.，斯迈利，T。J.：多结论逻辑剑桥大学出版社（1978）[19] Statman，R.：证明的结构复杂性。斯坦福大学博士论文（1974年）[20] Ungar，A.M.：正规化、割消与证明理论。CSLI演讲笔记，语言和信息研究，卷。28（1992）[21] Zucker，J. I.：割消与归一化的对应关系。数学逻辑年鉴7：1-156。（一九七四年）A其他标准化缩减图A.1. 置换约化：引入链接，然后是散焦弱化。L. Andrade等人/理论计算机科学电子笔记323（2016）317图A.2. 置换还原：集中弱化链接，然后消除。图A.3. 置换减少：聚焦/散焦削弱与T-链接和T-链接的链接。18L. Andrade等人/理论计算机科学电子笔记323（2016）3图A.4. 置换约简：先散焦，然后消除弱化的链接。图A.5. 置换缩减：聚焦/散焦，通过扩张和收缩弱化链接L. Andrade等人/理论计算机科学电子笔记323（2016）319图A.6. 可切换的缩减：介绍链接之后是扩展。图A.7. 可切换的减少：收缩和扩展与T型链接和双连杆.
我的内容管理
展开
