記号的には、 [x1:t1, ..., xk:tk | A1, ..., An |- B] 最初はk個の変数型宣言。型理論で言う型環境。 次にn個の前提（仮説）論理式。 1個の結論論理式。 出現するすべての変数は型環境で型付けされている。 自然言語風の記述は： for x1:t1, ..., xk:tk giv…

オペラッドの射をオペ射と呼ぶ。オペラッドのホムセットをオペホムセットと呼ぶ。オペホムセットを O(A, B⇒C) のように書く。⇒の左が空なら終対象を置き、右が空なら始対象を置く。ニ様なシーケント（http://d.hatena.ne.jp/m-hiyama-memo/20161026/14774513…

環境として、論理環境（logical environment）と応用固有環境（application-specific environment）がある。論理環境は、論理定理データベースと論理推論規則データベースからなる。応用固有環境は、応用固有定理データベースと応用固有推論規則データベース…

"Preface: Twenty Years of the QED Manifes" というPDF文書がある。これはアクセスするとダウンロードされてしまう2ページの文書。ここで要約しておく。QEDマニフェストとワークショップが1994,5,6あたりに行われたので、2014,5,6あたりで20周年になる。当…

Natural Deduction Mizar SerND → introduction assume assume + use → elimination – apply ∧ introduction thus concat ∧ elimination – select ∨ introduction – add ∨ elimination per cases cases ∀ introduction let for ∀ elimination – instantiate …