業務研究の内容（Agdaで知識様相論理の体系を実装する）について発表しました。発表の出来はそれなり、会場の受けは一応好評でした。要旨は以下の通りです。 目的: 知識様相論理の意味論を証明支援系に実装 二つの問題点 多変数述語を持つ型のデータ型の定義…

曇り、時々雪が降る。起床は10時、早めに出発。昼前には大学に到着。13時からワークショップ、17時半まで。その後Og先生の車で4人で金沢市内の温泉へ行き、それから片町の中華料理店「幸's」で懇親会（エビがおいしい）。その後、ノドグロとフキノトウの天ぷ…