Tait計算
メモ
シークエント計算におけるシーケント$ \Gamma \Rightarrow \Deltaの$ \Gamma \Rightarrowの部分を取り払って，$ \Deltaの論理式として現れるものに制約をかけた計算体系であるとされる? Tait計算では論理式の集合（列でもいいが，どのみち構造規則によって同一視出来る?）をシーケントという． 全ての論理式が否定標準形の形に正規化できるという事実などを使って$ \Deltaに現れる論理式を巧妙に設計するところにミソがあるらしい． シークエント計算っぽい体系で，定理証明支援系などで形式化するときにコンパクトで良いということが知られている そんな…
出典
本当に出典が少ない．