足りてない！ これじゃダメだ
ポールソンにしろ1994年KalvalaのGentle Introductionにしろ、アルゴリズムと証明論を結ぶ話をしてない。まったくと言っていいほどに説明がない。
次のような事柄のあいだの関係が分からない。
- ルール（定理でもある）に付けられた、elim, intro, destという属性
- そもそも、ルール（の形になった定理）が、アルゴリズムでどう使われるのか。
- 除去レゾリューション（elim-resolution）、導入レゾリューション（intro-resolution）、解体レゾリューション（dest-resolutio）の実際のところ
- レゾリューションが論理的に正しい根拠
とにかく、自然演繹の論理的な議論と実際のアルゴリズム／ソフトウェアのあいだのギャップがすごくて、それを埋める説明がない。
- 自然演繹の証明図は証明オブジェクトであり、証明行為のログではない。
- 証明行為はグラフとみなした証明図（証明グラフ）のグラフ書き換えによって行われる。
- 証明グラフの書き換えはリーズニングと呼ぶことにする。
- バックワードリーズニング、フォーワードリーズニングという分類は適切ではないようだ。
- 説明でもソフトウェアUIでも、リーズニング対象である証明グラフの一部しか相手にされない。
- 全域的な状況が説明もされず、不明である。
- リーズニングが論理的に正当であることを示すには、全域的な状況が必要である。
- 全域的な状況に言及されてないということとは、論理的な正当化はされてない。
腹立たしい。
