自然演绎 编辑
在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。这种方式对比于使用公理的公理系统。
1
相关
在证明论和数理逻辑中，相继式演算是一阶逻辑、模态逻辑等逻辑的一类证明演算。第一个相继式演算



L
K


{\displaystyle LK}

和



L
J


{\displaystyle LJ}

由格哈德·根岑在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。
在证明论和数理逻辑中，相继式演算是一阶逻辑、模态逻辑等逻辑的一类证明演算。第一个相继式演算



L
K


{\displaystyle LK}

和



L
J


{\displaystyle LJ}

由格哈德·根岑在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。
在数理逻辑中，特别是联合上证明论的时候，一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用：结构规则的概念是基于相继式表达，而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑和线性逻辑。