檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2009-03-10 (火)

長男に教わったパズル

| 11:29 | 長男に教わったパズルを含むブックマーク

一郎、二郎、三郎の三人で駆けっこをして、その結果を次のように言っています。

一郎:「僕は一番じゃない」
二郎:「僕は一番だ」
三郎:「僕は二番だ」

三人のなかで一人だけウソをついています。それは誰でしょう?


これは、論理的な推論というより、メタ論理的な推論の例ですね*1。モデルの存在/非存在に基づいて公理系(あるいはセオリー)の充足可能性をチェックするって話じゃないのかな。

*1:もっとも、論理学(ロジック)における議論のほとんどはメタ論理的ですがね。

kosakikosaki 2009/03/10 11:55 1位:二郎
2位:三郎
3位:一郎

おお、うそつきはいませんでした。よかったよかった(^^)/

bonotakebonotake 2009/03/10 12:14 > モデルの存在/非存在に基づいて公理系(あるいはセオリー)の充足可能性をチェックする

最近の形式仕様記述に使う「モデル発見器」ってのがまさにそのノリですね。形式仕様を書いて、充足するモデルがあるかどうかで妥当性をチェック→ 変なモデルが出てきたら or 何にも出てこなかったら仕様書き換え → またチェック… で仕様を書いていく、という。

最近、酒井さんがいろんなモデル発見器に数独を解かせてました。
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090222#p01
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090223#p01
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090302#p02
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090304#p01

僕はAlloyっていう、Z+指標みたいな言語を良く使ってます。

m-hiyamam-hiyama 2009/03/10 13:07 kosakiさん
> よかったよかった(^^)/
最良の解答です。


bonotakeさん
> 最近の形式仕様記述
解空間の要素をモデルと解釈するなら、論理型言語なら使えそう。まーもっとも、仕様記述に特化されているところに意義があるんでしょうが。

> 酒井さんがいろんなモデル発見器に数独を解かせてました。
いっぱいあるんですね。定番はないのかな、群雄割拠の状況?

bonotakebonotake 2009/03/10 18:30 >最良の解答です。
この場合、嘘つきは出題者の檜山さんってことでいいんでしょうか?(笑)

>定番はないのかな
とりあえず、モデル発見器("model finder")って言葉の言いだしっぺはAlloyで、なんで一番知名度が高いのも恐らくAlloyじゃないかなーと思います。
# 正確に言うと、Alloyは記述言語の名前で、Alloy Analyzer がモデル発見器に当たるんですが。

ただ、最近は雨後の筍みたいな感じかもしれません。

m-hiyamam-hiyama 2009/03/11 08:40 bonotakeさん、
> この場合、嘘つきは出題者の檜山さんってことでいいんでしょうか?(笑
はい、そうです。
「一人だけウソ」なるメタ言明をも懐疑して、「n人がウソをついている」ケースを網羅した上で、道義的・社会的に最も好ましい解を選択した -- さすがに富士通の小崎さんです。
> 最近は雨後の筍みたいな感じかもしれません。
それはいい傾向なのかもしれない。