ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (4) 自然演繹法
前回までは，何の説明も無く，いきなり intro や apply を使って，非常に初歩的な命題論理の証明を行ってみました． # ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ) # とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒) けっこういろいろやったので，復習としてコマンドをメモしておきます． Quit. Coq の終了． Check 識別子. 識別子の型を調べる． Section Declaration. 宣言セクションに入る． Variable va
ホワット・ア・ワンダフル・ワールド Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ Ａ Ｔｕｔｏｒｉａｌ (2) 定義
前回の続きです． 今回は，定義についてです． coq-interface の初期化の際に読みこまれるプレリュードは，いくつか数学的定義を含んでいます． 例えば，前回扱った nat は，数学的概念 (mathematical collection) (Set 型) として定義されています．また，定数 O (オー) や S，plus なども，それぞれ nat，nat -> nat，nat -> nat -> nat という型のオブジェクトとして定義が用意されています． では，O と S を用いて，自然数を定義してみましょう．ここでは，一番最初の自然数 O と，次の自然数を求める関数 S の存在を前堤とします． 1 は，どのように定義すれば良いでしょう ? そうです，1 は O の次の数ですね． $ coq-interface Welcome to Coq 8.0pl3 (Jan 2006) C
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (1) 宣言
The Coq Proof Assistant A Tutorial を参考にしつつ，Coq について勉強していこうと思っています． まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください． Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです． 対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと． このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと． とりあえず，C:\
ホワット・ア・ワンダフル・ワールド Proof Assistant Coq
The Coq proof assistant を，とりあえず apt-get でインストール (coq，coq-libs，coqide) してみようと思ったら，debian パッケージが壊れているっぽくて，インストールできませんでした (stable/testing/unstable いずれも)．残念．そのうち直ると思うので，しばらく様子を見てみます(軟弱者)． ちなみに Coq ってのは，Agda や Isabelle/HOL と同じような，定理証明支援系のこと．Calculus of Inductive Construction とかいう，あまり聞きなじみが無い論理体系をベースにしているそうな． # これについては，Interactive Theorem Proving And Program Development: Coq'art: The Calculus Of Inducti
えぷりくす
http://portal.acm.org/citation.cfm?id=1040305.1040313 今年のPOPLにこんなのがあったそうで、まさしく今 quantitative な analysis をテーマにしてる身としてはちょっと読んでみようかなと思ったり。 それはそうとすみいさんもほそやさんも POPL 通ってて自分はさっぱりうだつがあがらんなあとちょっとがっくり http://www.excite.co.jp/News/odd/00081108087433.html ジョーンズさんの友人の手元に渡るまでの経緯が激しく気になる http://www.nikkansports.com/ns/general/f-so-tp0-050111-0019.html 「鈴木亜美で妻子３人殺害」に見えた。 処方されたリタリンを試してみた。さすが「合法覚醒剤」の別名を持つだけあって、他の薬が
にわとり小屋でのプログラミング
この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
