シークエント計算
sequent calculus
シークエント
の列を用いた演繹手法
既に出現したシーケントに対し、推論規則を適用し、結論を導出していく
推論規則
の形は以下のいずれか
$ \frac{S_1}{S}
sequeent
$ S_1
が成り立つならば、
$ S
も成り立つ
$ \frac{S_1\; S_2}{S}
sequent
$ S_1
と
$ S_2
が共に成り立つならば、
$ S
も成り立つ
参考資料
/mrsekut-book-4007305803/046 (命題論理のシーケント計算)
/mrsekut-book-4007305803/078 (一階述語論理のシーケント計算)
/mrsekut-book-4007305803/108 (命題様相論理のシーケント計算)
『情報科学における論理』
p.23~
かなり丁寧に色々書かれている