シークエントの列を用いた演繹手法

既に出現したシーケントに対し、推論規則を適用し、結論を導出していく

推論規則の形は以下のいずれか

\frac{S_1}{S}

sequeent S_1が成り立つならば、Sも成り立つ

\frac{S_1\; S_2}{S}

sequent S_1とS_2が共に成り立つならば、Sも成り立つ

参考資料

『情報科学における論理』 p.23~

かなり丁寧に色々書かれている