（Taitの？）片側シーケント計算が結局の所どういう点で証明論的な分析や形式化において良い点があるのかをいまいち把握出来ていないのと、様相論理のシーケント計算におけるそれの文献は遥かに無さそうという点で迷っている（GLのTait計算は見たことがあるが論文は結局読めていない）