[Coq] Epistemic Logic

先日のFormal Methods Forum勉強会で話した話。

Epistemic Logicというのは「誰々は◯◯を知っている」「誰々は◯◯を知っていることは常識である」みたいな知識に関する事柄を扱う論理です。通常の命題 $P$ に対して、「$\alpha$は$P$を知っている」を表す $K_{\alpha} P$ や、「$P$は皆の常識である」を表す$C P$といった様相記号 $K_{\alpha}$ や  $C$ を用いた様相論理になります --- ということは、"Metareasoning for multi-agent epistemic logics" という論文 (PDF) に載っています。

酒井さんのヒビルテの「Alloyで知識論理を使って論理パズルを解く」という記事に載っている問題が上記の論文にも載っていて、その論文に従い Coq で定式化してみました。

Coq のコードは github の https://github.com/tmiya/coq/blob/master/epistemic/modal.v に上げてあります。

大雑把な解説をすると、論文に載っていた epistemic logic の公理系を Coq で下記の様に記述します。

Inductive theorem : (Ensemble prop) -> prop -> Prop :=
| intro_and : forall G p q, (G |-- p) -> (G |-- q) -> (G |-- (p && q))
| elim_and_l : forall G p q, (G |-- (p && q)) -> (G |-- p)
| elim_and_r : forall G p q, (G |-- (p && q)) -> (G |-- q)
| intro_or_l : forall G p q, (G |-- p) -> (G |-- (p || q))
| intro_or_r : forall G p q, (G |-- q) -> (G |-- (p || q))
| elim_or : forall G p1 p2 q, 
   (G |-- (p1 || p2)) -> ((p1::G) |-- q) -> ((p2::G) |-- q) -> (G |-- q)
| intro_imp : forall G p q, ((p::G) |-- q) -> (G |-- (p --> q))
| elim_imp : forall G p q, (G |-- (p --> q)) -> (G |-- p) -> (G |-- q)
| elim_not : forall G p, (G |-- !(!p)) -> (G |-- p)
| intro_not : forall G p, ((p::G) |-- F) -> (G |-- !p)
| reflex : forall G p, (p::G) |-- p
| dilution : forall G G' p, (G |-- p) -> ((G _+_ G') |-- p)
| intro_false : forall G p, (G |-- (p && (!p))) -> (G |-- F)
| intro_true : forall G, G |-- T
| rule_K : forall G a p q, G |-- ((K a (p --> q)) --> (K a p --> K a q))
| rule_T : forall G a p, G |-- (K a p --> p)
| intro_C : forall G p, (O |-- p) -> (G |-- (C p))
| elim_C : forall G a p, G |-- (C p --> K a p)
| rule_C_K : forall G p q, G |-- ((C (p --> q)) --> (C p --> C q))
| rule_R : forall G a p, G |-- (C p --> C (K a p))
where "G |-- p" := (theorem G p).

これを使って今回示したい定理は、

(* A1 may wear red hat (=M1) or white hat (= !M1).
   A2 may wear red hat (=M2) or white hat (= !M2). *) 
Parameter A1 A2: agent.
Parameter M1 M2: prop.
(* S1 = A1 that said "I do not know whether I wears a red hat".
        Therefore, prop "A1 does not know M1", 
        is commom knowledge. *)
Definition S1 := C (!(K A1 M1)).
(* S2 = Because the king said "At least one of A1 and A2
        wears the red hat". Therefore "M1 or M2" is
        common knowledge. *)
Definition S2 := C(M2 || M1).
(* S3 = Because A1 can see the A2's hat, A1 would know
        !M2 if !M2 stood, and this is common knowledge. *)
Definition S3 := C(!M2 --> K A1 (!M2)). 
(* After A1 said "I do not know whether I wears a red hat",
   using the common knowledge {S1, S2, S3}, it becomes the
   common knowledge that A2 wears the red hat. *) 
Theorem two_wise_men : S1::S2::S3::O |-- C M2.

を証明する、ということになります。
証明に際しては、この証明の導出に関する幾つかの tactic を定義するなどを多少工夫してみました。

残念ながら勉強会当日には間に合わなかったけど、ようやく証明出来ました。