広義の項書き換え系について考えている。書き換えと置換〈substitution〉は区別しなくていいだろう。とりあえず、3種類の書き換え＝置換がある。
- 関数項置換： 変数／リテラルをリーフとし、関数記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。
- 命題項置換： 原子論理式〈アトム〉をリーフとし、論理記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。
- バンチ置換： 論理式をリーフとし、構造構成子記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。
関数項置換、命題項置換、バンチ置換の上に、導出の書き換え＝リーズニング、リーズニングの書き換え＝メタリーズニング が構成される。
置換のなかで可逆・双方向なものを、等値置換（関数項のとき）、同値置換（命題項／バンチのとき）と呼ぶ。
