相继式演算

在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类证明演算。第一个相继式演算由格哈德·根岑（Gerhard Gentzen）引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演绎混淆。自然演绎、公理系统和相继式演算是常见的证明演算。
相继式演算是逻辑研究的重要工具。许多逻辑学者会为其所研究的逻辑构造出一个或多个相继式演算，并研究其性质（如切消定理）。

LK系统

在这个演算中的（形式）证明是一序列的相继式，这个的每个相继式使用下面的推理规则之一而推导自更早出现的相继式。

直觉解释

上面的规则可以被分成两个主要群组：逻辑规则和结构规则。每个逻辑规则都在十字转门的左边或右边介入一个新的逻辑公式。相反的，结构规则操作在相继式的结构上，忽略公式的准确形状。这个一般模式的两个例外是同一性公理和规则切。
尽管是以形式方式陈述的，上述规则允许用经典逻辑的方式非常直觉的读出来。比如，考虑规则。它陈述了如果你能证明可以从包含的公式序列推导出来，则你也能证明自更强的假定，也就是成立。类似的，规则陈述了如果和足够推导出，则从单独的你可以要么仍然推导出要么必然为假，就是说成立。所有规则都可以用这种方式来解释。
对于量词规则的直觉解释，考虑规则。当然只从为真的事实推导出成立一般是不可能的。但是如果变量在其他地方没有被提及（就是说，它仍可以被自由的选择，而不影响其他公式），则你可以假定，对的任何值都成立。其他规则应当是非常直接的。
不再把规则看作是对在谓词逻辑中合法的推导的描述，你还可以把它们当作为给定陈述构造一个证明的指导。在这种情况下规则可以自底向上的读。例如，声称要证明推导自假定和，分别证明可以推导自和可以推导自就足够了。注意，给顶某个前件，如何分解成和是不明确的。但是，只有有限多的可能需要检查，因为前件被假定为是有限的。这也展示了证明论如何被看作是以组合方式在证明的操作：给定对和二者的证明，你可以构造一个对的证明。 
在查找某个证明的时候，多数规则提供或多或少的如何做的处方。切规则是不同的：它声称，在公式可以被推导出来，并且这个公式也可以充当推导其他公式的前提的时候，则公式可以被"切掉"并把各自的推导连接起来。在自底向上构造一个证明的时候，这产生了猜测的问题（因为它在下面根本就没有出现）。这个问题在切消定理中处理。
第二个规则有某种特殊性，它就是同一性公理。明显的直觉读为：证明。

结构规则

结构规则需要某些额外的讨论。规则的名字是弱化（）、紧缩（）和排列（）。紧缩和排列确保序列元素的次序（）和多次出现（）都不重要。就是说，你可以不把它当作序列而作为集合。
但是使用序列的额外努力是正当的，因为部分或全部的结构规则可以被忽略。这么做了就得到了所谓的亚结构逻辑。

LK系统的性质

这个规则系统可以被证明关于一阶逻辑是可靠的和完备的，就是说，从前提的集合Γ语义上得到的一个陈述，当且仅当相继式可以用上述规则推导出来。
在相继式演算中，切是可接纳的。这个结果也称为Gentzen的Hauptsatz（"主定理"）。

变体

上述规则可以以各种方式修改：

次要结构变更

有些修改不改变系统的本质。所有这些修改都仍可以叫做系统。
首先，如上面提及的，相继式可以被看做由集合或多重集组成。在这种情况下，排列和（在使用集合的时候）紧缩公式的规则就可以废弃了。
弱化规则也变成是可接纳的了，在公理被变更的时候，使得形如的任何相继式都可以被得出。这意味着在任何上下文中证明。在推导中的任何弱化因此可以在开始处正确的进行。在自底向上构造证明的时候这是个方便的变更。
独立于这些修改，你还可以在规则内上下文被分割的方式：在、和的情况下，在向上走的时候，左上下文被以某种方式分割成和。因为紧缩允许它们的重复，你可以假定全部上下文在两个推导分支中都使用。通过这么做，你能确保没有重要的前提在错误的分支中被丢失。使用弱化，上下文中无关的部分以后可以被消去。
所有这些改变生成等价的系统，这是在LK中的所有推导可以有效的变换因使用了替代规则的推导反之亦然的意义上。

亚结构逻辑

人们可以限制或禁用某个结构规则。这产生了亚结构逻辑系统变体。它们一般要弱于（就是说有更少的定理），因为关于标准的一阶逻辑语义是不完备的。但是它们的其他有趣性质导致其在理论计算机科学和人工智能中的应用。