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

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

保証〈warranty〉 ： derivation T → A 反駁〈refutation〉 ： derivation A → ⊥ 証拠〈witness〉 ： 存在記号導入に使う要素、項 事例〈instance〉 ： 全称記号消去に使う要素、項 存在スタート条件〈existential starting condition〉 ： 存在記号消去に伴…

data Tree a = Leaf a | Tree (Tree a) (Tree a) 値コンストラクタ、型コンストラクタ、型が紛らわしいという例。値コンストラクタをタグだと考えると： type Tree<A> = @Leaf A | @Tree [Tree<A>, Tree<A>] タグ @Leaf, @Tree に対応する値コンストラクタを ^Leaf, ^</a></a></a>…

対象物： 型 関数 値〈データ | ポイント〉 特別な関数 汎関数〈メタ関数〉 命題（真偽値、述語、論理式） 導出 保証 特別な導出 リーズニング〈メタ導出〉 カリー／ハワード／ランベック対応 型 命題 関数 導出 値 保証 汎関数 リーズニング 項： 型項（多…

https://arxiv.org/abs/2102.03044 から。 証明が行うこと 読者の心に形成されるもの guarantee trust explain insight, understanding

https://arxiv.org/abs/2102.03044 の冒頭、同語義： {mathematical | logical | rigorous | formal | rational}* {derivation | proof} 単なる多義語ならいいのだけど、実際には曖昧語になっているのがタチが悪い。

動詞 DoSomething 名詞 Something 短縮 construct construction cons calculate calculation calc derive derivation deriv reason reasoning reas Begin Something WeHave A And, B Using Something X params WeHave A' And, B' Using Something Y params .…

$`\newcommand{\Sep}{\mathrel{\|} } \newcommand{\Subst}[2]{ {\scriptsize \begin{bmatrix} #1\\ #2 \end{bmatrix} } } %`$$`\quad \alpha \Sep \varphi: \Gamma \to B`$ここで： 型コンテキストはギリシャ文字小文字 命題コンテキストはギリシャ大文字 命…