Deep inference
午後の発表は、所長による研究所の紹介と、Alessio Guglielmi氏による "deep inference" の紹介。
"deep inference"は、Girardによる"Gemoetry" から発達した証明論の技法の一つ*1で、「exchange ruleなどの官僚主義的な瑣末にとらわれることなく、contraction ruleや論理定項の導入規則などの証明論的に重要な部分をグラフィカルに分析し、取り扱う」ことを目標とする。こうすることで、例えば証明の正規化が非常に簡単になるなどのメリットがある（が、現時点ではカリー・ハワード対応がこの体系では証明できないなどのデメリットもある）。
本人による解説ページがこちらなので、ぜひご覧ください。とてもユニークです。特にDeep Inference in One Minuteがおすすめ。
