ヒビルテ(2008-02-04)λ. Alloyで知識論理を使って論理パズルを解く bonotakeさんの日記で時々取り上げられているAlloy、パズルを解くのに便利とのことなので、ちょっと週末に遊んでみた。 対象とするのは、以前にSPASSで知識の論理を使って論理パズルを解く?でも取りあげた「赤いぼうし」の問題で、これは以下のような問題。 AさんとBさんがいて、少なくとも一人は赤い帽子を被っていて、赤い帽子を被っていない人は白い帽子を被っている。ただし、二人とも他人の帽子の色は分かるが、自分の被っている帽子の色は分からない。そして、Aさんが「自分の帽子の色が分からない」と発言した。このとき、Bさんの被っている帽子の色は何か? そして、Bさんは自分の被っている帽子の色が分かるか? この前提となる状況をAlloyでは以下のようにモデル化することが出来る。 -- 世界 sig W { K_a: set W, -- 「Aさんが
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20060423
