ちょっと前に M-! (shell-command) を使うことが多くなってきて、もっと打ちやすいキーに移動したくてとりあえず ! にしてました。しかし exclamation mark はプログラム書いててそれなりに使うのと、それほど打ちやすくもない位置なのでもう一度変更してみ…

ピタゴラス方程式のようなものの解の数え上げ。ちょっとめんどくさそうだと思って放置していた問題。全然そんなことはありませんでした。何の工夫もない二重ループで十分。最初ピタゴラス方程式の互いに素な解を生成しながら DP かと思ったのですが、途中で…

□, ◇ の単調性 if p → q then □p → □q if p → q then ◇p → ◇q と、axiom B に相当する公理の組*1 p → ◇□p ◇□p → p から intuitionistic reasoning で distributivity law ◇(p∨q) → ◇p∨◇q が導けることに気がついたので証明をメモ。 p → □◇p from the axiom □…

GCJ registration しておきました。来月までに練習しておかないと。Round 2 以降の時間が深夜なのがちょっと面倒。

今度は A. Palmigiano の論文。概要だけ見てみたのでメモ。昨日の Hilken の論文と同じで直観主義様相論理の duality の話。ただし、こちらの論理は Hilken の考えたものよりも強くて、様相を intuitionistic first-order logic での quantifier とみなすこ…

B. P. Hilken の論文。見た*1のでメモ。 概要 二項関係の入った位相空間 (relational spaces) と、様相演算子 □, ◇ の入った frame (modal frame) *2 の間の双対性についての論文。要するに Stone duality の直観主義様相論理版を考えましょうということ。直…

とある経緯により思いついた問題。GCJ 系。与えられたアルファベットの有限集合 Σ と、Σ 上の語の集合 {w_1, ..., w_n} に対し、次の条件を満たす語の列 u_1, ..., u_n で長さの和が最小になるものを(ひとつ)求めよ。( は "u は w の部分列である" の意味) …

distributivity のない可能様相をもつ直観主義様相論理の完全性はどうやって証明するものだったかなと思って "Categorical and Kripke semantics for constructive S4 modal logic" (Alechina et al. '01) を読み返しました。 気づいたこと: completeness fo…