2015-11-14から1日間の記事一覧

contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら,シーケント計算の推論規則を ∧右,∨左,⊃左は additive ∧左,∨右 は multiplicative にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いよう…