Isabelleの用語法の無茶苦茶さや、概念の混乱、理解のためのミッシングリンク、これらの大きな部分は「次元概念の欠如」によるのではないだろうか？ -- まず間違いない。 参考：シーケント計算、ムービー、高次圏 - 檜山正幸のキマイラ飼育記 メモ編 参考：…

オカシイ、オカシイ。除去規則（elim rule）がIsar satement formatだとobtainsで書かれる。これはオカシくはない、つうかまっとうなんだが、逆に通常の除去規則の書き方はいったいなんなんだ？ ということになる。disjEの例だと： ?P ∨ ?Q ==> (?P ==> ?R) …

ウッヒャーー、またしても新用法を発見。subgoalがsolveすべき対象である命題（＝論理式＝ルール＝定理）で、goalはそれらsubgoal達の集合の意味で使っている。つまり、ゴール＝サブゴールズ。しかし、サブゴールの結論をゴールと呼ぶことがあるから。「ゴー…

メニューツリーのパス: [Plugins]-[Plugin Options] タブ: [Plugin Options] ツリーコントロールのパス: /Isabelle/General レコードのフィールド名: Auto Quickcheck UIの種類を無視してパスで示すと Plugins/Plugin Options/Plugin Options/Isabelle/Gener…

「なるほど」とは思うが、なんか、これしか方法がないのかよ？ とも感じる。 Isabelleではgoal文はないので、lemma "命題" と書いて、この行の表示（カーソルあわせてOutputを見る）で、ゴールを見せる。 タクティクの説明は、apply(タクティク) oops とする…

ストリング図とストリンググラフの関係を使い、グラフ理論的な操作として証明行為＝リーズニングを理解する。キーワード（大事な言葉）の定義： 推論ノード：通常の推論規則を表す。複数（0個もあり）の入力（仮定）と1つの出力（結論）を持つ。 ワイヤー：…