Alloyで知識論理を使わずに論理パズルを解く

• Alloyで知識論理を使って論理パズルを解く- ヒビルテ (2008-02-04)

うーん、命題を指標にするのかー。

と感心しつつ、自分も眠気覚ましに解いてみました。途中様相論理をものすごく使いたくなったけど、敢えて使わない方針で。ちょっと嘘くさいんだけど。

-- Aさん、Bさん
abstract sig Person {
  wears: some Hat, -- 被っている帽子と思われるものの「集合」
}
one sig A, B extends Person {}

-- 帽子（赤を被らない人は白、はここの定義で言えている）
abstract sig Hat {}
sig RedHat, WhiteHat extends Hat {}

fact Rules {
  -- 少なくとも一人は赤い帽子を被っている
  some p: Person | p.wears in RedHat
  -- 帽子の数は人数分
  #Hat = 2
}
-- （相手の帽子の色を）知っている
pred knows(p: Person) {
  p.wears in RedHat || p.wears in WhiteHat
}

様相論理を使わない代わりに、AさんとBさんが被ってる帽子 'wears' を集合にしてやりました。で、

• どの帽子を被ってるのがわかっている ⇔ wears の集合が、赤の帽子か白の帽子かのどちらかに含まれる
• どの帽子を被ってるのがわかっていない ⇔ wears の集合に、赤帽子も白帽子も含まれる

という勝手な解釈で。非決定性を扱うのにリストで表現するようなもんです（本当か？）
Alloyという言語は述語論理と集合論のミクスチャーなんで、そこいらへんうまく使い分けると便利。（逆に、初学者にはひたすら混乱の元になってる気もしなくもないですが）

で、モデルのインスタンスがあるかチェック…するんだけど、見た目的に面白くないので絵は省略。記述はたとえばこんな感じで。

pred show() {
  knows[B]
}
run show for 10

で、下記アサーションで反例なしです。

assert BsHatInRed {
  (knows[B] and not knows[A]) => B.wears in RedHat
}

check BsHatInRed for 8

んー、やっぱちょっと嘘くさいんですがね。きちんとした解は、元記事のさかいさんをご参考に。