「命題」の曖昧性 真偽値 述語 論理式 （個体変数に関して）閉じた論理式 ところが、「論理式」が曖昧。 テンプレート述語項構文木（リーフが穴、ノードが述語コネクティブ） テンプレート述語項構文木＋述語コンテキスト 評価値である述語 型理論のときも、…

メタリーズニングの種類： ApplyReasoning : reas, deriv ≡> deriv ComposeReasoning : reas, reas ≡> reas ProductReasoning : reas, reas ≡> reas リーズニング 導出のマージ： MergeConj : conj → conj, con → conj ⇒ conj → conj MergeDisj : conj → dis…

$`\newcommand{\LLambda}{\mathrm{L}\Lambda} \newcommand{\Llambda}{\mathrm{L}\lambda} \newcommand{\RLambda}{\mathrm{R}\Lambda} \newcommand{\Rlambda}{\mathrm{R}\lambda} \newcommand{\Dia}{\diamondsuit} \newcommand{\mrm}[1]{\mathrm{#1} } \newco…

ド・モルガン双対 ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、 *(A1, ..., An) = (￢A1| ...| ￢An) *(,) = (|) *(A1| ...| An) = (￢A1, ..., ￢An) *(|) = (,) ** = id と定義する。推論規則は ￢ 左 (Γ → Δ| Φ) ⇒ (*Φ, Γ → Δ) …