在
证明论和
数理逻辑中,相继式演算(又译矢列演算、矢列式演算)是众所周知的
一阶逻辑(和作为它的特殊情况的
命题逻辑)的演绎系统。这个系统也叫做LK系统,用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。
在
证明论和
数理逻辑中,相继式演算(又译矢列演算、矢列式演算)是众所周知的
一阶逻辑(和作为它的特殊情况的
命题逻辑)的演绎系统。这个系统也叫做LK系统,用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。
相继式演算LK由Gerhard Gentzen介入为研究
自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的Logischer Kalkül
在
数理逻辑中,自然演绎是
证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。这种方式对比于使用
公理的
公理系统。