Welcome! | The Coq Proof Assistant
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain f
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)
いまだに Coq をよくわかってませんが，いちおう証明はできたみたいです． でも，いろいろ謎だらけです… 全然見当違いのことをしているのかもしれませんが… $ ledit coqtop Welcome to Coq 8.0pl3 (Jan 2006) Coq P. DN is assumed (* 排中律 EM を証明 *) Coq P ============================ P \/ ~ P EM P ============================ ~ ~ (P \/ ~ P) EM P H : ~ (P \/ ~ P) ============================ False EM P H : ~ (P \/ ~ P) ============================ P \/ ~ P EM P H : ~ (P \/ ~ P) ====
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (9) 排中律の証明
さかい さんからトラックバックをいただきました． ヒビルテ 2006-04-29 [Haskell] [quiz] (forall x. ((x->r)->r)->x) -> Either a (a->r) 問題の関数はこんな感じで定義できる。 notNotEM :: ((Either a (a->r)) -> r) -> r notNotEM k = k (Right (\a -> k (Left a))) dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r) dn2EM dn = dn notNotEM で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (10) 二重否定に関する小ネタ
直観主義というのは，「数学的対象は完結した存在 (神，イデア) ではなく，人間の心によって構成されていくものだ」 という思想です． π は π として最初から存在しているわけではなく，1 ステップずつ計算されて，徐々に形作られているものだよー，だから排中律なんてナンセンスだよーと． ブラウワ : 「本当，排中律とか無限 (極限) ってキモい．こんな，実際に作ることができないものを認めているから，数学は不確実になってしまうんだよー」 ヒルベルト : 「あんた馬鹿ぁ ? 数学者から排中律を奪うのは，天文学者から望遠鏡を，ボクサーから拳を奪うようなものだよー．よし，こうなったら，有限の立場でちゃんと数学の正しさを証明したる !」 という，数学の基礎をめぐる論争が，やがては不完全性定理へとつながり，チューリングマシンへとつながり，現在のコンピュータへとつながるわけですね．ドラマティック． 前回触れ
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (8) 一休み
現在，管理人は多忙と体調不良のため，あまり頭が回りません… もともとそんなに回りませんが． # 多忙と言っても，単に本人が無能で無駄に時間がかかっているというだけのことです．世間にはもっともっと大変な人達がたくさんいます．本当にもうしわけないです． 今回は，Coq に関係があるエッセイなどをいくつか紹介します． 萩谷先生のエッセイは，非常に面白くてオススメです．いつか私も，このような軽妙で優れた文章を書けるようになりたいものです． 機械による数学の型式化には，ドメインを限定して完全な自動証明を目指す定理証明系 (後述する B-M prover はこっち) と，体系は汎用的にしておいて，人間の手を借りる定理証明支援系 (Coq や Agda や HOL はこっち) があるそうです． ここらへんは， 形式化願望 論理と推論 --- 数学の形式化 ただ，人間の手を借りる以上は，やはりインタフェー
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (7) 古典論理
突然ですけど，古典論理 (排中律) ってうさんくさく感じませんか ? 一見 P ∨ ¬ P は，どう考えても自明に思えますが，本当にそう言い切ってしまって大丈夫なのでしょうか ? 一般的に，「古典」と名がつくものは，ある程度成熟して一般的になり，共通のコンセンサスが取れているもの，というような意味合いで使われます． # 「時代遅れ」とか「古くて適切ではない」，というニュアンスとは全く異なります． それらは非常に美しく理想化されており，普遍的なものであるからこそ，「古典」と呼ばれ，いつの時代も重要であり続けるのです． 例えば，バッハの音楽や中国の漢詩，宮本武蔵の五輪の書などは，立派な古典ですね． もちろん，これらは，そのまま現代の状況に応用できるわけではありませんが，その「コア」の部分は，時代に合わせて形を変え，脈脈と語り継がれて行くわけです． # 人間はそう変わるものではないので，5000
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (5) 自然演繹法 II
前回は自然演繹法についてちょっと書いただけで終ってしまったのですが，今回はちゃんと Coq を使います (笑) とりあえず，Coq のコマンドと，自然演繹法の推論規則の対応を押さえておきましょう． → 導入 intro H. → 除去 generalize (H1 H2); intro H3. ∧ 導入 split ∧ 除去 elim H; intros H1 H2. ∨ 導入の左側 left. ∨ 導入の右側 right. ∨ 除去 elim H; [intro H1 | intro H2]. ¬ 導入 intro H. ¬ 除去 absurd A; try assumption. とか contradiction. らしい．まだよくわかりません． 後ろ向き推論 apply とりあえず，対応表にそって，テキトーに証明を行ってみましょう． 例題は，チュートリアルの通りに，A ∧ B → B
えぷりくす
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 「鈴木亜美で妻子３人殺害」に見えた。 処方されたリタリンを試してみた。さすが「合法覚醒剤」の別名を持つだけあって、他の薬が
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (4) 自然演繹法
前回までは，何の説明も無く，いきなり intro や apply を使って，非常に初歩的な命題論理の証明を行ってみました． # ちなみに，本職の Logician の方々が見たら噴飯モノの，訳語とか概念に関する間違いや誤解，曖昧さがゴロゴロしていると思いますが，あんまり修正とか見直しとかはしないで，とりあえずどんどん進んでいこうかと思います．その過程で段々理解が進んできて，誤解も訂正されていくと思うので．必要以上に過去は振り返らないで，未来だけを見つめて行きましょう ! (耳障りが良い常套句 ｗ) # とはいえもちろん，ツッコミやコメントは大歓迎です (⌒▽⌒) けっこういろいろやったので，復習としてコマンドをメモしておきます． Quit. Coq の終了． Check 識別子. 識別子の型を調べる． Section Declaration. 宣言セクションに入る． Variable va
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (3) Minimal Logic
今回は，最も基本的な組み込みの最小論理 (Minimal Logic) 推論エンジンの，ほんのさわりだけを見ていきます． 使用するのは，いわゆる三段論法ってやつです (厳密にいうと，この用語はけっこう曖昧なので，あんまり使わないほうが良いのですが…)．A と A → B が成り立つならば，B が成り立つという，アレです．うむ，常識ですな (笑) # でも，型理論の論文とかで， A A → B -------- B とか書いていると，べつにどおってことないことなのに，何だかびびってしまいませんか ? (笑) まぁ，あたりまえのことを，あたりまえにやっていくのが，論理学ですからね．そして気がつくと，当たり前のことをずっとやってきたはずなのに，とんでもない結論が出てくると w これが論理学の醍醐味です．基本は大事なんですよ． というわけで，まずは Coq を立ち上げ，セクションを切り替えておきま
ホワット・ア・ワンダフル・ワールド Ｔｈｅ Ｃｏｑ Ｐｒｏｏｆ Ａｓｓｉｓｔａｎｔ Ａ Ｔｕｔｏｒｉａｌ (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
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明
前回までは，命題論理における自明なトートロジーをいくつか，手動で証明してみました． しばらく定理証明系を触っていると，構成的数学における証明 ※ とプログラミングは，本質的に区別がつかない (極論すれば，同じモノ) ということがよくわかってくると思います． ※ 何かが成り立つということを，弁証ではなく，実際に作って見せることによって証明を行う数学の流派． 定理は，同じことを何度も書かないですませ，証明を短くし，見通しを良くするための「サブルーチン」，あるいは，いくつかの公理を組み合わせ，より高級な命令を作るための 「マクロ」 ですし，公理や規則はまんま「機械語」です． 流派によって公理系 (公理の集合) が違うのは，CPU の命令セットの違いに例えることができますし，どの高級言語が優れているかという論争は，まんま論理体系の優劣論争 ※1 です w ※1 ほとんど全ての論理体系が扱える範囲自
自動定理証明 - Wikipedia
アルゴンヌ国立研究所は1960年代以降2000年代まで、自動定理証明のリーダーだった。 自動定理証明（英: automated theorem proving, ATP）とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。 歴史[編集] 論理学的背景[編集] 論理学の起源はアリストテレスまで遡るが、現代的数理論理学は19世紀末から20世紀初頭に発展した。フレーゲの『概念記法』(1879) が完全な命題論理と一階述語論理の基本的なものを導入[1]。同じくフレーゲの『算術の基礎』(1884)[2]でも、形式論理の数学（の一部）を説明している。この流れを受け継いだのがラッセルとホワイトヘッドの『プリンキピア・マテマティカ』で
Haar状特徴に基づくブースト分類器のカスケードを利用する高速物体検知
Haar状特徴に基づくブースト分類器のカスケードを利用する高速物体検知 Rapid Object Detection With A Cascade of Boosted Classifiers Based on Haar-like Features はじめに このドキュメントでは高速物体検知のためのブースト分類器のカスケード の訓練と使いかたについて説明します． 過完備Haar状特徴の集合は，シンプルな個体分類器のための基底を提供します． 対象物検知の例としては，顔，目および鼻の検知やロゴ検知などがあります． ロゴ検知には，対象物のサンプル画像を注意深く多数収集する必要がないため， このドキュメントでロゴ検知を物体検知の例として取り上げ，説明します． ここでは，サンプル画像を注意深く多数収集する代わりに，1つの原画像から 対象物の多数のサンプル画像を生成するユーティ
はてなブログ | 無料ブログを作成しよう
うまくいかない日に仕込むラペ 「あぁ、今日のわたしダメダメだ…」 そういう日は何かで取り返したくなる。長々と夜更かしして本を読んだり、刺繍をしたり…日中の自分のミスを取り戻すが如く、意味のあることをしたくなるのです。 うまくいかなかった日のわたしの最近のリベンジ方法。美味しいラペを…
OpenCVを使って画像の物体認識をするPerlモジュール作った - spiritlooseのはてなダイアリー
作った。 http://search.cpan.org/dist/Image-ObjectDetect/ http://d.hatena.ne.jp/darashi/20070223/1172232765でRubyの拡張ライブラリを公開されていたので、こりゃやらなくちゃ・・・と思った次第です。すみません。 こんな感じで使えます。Imagerで顔を囲んでみた。 #!/usr/local/bin/perl use strict; use warnings; use Imager; use Image::ObjectDetect; my $file = 'picture.jpg'; my $image = Imager->new->read(file => $file); my $cascade = '/usr/local/share/opencv/haarcascades/haarcascad
【コラム】OS X ハッキング! 第203回 OpenCV iSightで顔を認識? (MYCOMジャーナル)
Core 2 Duo搭載の二代目MacBookが発売になりました。初代が5月16日発売ですから、ほぼ半年ぶりのモデルチェンジです。ユーザとしては、半年で25%のスピードアップは微妙に悔しくもありますが……機会があれば、ユーザならではの視点で二代目を検証してみたいと思います。 さて、今回は「OpenCV」について。既報のとおり、画像の変形や認識などイメージング処理を目的としたクロスプラットフォーム指向のライブラリだが、OS Xユーザ要注目の機能もいくつか備えている。活用次第では、いろいろな力を発揮しそうなのだ。 OpenCVの特徴、そして導入の下準備 OpenCVの開発はクロスプラットフォーム指向で行われ、特定のハードウェアに依存しない。Intelが関与しているプロジェクトなだけに、メインターゲットはやはり"Wintel"ということになるが、POSIX互換機能を備えるUNIX系OSでも動作す
OpenCV@Chihara-Lab.
Link: 掲示板(32d) 適応的二値化処理(123d) Visual C++ 2008 Express Edition(302d) 射影変換(305d) RGBTRIPLE(366d) リンク(381d) GML C++ Camera Calibration Toolbox(558d) 高度なGUI(558d) 基本形(558d) 行列の出力(558d) Python(558d) カメラキャリブレーション(558d) PukiWiki/1.4/Manual/Plugin/L-N(558d) PukiWiki/1.4/Manual/Plugin/O-R(558d) ボールトラッキング(558d) SharperCV関数リファレンス(558d) 主成分分析(558d) カメラ利用の基本形(558d) マウス入力(558d) キャプチャ＆動画ファイル出力(558d) 画像の2値化処理(558
今すぐ自分に自信を取り戻すための7つのTips | P O P * P O P
読むとなんだか元気がでてくる記事がありました。 「すぐに自信を取り戻すための7つのTips」という記事です。人間誰しも落ち込む時はあります。そのような時のために自分をちょっと元気付けてくれるTipsはいくつか知っておきたいものです。 » 7 Helpful Tips To Immediately Increase Your Confidence 一体、どうすれば自信はつくのでしょうか。下記よりどうぞ。 「もし最悪の事態になったらどうしよう・・・」。そのように人間は起こっていない問題をついつい心配してしまいます。しかし、人間のエネルギーは一定です。心配事にエネルギーを無駄使いするくらいならば、もっと生産的なことにエネルギーを使いましょう。 何か初めてのことに取り組む時には「それは過去にすでにやった」と想像してみましょう。そして、目をつぶって、「これから取り込むことをうまくやっている」シーンを
(ogijunの)あとで書く日記 - あなたがMacを使うべき10の理由
前口上 もともとこのエントリを書こうと思い立ったのはETech会場はMacだらけ、というid:naoyaさんや他の参加者の報告に刺激されたからだったりするんだけど、中でid:iRSSさんが次のように書いている: 「どうして、この会場はMacユーザーが多いんですか？」と質問したら 「Unixが使えるポータブルだからだよ。」とのお答え。 これは確かにその通りで、とても簡潔な表現なんだけど真実を伝えてはいる。ただ、あまりに簡潔すぎるというかなんというか。まあ誤解はないとは思うけど、Unixであることは別にそれ自体が目的になってしまうわけはないのであって、だから一部のgeekはUnixさわってるだけでしあわせだから、そこの狭いマーケットにうまくはまっただけ、というわけではぜんぜんない。だから市場的なインパクトはないだろうという予想は当を得ていないと私は思う。本当はUnixであることを手段として、そ
あなたがMacを買わない10の理由 - はてダ保管所 by ogijun
また前口上 去年書いた『あなたがMacを使うべき10の理由』を書いたら、おおむね好評とともに読んでもらえたみたいで(ほんとかー?)うれしい限り。実際あのあとも記事の影響ってわけじゃないと思うけど*1Mac買ってくれた人もたくさんいるし、ますます広まってきているみたいでこれも私設営業の人としてはとてもうれしい。 Macを買うべき理由はあのときからそんなに大きく変わっていないんだけど、あのあと一部の人からは「Macは買わない」とか言われてて、そんな人たちに「なんで? なんで?」って聞いてみてたらそういう人たちの言い分にはいくつか類型があることがわかってきた。そしてそういった「買わない理由」の中には私から見ると解決可能なものも含まれているわけ。 もし些細なことが原因でその人がMacを使えないとしたら、それはその人にとってとても不幸なことだと思う(←とか決めつけるのを妄想といいます)。ゆめゆめゆゆ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
caramel*vanilla » Blog Archive » WordPressでLightboxを超簡単に使ってみる
わかりやすい404エラーページについて考えてみる | caramel*vanilla
「Gmail」日本語版、外部のPOPメールアカウントを受信できる機能追加