自然演繹システムのグラフィカル指標

muses 論理 半形式証明スクリプト

次元0 ワイヤー、ケーブル

  1. ⊥： 波線
  2. T： 破線
  3. A: 実線
  4. Γ： 実線または幅付き線

次元1 ノード

次元1 AND

  1. X_{Γ, Σ} ： スワップ Γ # Σ → Σ # Γ
  2. Δ_Γ ： 分岐 Γ → Γ # Γ
  3. !_Γ ： 削除 Γ → T
  4. π^1_{A, B} : 横線 (A, B) → (A)
  5. π^2_{A, B} : 横線 (A, B) → (B)
  6. ∧_{A, B} ： 横線 (A, B) → (A∧B)

次元1 OR

  1. (X)_{A, B} ： スワップ (A | B) → (B | A)
  2. ∇_A ： 合流 (A | A) → (A)
  3. i_A ： 生成 ⊥ → (A)
  4. ι^1_{A, B} ： 横線 A → (A | B)
  5. ι^2_{A, B} ： 横線 B → (A | B)
  6. ∨_{A, B} ： 横線 A∨B → (A | B)

次元1 IMP

  1. lev_{A, B} ： 左評価 [A←B], B → A
  2. rev_{A, B} ： 左評価 A, [A→B] → B

次元2 図式描き換え

次元2 AND

  1. AND-intro
  2. AND-elm-left
  3. AND-elm-right

次元2 OR

  1. AND-intro-left
  2. AND-intro-right
  3. AND-elm

次元2 IMP

  1. IMP-intro-left
  2. IMP-intro-right
  3. IMP-elm-left
  4. IMP-elm-right

次元3 図式描き換えの等式

  1. ベータ等式
  2. 他