自动定理证明的一个重要部分是通过弄清楚一个子句何时包含另一个子句来减少冗余。 直观地说，一个子句（CNF 中的一阶逻辑公式）C 包含另一个子句 D，当它至少是一般的。具体的定义是，必须用变量替换项，...