线性逻辑中的次指数证明系统

理论计算机科学电子笔记269（2011）109-123www.elsevier.com/locate/entcs具有次指数的线性逻辑中的证明系统Vivek Nigam1美国宾夕法尼亚大学费城分校Elaine Pimentel和Giselle Reis巴西贝洛奥里藏特米纳斯吉拉斯联邦大学摘要在过去的几年里，线性逻辑已经成功地被用作编码证明系统的一般逻辑框架。由于线性逻辑对结构规则的精细控制，可以使用线性逻辑连接词来匹配编码逻辑中指定的结构限制。 然而，一些对其序列施加更复杂的结构限制的系统不能容易地在线性中捕获。逻辑，因为它只区分两种类型的公式：经典和线性。这项工作表明，人们可以编码更广泛的证明系统，通过使用集中的线性逻辑与次指数。我们通过编码系统G1m的最小，多结论系统，mLJ，和聚焦系统来证明这一LJQ，直觉逻辑。最后，我们确定的一般条件，以确定是否线性逻辑公式对应于一个对象逻辑规则，这条规则是否可逆。保留字：逻辑框架，线性逻辑，次指数，聚焦。1介绍在过去的几年里，线性逻辑已经成功地被用作一个通用的逻辑框架，为不同的逻辑指定了许多证明系统。事实证明，在微积分中，一些对偶性直接出现。例如，在箭头的左边或右边出现的公式在某种意义上是该公式的“双重”出现。切割和初始推理规则是“对偶”推理规则。逻辑连接词的引入规则在箭头的左边和右边通常具有双重行为。2使用线性逻辑1如果没有Dale Miller的建议以及CNPq和FAPEMIG的支持，这项工作第一作者还得到了NSF，ONR和AFOSR MURI“协作政策和有保证的信息共享”的部分支持[2]至少当人们希望能够消除非原子切割和非原子初始规则时是这样。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.03.009110诉Nigam等人理论计算机科学电子笔记269（2011）109作为一个逻辑框架，它可以使用对合否定来直接捕捉编码系统的这种二重性，并对它们进行推理另一方面，在设计一个证明系统时，通常通过结构规则施加给其序列的结构限制，发挥着与逻辑规则本身同样重要的作用在根岑[6]设计的第一个微积分系统中，直觉主义逻辑系统LJ与经典逻辑系统LK的不同之处在于，前者将序列的右侧限制为最多包含一个公式。从那时起，其他几个证明系统也被提出来，这些证明系统在结构上的限制比在逻辑规则上的限制更重要与经典逻辑不同的是，在线性逻辑中，弱化和收缩的结构规则不允许用于任何公式，而只允许用于那些标有所谓指数（？）。通过这种方式，可以区分两种不同类型的公式：不适用结构规则的线性公式（即，它们不能被擦除或复制）和允许应用结构规则的无界公式。这种区别通常被认为是在语法上，使用包含两个上下文的形式为θ：Γ的序列[1]：Θ con-只包含无界公式，表现为一组公式，而Γ只包含线性公式，表现为一组公式。因此，人们可以利用这种不同的公式处理来指定证明系统，如LK和LJ，其序列最多有两个不同的上下文，其中一个上下文可以被视为多集，另一个上下文可以被视为一组公式。它似乎是不可能的，但是，指定的证明系统，它的序列，需要一个以上的上下文被视为一组或多组公式施加结构限制。例如，Maehara的mLJ系统[ 9 ]中的序列聚焦证明系统是强加需要多于一个上下文的结构限制的证明系统的其他示例。除了用于存储出现在序列的左侧和右侧的公式的上下文之外，还需要额外的上下文来跟踪所关注的公式结果表明，线性逻辑指数不是正则的[4]。事实上，有可能构造线性逻辑证明系统， 像运营商（？a，！a），称为次指数[15]，根据需要。这些运算符可能允许也可能不允许收缩和/或弱化，并且以指定用这些运算符标记的公式之间的蕴涵关系因此，子指数允许设计证明系统，其序列具有所需的尽可能多的上下文，并且其中任何一个都可以被视为多集或集。正如本文所示，使用次指数极大地增强了证明系统我们建议使用具有次指数证明系统的聚焦线性逻辑，称为SELLF[15]，来编码对其序列施加更复杂结构限制更具体地说，我们展示了如何编码诉Nigam等人理论计算机科学电子笔记269（2011）109111系统GIm[18]，mLJ[9]和LJQ[7，5]在SELLF中。到目前为止，我们已经描述了具有次指数的线性逻辑如何适合于指定广泛的逻辑系统。另一方面，人们可能会问，一个给定的线性逻辑公式是否是任何微积分系统的具体化事实证明，它是可能的分类线性逻辑公式，以这种方式来精确地确定是否线性逻辑公式对应于任何可能的对象级推理规则。本文的组织如下：第2节介绍了系统SELLF，重点是具有次指数的线性逻辑;第3节展示了使用SELLF的规范的示例;第4节研究了对象和元级逻辑之间的连接，最后，在第5节中，我们总结了未来工作的一些方向。2次指数线性逻辑虽然我们假设读者熟悉线性逻辑，但我们回顾了它的一些基本证明理论。文字是原子公式（A）或它们的否定（A）。连接词“”和“”及其单位“1”和“”是乘法;连接词“”和“”及其单位“0”和“T”是加法连接词;“”和“”是（一阶）量化器;和！然后呢？是指数。我们假设所有的公式都是否定范式，这意味着所有的否定都有原子作用域。由于指数，人们可以区分在线性逻辑两种类型的公式：线性的主要连接不是一个？和无界的，其主要连接词是？。线性公式可以被看作是只能使用一次的资源，而无限公式可以被看作是无限的资源，可以根据需要使用多次。这种区别通常通过在线性逻辑序列中使用两个不同的上下文（θ：Γ）来反映在语法中，一个（Θ）仅包含无界公式，另一个（Γ）仅包含线性公式[1]。 这种区别允许结合结构规则，即在经典逻辑中，我们可以把连接词的弱化和收缩引入到连接词的引入规则中，例如：G3c系统[18]。在这样的表示中，包含无界公式的上下文（Θ）被视为公式的集合，而仅包含线性公式的另一上下文（r）被视为公式的多集合事实证明，指数不是关于逻辑等价关系的规范[4]事实上，如果出于任何原因，我们决定用标准的经典规则定义一个蓝色和红色连词（分别是Bb和BrΓ，A，B<$ΔbL<$Δ，A<$Δ，B<$bRΓ，A<$bB< $Δ Γ<$ Δ，A<$bBΓ，A，B<$ΔrL<$Δ，A<$Δ，B<$rRΓ，A<$rB< $Δ Γ<$ Δ，A<$rB则很容易证明，对于任何公式A和B，A<$bB<$A<$rB。这意味着所有经典合取的符号都属于同一个等价类。112诉Nigam等人理论计算机科学电子笔记269（2011）109RRBRBBRB因此，我们可以选择使用任何特定颜色作为合取的标准形式，并且可证明性不受此选择的然而，同样的行为并不适用于线性逻辑模态。事实上，假设我们有红色！r，？R和蓝色！b，？b具有标准线性逻辑规则的指数集合：► ？Γ，FF，F► ？Γ，FF，F！R► ？ 你！F► 你，？FD呢？R！B► ？ 你！F► 你，？FD呢？B我们不能展示这个！rF！bFnor？rF？bF.这开启了定义指数类的可能性，称为次指数[15]。通过这种方式，可以构建包含尽可能多的类指数运算符（！我，？l）根据需要：它们可能允许也可能不允许收缩和弱化，并且被组织在指定这些算子之间的蕴涵关系的前序（≤）中。形式上，一个具有次指数的线性逻辑的证明系统，称为SELL，通过使用形式为I，≤，W，C的次指数签名来指定，其中I是集合在子指数的标号中，≤是I的元素之间的前序关系， W和C都是I的子集，分别指定哪些次指数允许弱化和收缩。我们将要求前序≤关于集合W和C是向上封闭的，也就是说，如果x∈y且x∈ W（x∈ C），则y∈ W（y∈ C）。对于所有的连接词，SELLSELL包含与线性逻辑中相同的引入规则，除了指数。另一方面，这些特征由次指数签名来指定，如下：3y yC，ΔXD，如果x ∈ I？C，？C，ΔC，if y ∈ C<$ΔW，如果z∈ W► ？C，Δ► ？C，Δ► ？ C，Δ也就是说，第一个规则，称为“舍弃”，可以应用于任何次指数，而收缩（相应地，弱化）仅适用于出现在集合C（相应地，W）中的次指数在本文中，我们假设C=W。提升规则由以下推理规则给出►？X1 C1，...， ？xn Cn，Cx x a！一►？1C1，...，？nCn，！C其中a≤xi，对于所有i = 1，.，n.提升规则将在这里发挥重要作用，即，指定编码证明系统的结构限制。特别地，可以使用次指数爆炸，！c，检查上下文中是否只有某些类型的公式，特别是那些标有次指数的公式，？x，使得c≤x。如果有公式的话？在这样的上下文中，那么！C不能使用。正如我们在本文中所示，使用次指数大大增加了线性逻辑的表达能力，不再限制人们只使用两个上下文，而是需要多少就使用多少，即每个次指数有一个上下文。此外，由于可以指定允许复制或擦除公式的子指数，[3]只要上下文清楚，我们就省略次指数签名。zy诉Nigam等人理论计算机科学电子笔记269（2011）109113这些上下文可以被视为多集或公式集。这将使我们能够在SELL中编码大量的证明系统，这些系统似乎不可能在简单的线性逻辑中编码。2.1聚焦由Andreoli [1]首次提出的用于普通线性逻辑的聚焦证明系统为无割证明提供了范式证明。在本节中，我们回顾了[15]中提出的SELL的集中证明系统，称为SELLF为了介绍SELLF，我们首先回顾一些术语。我们把主要连接词是，次指数爆炸，单位1和正文字的公式归类为正所有其他公式都被归类为负数。图1包含了聚焦证明系统SELLF，它是Andreoli原始系统的一个相当简单的概括。在这个证明系统中有两种箭头。带箭头的数列属于正相，并引入了“聚焦”公式的逻辑连接符带负相位的数列属于负相位，分解公式在它们的右边，以这样的方式，只有可逆的推理规则被应用。结构规则D1、D1、R和R在负相和正相之间进行过渡。与线性逻辑的通常表示类似，在序列的n和n的左边有一对上下文，这里记为K：Γ。 第二个语境，Γ，收集了其主要连接词不是问号的公式，表现为线性逻辑中的有界语境。但与线性逻辑不同的是，在线性逻辑中，第一个上下文是一个多集公式，其主要连接词是一个问号，我们将K推广为一个索引上下文，它是从集合I中的每个索引（对于某些给定和固定的次指数签名）到一个有限多集公式的映射，以便在SELLF中容纳一个以上的次指数。在Andreoli的线性逻辑系统中，索引集包含一个次指数∞，K [ ∞ ]包含无界公式集。图2包含在这样的索引上下文中使用的不同操作。例如，在张量规则中使用的操作（K1<$K2）指定通过合并两个上下文K1和K2获得的结果索引上下文。聚焦允许将具有相同极性的推理规则的集合组合成“宏规则”。例如，考虑一个公式N1<$N2<$N3，其中所有N1、N2和N3都是负公式。一旦集中，引入这样一个公式的唯一方法是使用一个K：ΓK：其中i∈ {1， 2， 3}。别无选择。举另一个例子，逻辑程序设计中的反向链接和正向链接规则也可以用这种方式来解释[8]。在这里，我们将以SELLF的方式编码证明系统，114诉Nigam等人理论计算机科学电子笔记269（2011）109我的世界K{|∈ W}1C W2如果i=lA）[i]，则&⎨我L⊕L负相K：K：不[] K：ΓL，A，B[]K：K：[] K：LK：[编辑]A{c/x}[k]k +1 A：r_L[？l]你好，我是说......LA正相位K：ΓK：Γ[K，给定（K1 = K2）|[C W]K：·[1，给定[]=]K：ΓA{t/x}[]K：ΓK ≤l：·l，给定[x lx/] =]我的 天！LA初始、反应和决策规则K：ΓK+1P：[D，givenl∈CW]K：ΓK+1P：ΓK：ΓK：r，P·中文（简体）K：图1.一、次指数聚焦线性逻辑系统 假设：L是公式列表，Γ是公式和正文字的多集合，Ap是正极性文字，P是非负文字，S是正 的文字或公式，N是负的公式。•（K1K）[i]=• K[S] = {K [i] |i∈ S}• （K+l）如果i∈ C <$W，则K1[ i ][i]否则· K ≤i [l]=K[l] 如果i≤l如果我• （K1*K2）|S为真当且仅当（K1[j]*K2[j]）图二. 在上下文上操作的具体化。这里，i∈I，j∈ S，S <$I，二元连接词∈{=，“macro-rules”如[14]所述，这是最强的充分性水平。本文将充分利用提升法则，！l，为了说明 证明系统的结构限制。特别地，当从结论到前提看到这个引入规则时，这个规则确定了两个不同的操作。第一个是由它的附带条件引起的：爆炸只能被引入，诉Nigam等人理论计算机科学电子笔记269（2011）109115如果不大于L的线性上下文都是空的。这个操作类似于普通线性逻辑中的提升规则：只有当线性上下文为空时才能引入bang。 Nigam和Miller在[14]中利用这一点在Andreoli的线性逻辑聚焦系统中对LJ进行编码。第二个操作是通过使用操作K≤l来指定的：在提升规则的前提下，所有不大于l的无界上下文都被擦除。请注意，这种操作在普通线性逻辑中不可用。最后，为了提高可读性，我们通常会显式地显示在索引上下文K的图像中出现的公式。例如，如果子指数索引的集合是{x 1，.， xn}，则下列负的► Θ1：x1Θ2：x2···Θn：xnγL表示SELLF矩阵K：Γ∈L，使得K[Xi]= Θi，对于所有1≤i≤n.我们还将假设存在一个称为∞的最大次指数，它允许收缩和弱化，并且大于所有其他次指数。该次指数用于存储指定证明系统的线性逻辑理论3编码证明系统类似于Church此外，在[17，16，14]之后，我们通过使用两个元级原子[·和[·|类型的形式→ O。它们分别表示出现在图的左侧和右侧的对象逻辑公式例如，在图 1 中，BnC1，.， Cm可以由SELLF序列编 码 ：∞[B1]，·· ·，[Bn]： 1[C1|，·· ·，[Cm|：r··，其中Θ对证明系统的引入规则进行编码。请注意，在SELLF中，我们可以通过相应地改变次指数签名来配置次指数l（左）和r（右）的上下文，使其表现得像集合或多集合例如，如果我们使用子指数签名<${l，r，∞}，≤，{l，∞}，{l，∞}<$，其中某些前序≤，则上下文l和∞被视为集合，而上下文r被视为多重集合。这种情况对于任何证明系统都是有用的，其中它的右边表现为公式的多集，而左边表现为公式的集合最后，为了方便起见，如果Γ是对象逻辑公式的（多）集合，则[Γ]（分别地，[Γ|）表示Meta级原子{[F]}的（多）集合|F ∈[Γ ε}（分别为{[F ||F ∈ [Γ|}）中。3.1G1m我们在SELLF中编码的第一个逻辑是最小逻辑的证明系统，称为G1m[18]，其中收缩和弱化的规则是116诉Nigam等人理论计算机科学电子笔记269（2011）109L：：：：L RLGIm∞[Γ 1，Γ 2]|[C|r·GIm∞L：R：L R：：系统和所有引入规则都是乘法的。4该系统的规则如图3所示。在那里，序列的左边和右边都被视为两个不同的公式的多集。这一点对于规则BRR和Cut尤其重要，因为在它们的结论序列右边的公式C必须移到正确的前提。因此，在SELLF中，我们将需要两个子指数l和r，它们不允许收缩或弱化，分别存储出现在左和右的对象逻辑公式。此外，我们使用图4中描述的理论LGIm在SELLF中指定G1m另一方面，这个理论存储在大于l和r的次指数∞中，并且由于引入规则可以根据需要多次用于对象逻辑证明中，因此允许∞收缩和弱化。这可以通过次指数签名{∞，l，r}，{l <$∞，r <$∞}，{∞}，{∞}来概括。直觉上，LGIm中的每个子句都指定了G1m的引入规则。为了获得这样强的对应关系，从LGIm获得的集中证明，我们需要精确地捕捉系统中的结构限制特别是使用的！1，指定规则CUTL，以及Id2，指定Cut规则，是必要的。它迫使出现在他们结论右边的副公式C移到正确的前提。这通过以下推导来说明：：：Gim∞[Γ 1]l[A|GIm∞ [Γ 2，A∈ I [C|r·l：啊！、、怎么样？L--我很好，？GIm∞[Γ 1<$l·r·！？ [A|GIm∞ [Γ 2] l [C|r·？ 【阿► LGIm∞[Γ 1，Γ 2]l[C|r·！？[A|你说呢？[AD，时间：∞当引入张量时，公式[C|不能去左边的分支，因为，在这种情况下，！could not beintroduced：为了引入这个连接词，r上下文必须为空。因此，引入公式Id2的唯一方法是使用诸如上面的推导。请注意，这种指定在普通线性逻辑中是不可能的，因为在那里，只有一个上下文可以被视为多集，而在G1m中，需要两个这样的上下文。在[13]中证明了以下形式命题3.1设Γ {C}是一组对象逻辑公式，并设子指数l和r由签名<${∞，l，r}，{l<$∞，r <$∞}，{∞}，{∞}<$指定。然后，：[Γ][C|·在SELLF中可证明，当且仅当在GIm中可证明的。：诉Nigam等人理论计算机科学电子笔记269（2011）109117∀∀⊃∀[·[·|L我L我Γ1−→AΓ2，B−→C>LΓ，A−→B<$RΓ，Ai−→C<$LΓ1， Γ2，A<$B−→CΓ−→A→BΓ，A1<$A2−→CΓ1−→AΓ2−→BΓ1，Γ2−→A<$BRΓ，A{t/x} −→CΓ，xA −→CLΓ−→A{c/x}RΓ−→γ xAΓ，A{c/x}−→C<$LΓ −→ A{t/x}<$RΓ，A−→CΓ，B−→CLΓ，xA−→CΓ−→γ xAΓ，A<$B −→CΓ −→ Ai<$RΓ −→CWA，A−→CCΓ−→A1→A2Γ，A −→CΓ，A −→CA −→AIΓ1−→AΓ2，A−→CΓ1， Γ2−→C切割图三. 最小逻辑的微积分系统GIm。 这里，Γ1， Γ2是公式的多集，C是一个公式;在规则<$L和<$R中，本征变量c在Γ和C中都不自由;且i∈{1，2}。（L） [AB（！l？r[A|你说呢？l[B]（R） [A]B|⊥ ⊗(? l[A]？r[B|）（L）[AB（？l[A]l[B]（R） [A]B|⊥⊗(? r[A|你说呢？r[B|）（L） [A B（？l [A]&？l[B]）（孟加拉国）[A] B|⊥⊗ (? r [A|你说呢？r [B|）（L） [B？l[BxX]（孟加拉国）[1998年B|你是谁？r[Bx|（L） [Bx？l[BxX]（孟加拉国）[1998年B|什么？r [Bx|（Id1）[B] |⊥（Id2）！l？r [B|你说呢？l[B]（CL）[B][CL][B] l[B] 什么？l[B）（WL）[B见图4。 理论，L吉姆，为吉姆。3.2MLJ我们现在在SELLF中编码多结论直觉演算mLJ，其规则如图5所示。为了指定mLJ，还需要两个不同的上下文。然而，与G1m不同，它们需要被视为公式集。这个限制是蕴涵和泛量化器的正确引入规则的结果。在这些规则中，所有出现在结论项右侧的副公式都必须在前提中删除，而出现在左侧的副公式保持不变。理论图6中的mlj指定SELLF中的mLJ。 像以前一样，我们利用两个次指数L和R分别存储元级原子和，但是现在我们允许对这些次指数指数的收缩和弱化 也就是说，我们使用次指数签名<${∞，l，r};{l ≤ ∞，r ≤ ∞};{∞，l，r};{∞，l，r}<$。的使用！ 在条款中（r）和（R）强制了上下文r当引入这些公式时，[4]交换规则仍然隐含地包含在一个表达式中，假设它的上下文是公式的多集而不是列表。这里使用的系统G1m在[18，备注3.1.5]中被称为上下文无关规则∧LL118诉Nigam等人理论计算机科学电子笔记269（2011）109（）[AB（？l[Alrr？[B]（二）[A]B|（？ [A|什么&？ [B|）rlmlj∞[Γ <$l[Δ，λxA|r·[A|快！艾利克斯？[斧头|L：：：：Γ，A<$B−→A， Δ Γ，A<$B，B−→ ΔΓ，A<$B −→ ΔΓ，A −→ BΓ−→AB， ΔΓ，A <$B，A，B −→ Δ <$Γ −→A<$B，A，ΔΓ −→AB，B，ΔLΓ，A<$B −→ ΔΓ，A<$B，A，−→ Δ Γ，A<$B，B−→ Δ<$LRΓ−→AB， ΔΓ−→A<$B，A，B， Δ<$Γ，A <$B−→ΔRΓ−→AB， ΔΓ，xA，A{t/x}−→ΔΓ，xA−→ΔΓ−→A{c/x}Γ−→ Δ，Δ xAΓ，xA，A{c/x}−→ΔΓ−→Δ，xA，A{t/x}Γ，xA−→ Δ Γ−→ Δ，xAΓ，A−→A， ΔIΓ −→B，ΔΓ，B −→Δ切割Γ −→ ΔΓ，π −→ Δπl图五.具有加法规则的多结论直觉演算mLJ（l）[AB（？r[A|什么&？l[A]（r）[A]B|你好！l（？l[A]？r[B|）（l）[AB（？l[A]？l[B）（r） [A B|⊥ ⊗(? r[A|？r[B|）（L）[B？l[BxR][1998年B|你好！我的天啊r[Bx|（L） [Bx？l[BxR][1998年B|什么？r[Bx|（比利时法郎） [详细]（Id1）[B][B][ B]|（Id2）？l[B] B？r[B|见图6。 多结论直觉逻辑系统mLJ.引入公式（FORMULA）：--[r]m [l]∞[r] m [l]|r·r--是吗？I∈Lmlj∞[r ∈l·r·r∈ x？ [斧头|LR中文（简体）：lr！mlj∞[Γ <$l[Δ，λxA|r·λ[λxA|Lmlj∞[Γ|r·！ 艾利克斯？ [斧头|⊗中文（简体）--D∞，► Lmlj∞[Γ <$l[Δ，λ xA|r·特别地，由于lr，在推广规则的前提下，上下文r上面的推导也说明了如何使用通用量化器指定新的值。与mLJ一样，本征变量c不能出现在Δ或Γ中。下面的结果是在集中证明[13]的高度上通过归纳证明的。命 题3.2 设ΓΔ 是一个 对象逻辑 公式集， 子命题l和 r由符号 {∞， l，r};{l≤∞ ，r≤∞};{∞，l，r};--{∞，l，r}然后，|r·r在SELLF中可证明，如果且只有当在mLJ中可证明时。3.3公司简介⊃⊃∀LRL布雷尔R诉Nigam等人理论计算机科学电子笔记269（2011）109119前面几节中的系统总是需要两个上下文，它们要么被视为多集，要么被视为集。然而，有些系统需要的不仅仅是120诉Nigam等人理论计算机科学电子笔记269（2011）109Γ，A<$B→A;·Γ，A<$B，B<$ Δ<$lΓ，A<$B <$rΓ，A<$B< $Δ Γ→A<$B;ΔΓ，A<$B，A<$Δ Γ，A<$B，B<$Δ<$l Γ <$A，B，Δ<$Γ，A<$B< $Δ Γ→A<$B;ΔΓ，A<$B，A，B<$ Δ<$l Γ→A; Δ Γ→B;Δ<$Γ，A<$B<$ ΔIΓ→C;ΔDΓ→A→B;Δ⊥Γ，A→A;ΔΓC， ΔΓ，πΔ图第七章直觉逻辑的聚焦式多结论系统-LJQ。（Id1）[A]|（ b）在任何情况下，（L） [A B（！l？f[A|快！r？l[B]（R） [A]B|你好！l（？l[A] ？r[B|）（L） [AB（！r？I[A！r？l[B]（R） [A]B|你好！r（？r[A| ？r[B|）（L）[AB！r（？l[A]？l[B]（R） [A] B|你好！r？f[A|快！r？f[B|）见图8。用于对系统LJQ进行编码的理论LJQ是LJQ编码。两个具体的上下文，例如图7中描述的直觉逻辑LJQ的聚焦多结论系统。该系统是Herbelin [7，page 78]提出的系统的变体，并由Dyckho Lengrand在[5]中使用。LJQ证明有两种类型的列式：形式为Γ Δ的无焦点列式和形式为Γ→A; Δ的有焦点列式，其中公式A在stoup中是有焦点的，证明受到如下限制：逻辑右引入规则只引入有焦点列式，而逻辑左引入规则只引入无焦点列式。我们使用图8中描述的理论Lljq来指定SELLF中的系统LJQ。除了次指数∞之外，我们还使用了三个次指数：前两个l和r和前面一样，分别用于编码对象逻辑序列的左侧和右侧，而第三个次指数f是新的，用于编码对象逻辑集中的序列。形式上，它们由签名<${f，l，r，∞}{r<$l<$∞};{l，r，∞};{l，r，∞}<$指定。注意，与前面的编码不同，子指数r和l在前序中相关，而且收缩和弱化不仅适用于f。和以前一样，聚焦规则对序列的限制是通过使用次指数来隐式编码的人们能够正确地指定限制，即积极规则只能应用于重点公式，消极规则只能在stoup为空时应用为了说明否定规则只适用于stoup是RL诉Nigam等人理论计算机科学电子笔记269（2011）109121ljql[Γ，A，B]r[Δ |f·：·[|··ljql[r]r[Δ |f·：·[AB！（怎么样？ （A？[B]DL：J：：ljq∞LRFRL空，考虑引入子句（BTL）的以下推导：中文（简体）KL：[Γ j|--r（？l[A]？l[B]！ ，2 ×？电话：ljql：R f⊥r l l⊗ljql[r]r[Δ |f·：·∞：J--其中K是上下文L[r Δ]的缩写，并且rJ是集合I.{A<$B}. 因为rf，所以上下文f必须为空才能引入！R在右支。另一方面，由于r l，l上下文在这个推导的前提中保持不变，因此精确地指定了rL引入规则。正如预期的那样，Lljq中的每个子句都精确地指定了LJQ[13]中的一个推理规则：命题3.3设ΓΔ{C}是一组对象逻辑公式，并设子指数l，r和f由签名<${f，l，r，∞}{r<$l <$}指定--∞};{l，r，∞};{l，r，∞} 那么，|f·：·可证明于SELLF当且仅当在LJQ中可证明的是π Γ π Δ。3.4用次指数图1中描述的系统和本文中列出的所有编码示例都是使用λ-Prolog实现的。在这种情况下，具有次指数的聚焦线性逻辑是对象级逻辑，而直觉逻辑的片段是元级逻辑。图1中的大多数推理规则在λ-Prolog中有一个直接的规范，只在上下文管理中有区别。加法算子和乘法算子之间的区别以及子命题的存在都与上下文控制有关。源代码可以在http://kontesti.me/ ~ giselle/SELLF/上找到。4关联元级公式和对象级规则到目前为止，我们已经展示了如何使用线性逻辑来对逻辑系统进行编码，以及子指数如何极大地增加可以编码的系统数量另一方面，很自然地会问一个线性逻辑公式是否对应于一个推理规则的一个具体化在[2]中，Agata等人介绍了一个系统的程序， 线性逻辑公式转换为等价的结构推理规则在微积分和超微积分。在这项工作中，定义了类Ni和Pi，使得NiNi+1，Ni<$Pi+1，Pi<$Pi+1，Pi<$Ni+1和Pi使用正连接词构建，而Ni使用负连接词构建。虽然这个定义过于直观，没有指数的线性逻辑，可以直接将这些类扩展到整个线性逻辑。，2×100122诉Nigam等人理论计算机科学电子笔记269（2011）109N N定义4.1一个非同步公式是一个线性逻辑公式，它只包含异步连接词的出现，即，T，和模态？，它只能有原子范围。双极是一个公式，其中没有同步连接词在异步连接词的范围内，在哪里？原子的范围。因此，单极是在N1，而双极是在P2，都与限制，？必须具有原子范围。在[2]中有两个主要结果：1）N2中的每个公理等价于一个有限的结构规则集; 2）P3中的每个公理等价于一个有限的超结构规则集。 事实证明，在我们的方法中，我们可以完全刻画P2中的公式。事实上，由于双极定义了合成的连接词，这些公式中的每一个都确定了一个微积分推理规则。例如，线性逻辑公式A（BC）确定一个宏规则：K1：Γ1► K1<$K2：Γ1， Γ2<$A<$（BC）为了将其与对象级逻辑联系起来，我们引入了引入子句的概念。定义4.2设Q是一个固定的一元谓词集合引言从句是一个封闭式公式，其形式为10000.. . n[q（x1， . ，xn））（x nB]其中n是n（n≥0）元的对象级连接符，q∈ Q，B是双极的。此外，出现在B中的原子的形式为p（xi）或p（xi（y）），其中p是元级谓词且1≤i≤n。在第一种情况下，xi具有0阶类型，而在第二种情况下，xi具有1阶类型，并且y是在B中量化（普遍或存在）的变量（特别地，y不在{x1，...， xn}）。下一个结果（通过对结构的直接案例分析证明双极公式）指出，介绍子句自然产生对象级推理规则。命题4.3每一个介绍子句（因此在P2中）对应于一个微积分介绍规则的一个具体化。有一些有趣的问题与这个主题有关。例如，如何使用线性逻辑来建模超序列还不清楚（因此我们不知道如何处理类P3）。对于类Ni，i≥3，我们有如下结果。定理4.4在Ni，i ≥ 3中存在不对应于对象级推理规则的任何指定的引入子句。证据 下面证明了上述定理，其中n = 3，由于ij，j，结果出来了。考虑以下非双极的诉Nigam等人理论计算机科学电子笔记269（2011）109123（C） [A][B][C]|&[B]（英） [英]|⊥⊗[A♩[B|.（C）[A][B][A][B]。（英） [英]|[A]|&[B|.（英） [英]|[A]|[B|.（C）[A][B][A]&[B]。（fcL）[fcL] T.见图9。 G3C的规格。机构：5个[o（A，B，C）|电子邮件（[A|&（[B|中文（简体）|））[o（A，B，C）（[A（[B[C））如果它们要对应于可重构推理规则的编码候选人将Γ1， Γ2< $Δ1， Δ2，AΓ1< $Δ1，BΓ2<$ Δ2，CΓ1， Γ2< $Δ1， Δ2，<$（A，B，C）事实证明，在Meta层面上，Γ，A ΔΓ，（A，B，C）<$ΔΓ，B，CΓ，（A，B，C）<$Δ► （Id1）：·[A|&（[B| 中文（简体）|）、[A（[B）]是可能的，而在对象层次上，上面列出的两条规则不能用来证明（A，B，C）.这个公理只能通过直接应用初始公理来证明。因此，对象级推理规则的元级编码在该非双极示例中是不够的。Q4.1规则的可逆性另一个在微积分中研究过的性质是规则的逆运算.我们说一个规则是可逆的，如果结论的可证明性蕴涵着所有前提的可证明性这个属性对证明搜索非常感兴趣，因为可逆规则与证明的其他规则一起排列，从而减少了证明搜索的非确定性。特别是，在只有可逆规则的系统中，自底向上的证明搜索可以在达到不可证明的条件时立即停止例如，众所周知，G3c（见[18]）中的所有规则都是可逆的。 该系统如图9所示。注意，主体中的Meta级别连接词是异步的。一般来说，下面是一个简单的结果。定理4.5一个简单的引入子句对应于一个可逆的对象级规则。5结论和今后的工作我们已经介绍了逻辑框架SELLF，并展示了如何指定不同的逻辑系统。此外，我们还解决了表征线性5注意这些子句在N3中，因为它们等价于公式[o（A，B，C）] |−（[A|&（[B|中文（简体）|））和[o（A，B，C）<$$> −（[A<$$>（[B <$[C <$））]）。124诉Nigam等人理论计算机科学电子笔记269（2011）109逻辑公式作为推理规则，以及可逆规则。有几种方法可以继续这项工作。事实上，在[11]中，为了保证特定系统具有割消性质，给出了一个必要条件。这个结果是基于这样一个事实，即切割消除往往是通过案例分析证明，其中推理规则的对偶性在消除非原子切割中起着重要作用。这是翻译到元水平的“对偶”线性逻辑公式。将这个结果推广到具有次指数的线性逻辑会很有趣，因为在本文中指定的大多数系统中，在元级上证明割消真的很难。另一个研究方向是指数多聚焦通过这种方式，扩展了证明搜索对应于顺序算法的概念，如[13]所述引用[1] 让-马克·安德雷奥利逻辑程序设计与线性逻辑中的聚焦证明。J. of Logic and Computation，2（3）：297[2] Agata Ciabattoni，Nikolaos Galatos，和Kazushige Terui.从公理到非经典逻辑的分析规则。在LICS[3] 阿朗佐·丘奇简单类型论的一个公式 J. 《符号逻辑》，5：56 -68，1940。[4] 文森特·达诺斯，让-巴蒂斯特·儒瓦内，哈罗德·谢林克斯。指数的结构：揭示线性逻辑过程的动力学。KurtGöodelCo ll oquium，1993年。[5] R. Dyckho和S.朗格朗LJQ：一个强聚焦的直觉逻辑演算在2006年的CiE[6] 格哈德·根岑对逻辑推理的研究。《格哈德·根岑文集》，第68-131页。1969年阿姆斯特丹北荷兰[7] 雨果·赫尔·贝 林 。计算的 结果：对计算结果的解释与对数据的计算结果相同，也与对数据的计算结果相同。PhDthesis，Uni versi t'eParis7，1995.[8] 查克·梁和戴尔·米勒。线性、直觉与古典逻辑中的聚焦与极化Theoretical Computer Science，410（46）：4747[9] S.前原直觉主义逻辑在古典学中的一个分支。名古屋数学杂志，第45-64页[10] 戴尔·米勒。论坛：一个多结论规范逻辑。Theoretical Computer Science，165（1）：201[11] 戴尔·米勒和伊莱恩·皮门特尔。使用线性逻辑来推理系统。在02年的桌子上Springer，2002年。[12] 戴尔·米勒和伊莱恩·皮门特尔。线性逻辑作为一个框架，为指定微积分。在逻辑学术讨论会[13] 维韦克·尼加姆利用微积分中的非正则性。2009年9月，巴黎综合理工学院博士论文[14] 维韦克·尼加姆和戴尔·米勒专注于线性元逻辑。在IJCARSpringer，2008.[15] 维韦克·尼加姆和戴尔·米勒线性逻辑中的次指数规范。在PPDP 09，2009。[16] ElaineGou诉Pime。L'ogicaline e areaes peci ficapassicpassiaodesistemascomputacionais.博士论文，米纳斯吉拉斯联邦大学，贝洛奥里藏特，M.G.，巴西，2001年12月。 用英语写的。[17] 伊莱恩·皮门特尔和戴尔·米勒。 关于系统的规范 在LPAR[18] 安妮·S Troelstra和Helmut Schwichtenberg。 基本证明理论 剑桥大学出版社，1996年。