リーズニング規則の種類

• 生成規則 generation： 前提（既存証明オブジェクト）がないところから証明オブジェクトを1個作る
• 変形規則 deformation： 1つの前提から証明オブジェクトを1個作る
• 組み合わせ規則 combination： 複数の前提から証明オブジェクトを1個作る

また、リーズニング規則はグラフのリストからグラフのリストへの写像とみなすほうがよいだろう。グラフをツリーに限れば、これはヘッジからヘッジとも言える。実際はツリーに限定するのは難しい。

グラフ書き換えとしてのリーズニング規則と、ゴールを展開するレゾリューションはまったく違う。これを混同するから混乱する。レゾリューションは論理的な規則ではなくてアルゴリズムだ。レゾリューションアルゴリズムが論理的に正当であることは別に証明（メタ証明）を要する。