序列演算 / 相继式演算：数理逻辑（尤其是证明论）中的一种形式化推理系统，用“序列（sequent）”来表达从一组前提推出结论的关系，常写作
(\Gamma \Rightarrow \Delta)（直观理解为“在前提集合 (\Gamma) 下，可推出结论集合 (\Delta)”）。
常用于研究证明结构、可判定性与消去割（cut-elimination）等性质。（该术语也可在更广义的逻辑系统讨论中出现。）
/ˈsiːkwənt ˈkælkjʊləs/
Sequent calculus is used in proof theory.
序列演算用于证明论。
By translating the argument into sequent calculus, we can analyze the proof steps and see whether the cut rule can be eliminated.
把论证改写成序列演算后，我们可以分析证明步骤，并判断是否能消去割规则。
sequent 来自拉丁语 sequi（“跟随、由此推出”），表示“由前提相继推出结论”的形式；calculus 来自拉丁语 calculus（“小石子”），古人用小石子计数，后来引申为“演算/计算体系”。“Sequent calculus”作为术语与体系主要由德国逻辑学家 Gerhard Gentzen（根岑）在 1930 年代建立，用来刻画形式证明的规则与结构。
Select Language