法則としてのシーケント

記号的には、

• [x₁:t₁, ..., x_k:t_k | A₁, ..., A_n |- B]
• 最初はk個の変数型宣言。型理論で言う型環境。
• 次にn個の前提（仮説）論理式。
• 1個の結論論理式。
• 出現するすべての変数は型環境で型付けされている。

自然言語風の記述は：

for

 x1:t1, ..., xk:tk

given

  A1

  and

  ...

  ...

  and

  An

shows

  B

この意味を単一の論理式で書くなら、

• ∀x₁:t₁, ..., x_k:t_k.(A₁∧ ... ∧A_n)⇒B

αが法則（公理、定理）としてのシーケンのとき、

• apply α to β1, ..., βp

の形で適用できる。

β1, ..., βp を A₁, ..., A_n とマッチングして、ユニフィケーションの結果であるユニファイヤをΘとする。マッチングで残った前提を A'₁, ..., A'_q として、適用（apply）の結果は、

• [x'₁:t'₁, ..., x'_l:t'_l | A'₁[Θ], ..., A'_q[Θ] |- B[Θ] ]

適用結果はシーケントなので、適当に論理式にして結果とする。

アルゴリズム的にはユニフィケーションがキモ。