CLC

16:00-17:00

線形時間論理の2つのシーケント計算体系の同等性およびcut除去の概要、また分岐時間論理の拡張 4CTL*（4-valued CTL）、 4LCTL* （4CTL+場所）の紹介。背景説明が主。

17:00-18:00

プログラム更新システムのプロトコルの、 信念を表すBAN logicを用いて行なった安全性検証の紹介。BAN Logicを使わずとも、普通の一階論理に信念を表す公理を導入して理論化すれば十分じゃないかとの意見を巡って議論。
･･･って、似た反論は曖昧性に関する議論で私も受けたことがあったなぁ･･･論理に関する複数主義か、伝統的な一階論理上の「理論」か、こういう話では必ず問題になる点ではあります。