絵がダメダメ
KalvalaのGentle Introductionにある自然演繹とユニフィケーションの絵、Nipkowの http://isabelle.in.tum.de/coursematerial/PSV2009-1/session45/document.pdf の絵とか。ダメダメだ。
頑張って親切に説明しているが、誤解を助長するだけだろう。
やっぱりストリング図と同様に、グラフ書き換え系で説明すべきだろう。バックワードリーズニング、フォーワードリーズニングという分類のイイカゲンさ、導入規則と除去規則という分類の無意味さをキチンと説明しないとダメだ。
- intro書き換え：既知推論ノードを下側に挿入する
- elim書き換え： 既知推論ノードを上側に挿入する
- dest書き換え： 未知推論ノードを置き換える
次の3つを区別する。
- グラフの推論ノード、推論ブランチ
- コンテキスト＝ルールベース内のルールグラフ（スキームグラフ）、そのインスタンス化
- リーズニングステップ
定理、推論、証明などの言葉の曖昧性で、これらがゴチャゴチャになっている。
