↓これの続きでこざる。 cut-elimination.hatenablog.com シーケント計算 シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなん…

↓これの続きでっせ。 cut-elimination.hatenablog.com 3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。 Chapter 3 カリー=ハワード同型 命題を型と対応させる。型付項のシステムにおいても sense と den…