現時点での疑問点など
- タクティク、タクティカル（証明コンビネータ、推論コンビネータ）、ゴールなどは手続き的証明遂行の用語だよな。
- ファクト、ゴール、サブゴールとかを宣言的証明の文脈で使われても意味わからん。
- ファクトって何だよ？
- ゴールって意味不明だろ→Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4） - 檜山正幸のキマイラ飼育記
- Judgementが特殊な意味で使われているようだ。
- じゃ、普通の意味の判断＝シーケントはなんて呼ぶのだ？
- シーケントの左辺は何て呼ぶ？ これがcontextか。
- contextは論理式の集合、それともリスト（順序付き）？
- 組み込みクラスpropがワカラン。
- signatureは使わないようだ。使うとまた曖昧になるからいいけど。
- definition, statement, proofって、最も基本的だけど、定義がなくてワカラン。definitionのdefinitionが見つからない。
- local factって何？ factが意味不明で、localが意味不明。つまり、サッパリわからん。
- proof method？ メソッド？？ 推論ルールとは違う？ タクティクとも違う？ proof method = proof command？
- deduction ruleとinference ruleと単なるrule、気分で使っているだけ？
- そもそも、deductionとinferenceとproofって同じ？ 違う？？
- claimとconclusionとconsequenceは違う？
- assertionとclaimとpropositionて違う？
- contextは何？ environment, proof stateとは違う。proof stateとcontextの関係は？
- libraryは何を意味する。theoryの集合体？
- promiseとassumptionは違う？
- で、statementって何？ どういうときにstatementって言う？
- propositionとformulaとtermは違う？ 同じ？ 気分で使っている。
- goalって、conclusionと同義？ それともやっぱり goal = sequent？
- implicationとentailmentは違う？
- primitive, atomic, basic って区別している？ 気分で言ってる？
- 論理に関する説明は、だいたいは論理的には語ってくれない。用語は曖昧なままに使用される。ジャーゴン／方言多し。
