2007-12-02 [長年日記]
λ. 計画停電
今日(12/2)はSFCで計画停電があるため、この日記も止まる予定。それから、それにあわせてこのサーバーのリプレースも行うそうなので、環境が変わって動かなったりとかもあるかも。
【2007-12-08追記】 今回の移行で、Linux/x86からLinux/x86_64になったのだけど、GDBMのフォーマットはアーキテクチャ依存なのを忘れていて、w3mlとRuBBSが動かなくなっていた。 以前、WebサーバがSolaris/sparcからLinux/x86になったときにも嵌ったのに、同じ事で二度失敗するとは……
λ. シャガール展
生誕120年記念 色彩のファンタジー シャガール展 −写真家イジスの撮ったシャガール− というのをやっていたので、見に行ってみた。 「受付にて『シャガール〜大柴！』とくっきりはっきりいった方は100円割り引きます」とのことなので、ちょっと恥ずかしかったけど言ってみた。もっともルー大柴という人のことは良く知らないのだけど。
λ. 石焼ホットックと黒蜜きな粉アイス
土古里(도고리)というところでお昼を食べて、デザートに「石焼ホットックと黒蜜きな粉アイス」というのを食べた。 「ホットック」って何かと思ったら、お米から作ったお菓子らしい。英語では「Korean Ricecake and Brown Sugar Soybean Flour Icecream in Hot Pebbles」という説明で、韓国語では「돌솥 호떡 콩가루 아이스크림」と説明されていた。韓国語でもアイスクリームは「アイスクリーム」なのね。
![[石焼ホットックと黒蜜きな粉アイス]](./images/20071202_0.jpg)
λ. “A simple propositional S5 tableau system” by Melvin Fitting
- <URL:http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/SimpleSfive.pdf>
- <URL:http://www.ingentaconnect.com/content/els/01680072/1999/00000096/00000001/art00034>
を読んだ。
S5のシーケント計算はcut-admissibleではない(cf. 様相論理のシーケント計算)から、タブローもややこしいのではないかと思い込んでいたが、想像していたよりもずっと簡単なんだな。しかも、TやS4の決定問題がPSPACEなのに対して、S5の決定問題は高々NP完全で済むそうだ。これは、TやS4では(様相を剥がす時の)ブランチの破壊的な変更の順序に意味があったが、S5ではどの順序で行っても結果が同じため。
それから、健全性を示すための議論で、全ての世界の間に到達可能性関係が成り立つような構造だけを考えているのが、ちょっと目から鱗だった。S5の通常の構造では到達可能性関係は任意の同値関係なのだけど、ここでの扱いはこの通常の構造における同値類を取り出してきて一つの構造として扱っていると考えられる。妥当性を考える場合には、任意の構造を考えるので、こうしても実は結果は同じ。
ちなみに、何故これを読んだかというと、例によって知識論理を使って論理パズルを解くため。 先日のSPASSで知識の論理を使って論理パズルを解く?では定理証明機SPASSを使ってみたが、S5は決定可能なはずなのに、正しくない結論を与えたときに止まらなくなってしまうようで、どうもよろしくない。 それならば、S5の決定手続きを調べてみよう、という事で読んだのだった。 実際に論理パズルを解くために使うのはまた今度挑戦してみる予定。
【2007-12-04追記】 あれれ!? この場合のタブローってシーケント計算とほぼ同じで、しかもカットに対応するようなものは入っていないように見えるんだよな。シーケント計算がcut-admissibleでないのに対して、これが完全なのは、一体何が原因?
【2007-12-06追記】 Deep Inference and the Calculus of Structures - Modal Logic 見つけた A Deep Inference System for the Modal Logic S5 という論文には以下のように書いてあったのだが、具体的に何が問題なのか良くわからない……
The failure of the sequent calculus to accommodate cut-admissible systems for the important modal logic S5 (e.g. in Ohnishi and Matsumoto [21]) has led to the development of a variety of new systems and calculi. A partial solution to this problem has been presented in Shvarts [25] and Fitting [5], where theorems of S5 are embedded into theorems of cut-free systems for K45. These systems provide proof search procedures for S5, they are, however, systems of a weaker logic.
