証明とリーズニング

次の3つを混同しない！

1. 定理のボディ（関数定義のボディ相当）
2. 証明項
3. リーズニング

リーズニング：

バックワード	フォワード
背景知識ベース	背景知識ベース
リーズニング・ステージ	リーズニング・ステージ
ステージ・コンテキスト	ステージ・コンテキスト
問題〈ゴール〉	判断
問題のコンテキスト	判断のコンテキスト
問題のターゲット命題	判断のターゲット命題
問題の未知項	判断の既知項
自明問題（終状態の問題）	自明判断（始状態の判断）
リーズニング・ステップ	リーズニング・ステップ
タクティク	コンビネータ
還元、分解	合成、生成
タクティク・スクリプト	コンビネータ・スクリプト

ちなみに、定理のヘッドは、定理名（オプショナル）とシーケント〈プロファイル〉からなる。定理のヘッドまたはシーケント〈プロファイル〉を定理のステートメントともいう。

バックワードリーズニングは、リーズニングの開始状態のセットアップが明確かつ簡単。それに対して、フォワードリーズニングは、状態の定義が曖昧で難しくなる。フォワードリーズニングが機械に向かない事情だろう。