型ユニフィケーションは、証明ターゲット S⊆T を証明する過程の中心的な処理である。処理の結果として、いくつかの「不定命題＝動的なチェック条件」を出力する。注意：このエントリーは他の関連エントリーとの兼ね合いで大幅に修正したり、場所を移動したり…