「様相論理の証明支援系上の実装」

業務研究の内容（Agdaで知識様相論理の体系を実装する）について発表しました。発表の出来はそれなり、会場の受けは一応好評でした。要旨は以下の通りです。

• 目的: 知識様相論理の意味論を証明支援系に実装
• 二つの問題点
  1. 多変数述語を持つ型のデータ型の定義が難しい
  2. 充足関数の再帰的定義が停止判定に合格しない
• 解決法
  1. ベクトルを使用
  2. 論理式のデータ型の情報量を増やす: P(x,y)を二変数述語とする。論理式 のデータ型として
     • 従来: Fml 1 （一変数述語）
     • 今回: （二変数のうち一変数が束縛されている）

この増えた情報量によって、帰納法を行うことで、停止判定を合格させる定義が可能になる

この内容の正式報告は、3月中盤の情報処理学会で発表します。