结构规则, 在证明论中, 是不提及任何逻辑连结词的推理规则, 它直接操作于判断或相继式, 通常模仿逻辑的元理论性质, 拒绝一个或多个的逻辑被归类为亚结构逻辑, 常见, 编辑弱化, 这里的相继式的假设或结论可以扩展到额外的数目, 在符号形式中弱化规则可以写为Γ, displaystyle, frac, gamma, vdash, sigma, gamma, vdash, sigma, nbsp, 在十字转门的左侧, displaystyle, frac, gamma, vdash, sigma, gamma, vda. 在证明论中 结构规则是不提及任何逻辑连结词的推理规则 它直接操作于判断或相继式 结构规则通常模仿逻辑的元理论性质 拒绝一个或多个结构规则的逻辑被归类为亚结构逻辑 常见结构规则 编辑弱化 这里的相继式的假设或结论可以扩展到额外的数目 在符号形式中弱化规则可以写为G S G A S displaystyle frac Gamma vdash Sigma Gamma A vdash Sigma nbsp 在十字转门的左侧 和 G S G A S displaystyle frac Gamma vdash Sigma Gamma vdash A Sigma nbsp 在右侧 紧缩 这里的在相继式同一侧两个相等的 或可合一的 成员可以替代为单一的一个成员 或公共实例 符号化为 G A A S G A S displaystyle frac Gamma A A vdash Sigma Gamma A vdash Sigma nbsp 和 G A A S G A S displaystyle frac Gamma vdash A A Sigma Gamma vdash A Sigma nbsp 在使用归结原理的自动定理证明中也叫做因子化 在经典逻辑中称为蕴含的幂等性 交换 这里的在相继式同一侧的两个成员可以对换 符号化为 G 1 A G 2 B G 3 S G 1 B G 2 A G 3 S displaystyle frac Gamma 1 A Gamma 2 B Gamma 3 vdash Sigma Gamma 1 B Gamma 2 A Gamma 3 vdash Sigma nbsp 和 G S 1 A S 2 B S 3 G S 1 B S 2 A S 3 displaystyle frac Gamma vdash Sigma 1 A Sigma 2 B Sigma 3 Gamma vdash Sigma 1 B Sigma 2 A Sigma 3 nbsp 这也叫做排列规则 没有任何上述结构规则的逻辑将把相继式解释为纯粹的序列 带有交换规则它们就是多重集 带有紧缩和交换规则二者它们就是集合 最著名的结构规则叫做切 证明论理论家花了相当的努力来证实切规则在各种逻辑中是多余的 更严格的说 证实了切只是 某种意义上 简化证明的工具 不能增加可以证明的定理 成功消除了切规则叫做切消定理 直接有关于规范化计算 参见lambda 演算 的哲学 它经常对给定逻辑的判定的复杂性给出好的指示 参见 编辑相继式演算 亚结构逻辑 线性逻辑 仿射逻辑 严格逻辑 有序逻辑 取自 https zh wikipedia org w index php title 结构规则 amp oldid 77964513, 维基百科,wiki,书籍,书籍,图书馆,