シーケント計算をリーズニング構成の計算と考える。できるだけ少ないリーズニングで計算をしたい。リーズニングを少なくするには、プリミティブな導出を揃える。 ∧-モノイド構造 ∨-モノイド構造 ![A] Θ[A] Δ[A] ∇[A] π1[A, B] ι1[A, B] π2[A, B] ι2[A, B] X[…

知識ベースには、次のようなものが入っている。 型の宣言・定義 関数の宣言・定義 命題の宣言・定義 導出の宣言・定義 リーズニングの宣言・定義 メタリーズニングの宣言・定義 それらを組織化する構造ファセット 知識ベースを背景にして、新しい型／関数／…

とある論文で使っていた用語法： シーケントの左辺 ＝ antecedent〈前件〉 シーケントの右辺 ＝ succedent〈後件〉 イニシャルシーケント ＝ 公理シーケント シーケントの推論規則用語： 上式 ＝ premises〈仮定〉 下式 ＝ conclusion〈結論〉 前件、後件、…