ipc_botの紹介
この記事はTheorem Prover Advent Calendarの22日めの担当記事です.
今年の僕の持ちネタの一つですが,ipc_bot というTwitter botを作りました.
このbotは直観主義命題論理の命題を投げると解いてくれるbotです.
仕組み
証明を探すのは適当にやっても出来るのですが,証明が存在しないことを確認するのは結構大変です.
(古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが,直観主義論理命題論理だとそう簡単ではありません)
証明が存在するかどうかを有限時間内で判定するには,推論規則を色々いじる必要があります.しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい. http://www.tsg.ne.jp/buho/305/buho305.pdf [PDF]
その他の応用例
Coqのtautoがこのような決定アルゴリズムを使っているようです.
試しにそこそこ複雑な命題を投げても,きちんと答えを返してくれます.
Goal forall P Q R S:Prop, ~~((P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S)). Proof. tauto. Qed. Goal forall P Q R S:Prop, (P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S). Proof. try tauto. (* fail *) Abort.
形式的証明
かつて形式的証明を書いたことがあります.
- スライド: http://www.slideshare.net/qnighy/proving-decidability-of-intuitionistic-propositional-calculus-on-coq
- ソースコード: https://github.com/qnighy/IPC-Coq
また,Coqのcontribにも検証済みの証明探索アルゴリズムがあります.こちらについては未確認ですが,OCamlへの抽出もできるようになっており,かなりよく出来ていることが推察されます.
まとめ
随分と雑な記事になってしまってすみません.来年は精進します.
お詫びに,おもちゃの定理証明器に線形型を加えたものへのリンクを貼っておきます.
まだ型検査器しか作ってないですが一応定理証明器と言えると思います.ですが,おもちゃの定理証明器についてはkikxさんが既に記事にしていたようなのであまり書くことがありませんでした.
以上です.