存在記号の除去規則について考える - 檜山正幸のキマイラ飼育記 (はてなBlog)
「全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。 存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業（記法のあいだの翻訳）に慣れて、その“どうでもよさ”（記法が変わっても内実は変わらないこと）を感じていただければ幸いです。 内容： 存在記号の除去規則 限量随伴性 引き戻しと存在限量子の随伴性 随伴性を証明に利用する 随伴性からサイド証明へ メタ循環構造 存在記号の除去規則 標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。 P(a) : : ∃x.P Q -------------[∃除去] Q僕は、自然演繹に愚痴を言い、悪態をついてます（「自然演繹はちっとも自然じゃない -- 圏論による
Globularの威力をお見せしよう - 檜山正幸のキマイラ飼育記 (はてなBlog)
Globularはとっつきにくいソフトウェアなので、使い方を伝えるには、最初から順番に説明する必要があるでしょう。しかし、タクサンの画面キャプチャを撮ってマウス操作の説明を付けていく気力は湧きません（大変過ぎる！）。とりあえず、Globularのデモンストレーションとして、“それなりの内容の定理”を証明したサンプルをお見せします。誰でもアクセス可能なので体験して悟ってください(苦笑)。 http://globular.science/1601.004v2 （Chrome推奨） 「証明の過程を追体験する」の節だけは、頑張って手取り足取りな解説を書いたので、そのとおりに操作してみると雰囲気が伝わるでしょう。 このサンプルの内容はというと： 「絵算の威力をお見せしよう」において、ラルフ・ヒンズ（Ralf Hinze）の論文にある命題を2つ選んで絵に描きました。選んだ2つの命題は、論文の入り口にあ
絵算ベースの証明支援系 Globular - 檜山正幸のキマイラ飼育記 (はてなBlog)
絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。 http://globular.science/ ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。 証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。100%グラフィカルで、テキストによる表現や命令は一切使いません。パッと見ただけでは、何をするものか見当が付かないのではないでしょうか。 このソフトウェアを開発したのは、アブラムスキーとクック（この記事に二人の写真あり）が率いるオックスフォードのQuantum Groupで、開発の中心人物はジェイミー・ヴィカリー（Jamie Vicary）です。 Quantum Groupは、数年前から同種のソフトウェア（diagrammatic proof assistant）としてQuantomaticも提
Category Theory in Coq
This is a quick page I've thrown together for my Coq library formalizing basic category theory. The development follows Steve Awodey's book on category theory; the files are named after chapters and subchapters of that book for easy reference. Getting It The gitweb is here. You might also want to look at the README Design Decisions One of the difficulties with putting together a formalization of c
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
bitbucketの使い方
