漠然として思ってるんだけど、
ゲンツェン流の形式的体系でシーケントを使うのあるじゃないですか
で、カット除去定理の証明に見られるように証明図をグラフ理論でいうところの｢木｣に見立てることってあるじゃないですか
じゃあ、いっそのこと、証明図をグラフ理論の知識を使って解析してほしいなって思うんですよ