業務研究・今週のまとめ

いつのまにか、私は様相述語論理の専門家ということになってしまった。内容は面白い。っていうか Kripke frame が役に立たない。だから証明論的な体系をコンピューター上の定理証明支援系(Agda)に実装することになる。・・・これって、「意味論」と呼んでいいのだろうか。