シークエント計算（シークエントけいさん、英: Sequent calculus）は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。

シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。
LK

シークエント計算ではシークエントの列で証明が記述され、各シークエントは証明過程で既に出現したシークエントに後述する推論規則を適用することで導出される（シークエントとは、命題群の論理積を前提とし、別の命題群の論理和を帰結とする論理的帰結関係を表す論理式の並びである）。
歴史

シークエント計算 LK は1934年、ゲルハルト・ゲンツェンが自然演繹を研究する道具として生み出した。その後、論理導出を行うのに非常に有効であることから普及した。LK（エルケー、エルカー） という名称はドイツ語の Logischer Kalkul（論理計算）に由来する。
LK の推論規則

ここでは、以下のような記法を用いる:

横線の上の論理式が与えられたとき、横線の下の論理式が推論によって導出されることを示す。

A {\displaystyle A} や B {\displaystyle B} は一階述語論理の論理式を表す（命題論理の論理式に限定する場合もある）。

Γ , Δ , Σ {\displaystyle \Gamma ,\Delta ,\Sigma } や Π {\displaystyle \Pi } は有限個（0個もありうる）の論理式の列であり、コンテキスト（文脈）と呼ぶ。

t {\displaystyle t} は任意の項を意味する。

A [ t / v ] {\displaystyle A[t/v]} は A {\displaystyle A} 内の変項 v {\displaystyle v} の全ての自由出現を項 t {\displaystyle t} で置換した論理式を表すが、 t , v , A {\displaystyle t,v,A} は「 t {\displaystyle t} 内のいかなる変項のいかなる自由出現もこの置換によって新たに束縛されない」という（代入可能）条件を満たすものとする。たとえば、 ∀ x ( p ( x , v ) ) {\displaystyle \forall x(p(x,v))} （ p {\displaystyle p} は 2 項述語、 x , v {\displaystyle x,v} は異なる変項）の v {\displaystyle v} の自由出現を x {\displaystyle x} で置換することは許されない。

x {\displaystyle x} や y {\displaystyle y} は（同じでもよい）変項を表す。

量化子 ∀ {\displaystyle \forall } や ∃ {\displaystyle \exists } で束縛されない変項を自由変項と呼ぶ。

W L {\displaystyle WL} は Weakening Left、 W R {\displaystyle WR} は Weakening Right、 C L {\displaystyle CL} と C R {\displaystyle CR} は Contraction、 P L {\displaystyle PL} と P R {\displaystyle PR} は Permutation の略である。

公理:カット:
A ⊢ A ( I ) {\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)} Γ ⊢ Δ , A A , Σ ⊢ Π Γ , Σ ⊢ Δ , Π ( C u t ) {\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})}
左論理規則:右論理規則:
Γ , A ⊢ Δ Γ , A ∧ B ⊢ Δ ( ∧ L 1 ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})} Γ ⊢ A , Δ Γ ⊢ A ∨ B , Δ ( ∨ R 1 ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})}
Γ , B ⊢ Δ Γ , A ∧ B ⊢ Δ ( ∧ L 2 ) {\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})} Γ ⊢ B , Δ Γ ⊢ A ∨ B , Δ ( ∨ R 2 ) {\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})}
Γ , A ⊢ Δ Σ , B ⊢ Π Γ , Σ , A ∨ B ⊢ Δ , Π ( ∨ L ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)} Γ ⊢ A , Δ Σ ⊢ B , Π Γ , Σ ⊢ A ∧ B , Δ , Π ( ∧ R ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)}
Γ ⊢ A , Δ Σ , B ⊢ Π Γ , Σ , A → B ⊢ Δ , Π ( → L ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)} Γ , A ⊢ B , Δ Γ ⊢ A → B , Δ ( → R ) {\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)}
Γ ⊢ A , Δ Γ , ¬ A ⊢ Δ ( ¬ L ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)} Γ , A ⊢ Δ Γ ⊢ ¬ A , Δ ( ¬ R ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)}