定理証明リンク集
定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type
Write Yourself a Theorem Prover in 48 Hours (その1) - Qiita
この記事は定理証明アドベントカレンダー2013のたぶん7日目の記事です 誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。 タイトルの元ネタは http://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours です。というわけで、使う言語はHaskellですが、他の言語でも特に問題ないと思います。 定理証明器の部品は以下のものが必要です。 記述言語 カーネル 証明支援言語 その他 記述言語はCoqではGallinaといわれてる部分です。立派なプログラミング言語をひとつ設計しないといけません。このプログラミング言語によって、定理のステートメントを記述したり、証明を記述したり、関数を書いたり、データ構造を定義したりします。 カーネルは記述言語のインタープリタになります
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
