文系の人間にとって、シークエント計算は自然演繹に比べると習得するのが少し難しい。たぶん、練習問題をたくさん解くのが遠回りなようで早道なのだが、証明図を書く練習をするのに便利なサイトを知った。
古典命題論理、直観主義命題論理、様相命題論理、線形論理のシークエント計算を扱っている。結合子の数がやたらと沢山ある線形論理の証明図を書く練習ができるのがよいと思う。
あと、使い道が全然分からないのだが、条件法の論理の証明図を勝手に書いてくれるサイトを見つけた。
このサイトで扱っている論理はどれも決定可能なので、妥当でない式を書いた場合には"invalid"と表示される。validな場合には証明図のpdfが出力される。それはいいのだけど、ルイス『反事実的条件法』で論じられているV論理は（たぶん）何一つこのプログラムでは扱えなさそう。
