パズル的な問題を知識論理で書いてみた

こんな問題見かけました。

2≦m≦n なる自然数(m,n)に対し,Aはm*nの値のみを知っている,Bはm+nの値のみを知っている.A「m+nの値は分からない」B「君がそう言うことは分かっていた」A「まだm+nの値は分からない」B「m+nは14未満だ」A「mとnが分かった」B「私も分かった」さてm,nは?
http://twitter.com/#!/kakenman/status/139943992283496448

こういうのを一度きちんと知識論理使って書いてみたかったのでやってみた。

  •  W_0 = \{ (m, n) | 2 \leq m \leq n \}
  •  (m, n) R_A (m', n') iff  mn = m'n'
  •  (m, n) R_B (m', n') iff  m+n = m'+n'

として, W \subset W_0, x \in W に対して  x ||\hspace{-5}- !_A を「 x R_A y, y \in W ならば  x=y」であることと定義しましょう。 !_B も同様に定義します。このとき

 W_1 = \{ x \in W_0 | W_0, x ||\hspace{-5}- K_B \neg !_A \}

とすると,これは A「m+nの値は分からない」B「君がそう言うことは分かっていた」 のやりとりが発生しうる (m, n) の全体となります。以下同様に

  •  W_2 = \{ x \in W_1 | W_1, x ||\hspace{-5}- \neg !_A \}
  •  W_3 = \{ (m, n) \in W_2 | m + n < 14 \}
  •  W_4 = \{ x \in W_3 | W_3, x ||\hspace{-5}- !_A \}
  •  W_5 = \{ x \in W_4 | W_4, x ||\hspace{-5}- !_B \}

がそれぞれ A「まだm+nの値は分からない」B「m+nは14未満だ」A「mとnが分かった」B「私も分かった」 に対応して,最終的に  W_5 に入っているものが解となります。

たぶん。