在证明论和数理逻辑中,相继式演算是一阶逻辑、模态逻辑等逻辑的一类证明演算。第一个相继式演算
L
K
{\displaystyle LK}
和
L
J
{\displaystyle LJ}
由格哈德·根岑在1934年/1935年引入,作为研究自然演绎的工具;它的名字得来自德语的“Logischer Kalkül”,意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统,但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。
1
切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中,拥有利用了切规则的证明的任何判断,也拥有无切证明,就是说,不利用切规则的证明。