タグ

2012年10月12日のブックマーク (4件)

  • 基礎演習 I 論理学

    CAPE論理学上級Ⅱ「構成的型理論」 開催予定日(中継urlはポスト下部を参照してください) ① 3月26日(土)1030-1230「ラッセルのパラドックスと3つの対策」 ② 3月26日(土)1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」 ③ 3月27日(日)1030-1230「証明論的意味論としてのマーティン・レーフの構成的型理論」 ④ 3月27日(日)1430-1630「認識論の機械化:証明の正規化と証明支援系」 ①3月26日(土)1030-1230「ラッセルのパラドックスと3つの対策」 [2021CAPE公開セミナー] 論理学上級 Ⅱ-1「ラッセルのパラドックスと3つの対策」 from Shunsuke Yatabe ②3月26日(土)1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」 [2021CAPE公開セミナー] 論理学

    基礎演習 I 論理学
  • シークエント計算 - Wikipedia

    制約: (∃L) と (∀R) の規則において、変項 は と に自由出現をもたない。 なお、(∃L) と (∀R) の規則、および、制約は次を採用してもよい。 制約: (∃L) と (∀R) の規則において、変項 は に自由出現をもたない。 直観的説明[編集] 上記の規則群は「論理規則」と「構造規則」に分けられる。論理規則は帰結関係 の右辺か左辺に新たな論理式を導入する。一方、構造規則はシークエントの構造を操作し、論理式の正確な形を無視する。例外として同一性の公理 (I) とカット規則 (Cut) がある。 形式化されているものの、これらの規則は古典論理的に直観的に読み解くことができる。例えば、(∧L1) 規則を見てみよう。これは、A を含む論理式の列から Δ が証明される場合は常に A∧B という(より強い)仮定からも Δ が導かれることを示している。同様に、(¬R) 規則 は Γ と

    シークエント計算 - Wikipedia
  • 自然演繹 - Wikipedia

    自然演繹(しぜんえんえき、英: Natural deduction)は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 自然演繹論理[編集] 自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基的規則だけを持つ。 仮定の規則 "The Rule of Assumption" (A) モーダスポネンス "Modus Ponendo Ponens" (MPP) 二重否定の規則 "The Rule of Double Negation" (DN) 条件付き証明の規則 "The Rule of Conditional Proof" (CP) ∧-導入の規則 "The Rule of ∧-introduction" (∧I) ∧-除去の規則 "The Rule o

    自然演繹 - Wikipedia
  • 夕暮ログ JSON.parseとevalなどの比較とスピードテスト

    JSONはjavascriptのオブジェクトの記法をベースにしたもので、主にjavascriptでオブジェクトを文字列で表す際に利用されます。 特にAjax分野ではかなり多用されます。 非常に扱いやすいので、さまざまなプログラミング言語で使うことが出来るようになってきています。 JSONは文字列なので、それをオブジェクトに変換して使うわけですが現在javascriptでやるにはいくつかの方法があります。 eval new Function JSON.parse jQuery json2.js それぞれの違いについて改めて調べてみました。 eval、new Function evalとnew Functionは古くから使われている方法です。 どちらも文字列をjavascriptとして認識、実行する方法です。 JSONはjavascriptのオブジェクトを書く方法がベースとなっているので普通に