RCOのコーディング試験の出題例の「相手の思考を推理する」 https://www.rco.recruit.co.jp/career/engineer/entry/pastexam の問題を解いてみた。 https://gist.github.com/msakai/7b21398085d62b8a4f3c
* 知識論理の基本的な応用だと思うのだけれど、そういう解き方は思いつかず、ナイーブにシミュレータを再帰的に呼び出してしまった。
* 小規模な問題なのでやらなかったけど、メモ化した方が良いかも。
* これCoqやAgdaで満たすべき性質を定義するにはどうしたら良いかな?