コンパクト有向シーケント計算／高次シーケント計算の動機

1. 自然演繹の欠点を克服したい。
2. 自然演繹とシーケント計算を別々に扱うのではなくて、融合・統合して一体として扱いたい。
3. 証明オブジェクトと証明オブジェクトの操作であるリーズニングを区別したい。そして、曖昧性を排除したい。
4. 人間が通常行っている混合証明／混合リーズニング（混合証明オブジェクトの操作）を定式化したい。
5. 特に、トンネル論法（両端から掘り進めて中間地点で出会う）を合理化したい。
6. アブダクションの定式化をしたい。
7. 科学的帰納法など、科学的論理の定式化をしたい。

ちなみに、トンネルで片方から掘るのは「片押し」と言うらしい。両側から掘る際の誤差は、2016年6月開通のスイス「ゴッタルドベーストンネル」（全長57km、現在世界最長の鉄道トンネル）の出会い時の誤差は8cm程度とのこと。すげーな。