次の3つを混同しない！
- 定理のボディ（関数定義のボディ相当）
- 証明項
- リーズニング
リーズニング：
| バックワード | フォワード |
|---|---|
| 背景知識ベース | 背景知識ベース |
| リーズニング・ステージ | リーズニング・ステージ |
| ステージ・コンテキスト | ステージ・コンテキスト |
| 問題〈ゴール〉 | 判断 |
| 問題のコンテキスト | 判断のコンテキスト |
| 問題のターゲット命題 | 判断のターゲット命題 |
| 問題の未知項 | 判断の既知項 |
| 自明問題（終状態の問題） | 自明判断（始状態の判断） |
| リーズニング・ステップ | リーズニング・ステップ |
| タクティク | コンビネータ |
| 還元、分解 | 合成、生成 |
| タクティク・スクリプト | コンビネータ・スクリプト |
ちなみに、定理のヘッドは、定理名（オプショナル）とシーケント〈プロファイル〉からなる。定理のヘッドまたはシーケント〈プロファイル〉を定理のステートメントともいう。
バックワードリーズニングは、リーズニングの開始状態のセットアップが明確かつ簡単。それに対して、フォワードリーズニングは、状態の定義が曖昧で難しくなる。フォワードリーズニングが機械に向かない事情だろう。
