LaTeXによる証明図の記述 - kivantium活動日記
証明図は「bussproof.sty」にお任せを参考にいくつか証明図を書いてみました。ひな形はこんな感じです。 \documentclass{jsarticle} \pagestyle{empty} \usepackage{bussproofs} \begin{document} \begin{prooftree} %ここに証明図を書く \end{prooftree} \end{document} 以下は省略してprooftree環境の中だけ書きます。 まずは簡単なものから \AxiomC{$(\Phi \land \Psi)$} \UnaryInfC{$\Phi$} \AxiomCには公理や前提となる命題を記述します。 \UnaryInfCには単一の命題からの帰結を記述します。 \AxiomC{$\Phi$} \AxiomC{$\Psi$} \BinaryInfC{$\Phi \land
有限集合とは何だろう（ストーリー付き練習問題集） - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Xは有限集合である」とか「Xは有限集合でない」とかの表現はよく出てきますが、この有限性ってのはいったい何なんでしょう？ 少しマジメに考えてみることにします。これといった予備知識を要求しませんが、マジメに考える態度は必要です。 実は、有限性を調べるのは目的じゃなくて手段です。証明の“お膳立て”シリーズとか、自然演繹ダメじゃんシリーズ（って、そんなシリーズねえけど、「存在記号の除去規則について考える」とか）に対して、例題を提供するのが、この記事の主たる目的です。この記事を読みながら、ハッキリとは書いてない証明を全部書いていくことが練習問題になります。内容的には超カンタン（当たり前）なので、明示的な証明は逆にハードです。 内容： 自然数についてよく知っているとする 論理記号など 有限性の定義 個数勘定の原理 個数勘定の補題と鳩の巣原理 個数勘定の補題と数学的帰納法 もう少し数学的帰納法のための
Mathematical proof - Wikipedia
P. Oxy. 29, one of the oldest surviving fragments of Euclid's Elements, a textbook used for millennia to teach proof-writing techniques. The diagram accompanies Book II, Proposition 5.[1] A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, suc
Haskell+GADTで定理証明 その1: 型レベル自然数の等価性 - keigoiの日記
実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないことになっているらしい。やっぱりHaskellを使うものとして型安全性くらいは保証したい。でも、かといって普通のHaskellではうまく型を付けられない。(Typeableクラスのキャストを使っても解決にはならない。) そこで、魔法のGADT。 この型とこの型はぜったい等しいのにーというのが文脈から明らかなとき、それを表現できるのがGADTだ…というのが私の理解。まさしく私のケースにぴったりだ。これを使えばunsafeCoerceなんか要らんかもしれない。 いいかえれば、いわゆる定理証明をGADTつきのHaske
推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─ - λx. x K S K ＠はてな
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です． 元々このネタは， 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです． このため，ここで紹介するプログラムや証明は， タクティクの種類やライブラリの利用が必要最低限に絞られているので， もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため，敢えて auto も使いませんでした)． Coq 上級者には冗長な証明が気になるかもしれませんが，その点は予めご了承ください． はじめに 比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ， クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソー
定理証明系 Haskell
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
)
Lagrange's Theorem (Group Theory) - ProofWiki