An Investigation of the Laws of Thought by George Boole
Read now or download (free!) Choose how to read this book Url Size
オンラインで入手できる数理論理学・数学基礎論のテキスト
オンラインで入手できる数理論理学・数学基礎論のテキスト 数理論理学、数学基礎論の教科書的に使えるテキスト（講義ノート、サーヴェイ、モノグラフ等）のうち、オンラインで入手できるものを集めました。 入門的概説 論理一般 高階論理と型理論 直観主義論理 コンビネータとラムダ計算 時相論理および時制論理 様相論理 適切さの論理 自然言語の論理 空間論理 モデル理論 安定性理論 無限論理 計算可能性理論および再帰理論 集合論 pcf理論 記述集合論 実数の集合論 選択公理 強制法と内部モデル 連続体仮説 NF 証明論と構成的数学 順序数解析 算術の体系と不完全性 証明可能性論理 線形論理 構成的数学 代数的論理と圏論 ブール代数 普遍代数 量子論理 圏論 歴史 入門的概説 [▲] 加茂静夫，「数理論理学（命題論理と述語論理）」．[PDF] 嘉田勝，「数理論理学 講義ノート（2013年度版）」． St
論理とカリー・ハワード対応について書いたこと一覧とメモ - 再帰の反復blog
「直観主義論理の「自然さ」(1) 自然演繹」 直観主義論理の自然演繹では導入則と除去則とが相補的な関係になっている。 「直観主義論理の「自然さ」(2) シーケント計算 」 直観主義論理の自然演繹体系を変形すると直観主義のシーケント計算の体系が得られる。 「直観主義論理の「自然さ」(3)古典論理のシーケント計算と自然演繹」 直観主義論理の演繹体系に規則を追加して結論に複数の論理式を置けるようにすると古典論理の体系になる。 「直観主義論理のカリー・ハワード対応」 直観主義論理の自然演繹と型付きラムダ計算との対応関係の説明。 「call/ccと古典論理のカリー・ハワード対応」 ラベル付きブロック構文とcall/ccの説明。型付きラムダ計算にcall/ccを追加したものは、直観主義論理+(¬A→A)→A = 古典論理に対応する。 「古典論理のカリー・ハワード対応のためのラムダ計算」 λμ計算(の変
CS 6110 Spring 2013
Overview Programming languages are a fundamental part of computer science. This course introduces the formal tools needed to describe precisely what a program means. These tools help us answer many useful questions about program analyses and transformations, such as: Is this program correct? Will this program encounter a run-time type error? Is one program indistinguishable from another? Is this o
公理図式 - Wikipedia
公理図式（英：axiom schema、英複数形：axiom schemata）とは、数理論理学における用語で、公理を一般化した概念である。公理型とも訳される。 公理図式とは、ある一群の（多くの場合には無限個の）類似の「形式」（schema）を持った公理を、メタ変数を含む単一の論理式で表現したものをいう。より正確にいえば、項を表すメタ変数記号と、論理式を表すメタ変数記号とを含むような拡大言語を考えたときに、その拡大言語に於ける論理式として記述された公理が公理図式である。メタ変数記号に代入される項や論理式に何かしらの条件（自由変数の出現に関する条件等）を付ける場合もある。具体的な公理はそれらのメタ変数に項や論理式を代入することによって得られる。 メタ変数に代入されうる部分論理式や項が可算無限通りあるとすれば、その公理図式は可算無限個の公理の集合を表すことになる。この集合は、メタ変数に代入され
Peirce's Law Equivalent to Law of Excluded Middle - ProofWiki
Theorem Peirce's Law: $\left({p \implies q}\right) \implies p \vdash p$ is logically equivalent to the Law of Excluded Middle: $\vdash p \lor \neg p$ That is, Peirce's Law holds if and only if the Law of Excluded Middle holds. Law of Excluded Middle implies Peirce's Law Let the truth of the Law of Excluded Middle be assumed. Then: $\left({p \lor \neg p}\right) \vdash \left({\left({p \implies q}\ri
Haskell/カリー=ハワード同型 - Wikibooks
カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。 導入[編集] これよりカリー=ハワード同型は単に C-H と表記する。C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということだ。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では error や undefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCo
ビジービーバー - Wikipedia
ビジービーバー（英：busy beaver）とは、計算可能性理論で扱われるある種のチューリングマシンである。この名称は「仕事人間」を意味する英語の慣用句に由来する。ビジービーバーは空のテープから処理を開始し、可能な限り走り続けるが、最終的には停止する。これは停止するチューリングマシンのクラスが消費し得る時間と領域（テープ）の長さの上限を与える。 ビジービーバー関数はこの上限を数値化するものであり、計算不能関数の一例でもある。この関数はいかなる計算可能関数よりも急速に増大するということを証明できる。ビジービーバー関数の概念は、ティボール・ラドー（英語版）による1962年の論文 "On Non-Computable Functions" の中で、「ビジービーバー・ゲーム」という名称で初めて導入された。 ティボール・ラドーは、1962年の論文で以下のように「ビジービーバー・ゲーム」を導入した。
@syamino はてなダイアリー
ラムダ計算でEither Either型の値をパターンマッチする状況を考えます。 「データコンストラクタのパターンマッチ」は，下図のようにしてラムダ計算で表現できます。 ラムダ計算でBool 今度は，Bool型の値をパターンマッチする状況を考えます。 TrueやFalseには引数が無いので，(3)や(4)はλで囲みません。 パターンマッチ = 「データコンストラクタを他の関数に置き換えること」 パターンマッチによって，Leftがlに置き換わります。以下同様です。 「データコンストラクタを置き換える」という概念について，もう少し詳しく考えていきます。 データコンストラクタの置き換え方は2種類ある リストのような再帰的なデータ型では，データコンストラクタの置き換え方が2種類あります。 data List a = Cons a (List a) | Nil (1) 全てのデータコンストラクタを置
ロジバン - Wikipedia
ロジバン ( lojban [ˈloʒban] ( 音声ファイル) ) は、ログランを元に、さらなる機能性を追求して LLG が開発を引率してきた人工言語である。1987年に公表され、1997年に文法が暫定的に完成、2002年から実用段階に入った。主にインターネットを中心とする国際的な研鑽が進んでいる。 ログランから継承したものも含め、ロジバンは以下の性格を有する。 言語表現の論理的な構造を正確に（そしてしばしば簡潔に）記述するために開発されてきた述語論理を文法の基盤としている。そのため、自然言語では表現が困難であるような複雑な構造をごく明晰に記述できる一方で、文芸的理由から敢えて多義的な表現を織ることもでき、自然言語と同様、話者の自在に任せた表現が可能である。『In the Land of Invented Languages』の著者でありエスペラントやクリンゴン語に精通している Ari
再帰論述法 - アンサイクロペディア
再帰論述法とは[編集] 校長先生や政治家、さらには店長まで、効果的なスピーチをするときに、必ずといっていいほど必要なのがこの再帰論述法である。主に中年～中高年の男性に使われる（いわゆる知識層である）。しばしば幼稚園の園児や小学生などにも使われることがあるが、これが再帰論述法に当たるかとうかは判断がわかれるところである。また、歴史上の暴君が使用したこともある。 再帰論述法の具体的な効果としては、催眠がある。左のグラフは、授業中に眠ってしまう生徒の割合をグラフで示したもので、黄色が再帰論述法を使わない先生、緑色がときたま使ってしまう先生、桃色が常に使い続けている先生を表している。 一般に、教育現場では生徒を80％以上眠らせることは不可能（「別のこと」をやっているパターンがあるため）と言われており、再帰論述法の効果がいかに大きいかということを端的に示す例であるといえる。 分類[編集] 再帰論述法
バター猫のパラドックス - Wikipedia
起こりうる事態について描かれた漫画 バター猫のパラドックス（バターねこのパラドックス）は、2つの言い伝えを皮肉った組み合わせに基づいた逆説である。 猫は常に足を下にして着地する（参照：ネコひねり問題） バターを塗ったトーストは常にバターを塗った面を下にして着地する（参照：選択的重力の法則） もしバターを塗ったトーストを（バターを塗った面を上にして）猫の背中へくくり付けて、ある高さから猫を落としたらどうなるかを考えた場合、この逆説が発生する。 もし実際に猫を落とすならば、2つの最終結果のうちのどちらか一方は決して起こらないことになる。もし猫が足を下にして着地すれば、トーストはバターが塗られた面が上になったままだし、逆にバターが塗られた面が下になって着地するならば、猫は背中から着地することになるはずだ。 この逆説は言い伝えを皮肉った組み合わせが起源であるが、この2つの規則が常に正しいと仮定した
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Decidability Proof of LTL The goal of this note is to explain why LTL is decidable. Given an LTL formula ψ we explain how to build a finite transition system S with a “partial” labelling function L (this is explained below) such that ψ has a model
Amazon.co.jp: 数学基礎論: 新井敏康: 本
Amazon.co.jp: The Foundations of Mathematics (Studies in Logic: Mathematical Logic and Foundations): Kunen, Kenneth: 本
https://dl.acm.org/citation.cfm?id=96714
CiteSeerX
Amazon.co.jp: 論理と計算のしくみ: 萩谷昌己, 西崎真也: 本