用单元归结法(unit resolution)，证明 A1∧A2∧A3→B
其中 A1 = (∀x){¬(D(x) → E(x)) → (∃y)(F(x,y)∧H(y))}
A2 = (∃x){D(x)∧G(x)∧(∀y)(F(x,y) → G(y))}
A3 = (∀x)(¬E(x)∨¬G(x))
B = (∃x)(H(x)∧G(x))
为了证明A1∧A2∧A3→B，我们将表达式转化成否定的形式，即 A1∧A2∧A3∧¬B
接下来，我们使用单元归结法。
首先，我们将A1化简为 (∀x){¬(D(x) → E(x)) → (∃y)(F(x,y)∧H(y))} 等价于 (∀x)(D(x) ∧ (∀y)(F(x,y) → ¬H(y))) → ¬E(x)
然后，我们将A2化简为 (∃x){D(x) ∧ G(x) ∧ (∀y)(F(x,y) → G(y))} 等价于 (∃x)(D(x) ∧ G(x) ∧ (∀y)(¬F(x,y) ∨ G(y)))
接下来，我们将A3化简为 (∀x)(¬E(x)∨¬G(x))
最后，我们假设¬B，即 (∀x)(¬H(x) ∨ ¬G(x))
接下来，我们使用归结法：
-
从A1中选取子句¬E(x)，从A3中选取子句¬E(x) ∨ ¬G(x)，进行归结，得到 (∀x)(D(x) ∧ (∀y)(F(x,y) → ¬H(y))) ∨ (∀x)¬G(x) 这个式子中有一个普遍量化变量和两个子句，所以我们需要重命名这个变量 (∀x)(D(x) ∧ (∀y)(F(x,y) → ¬H(y))) ∨ (∀z)¬G(z) 这个式子没有与其他子句可以归结，所以需要继续使用单元归结法。
-
从A2中选取子句¬F(x,y) ∨ G(y)，从第1步中的归结结果中选取子句¬G(z)，进行归结，得到 (∃x)(D(x) ∧ G(x) ∧ G(y)), 其中y是第1步中的普遍量化变量 这个式子中有一个存在量化变量和两个子句，所以我们需要重命名这个变量 (∃x)(D(x) ∧ G(x) ∧ G(y)), 其中y是第1步中的普遍量化变量，x和y不相同。
-
从第2步中的归结结果中选取子句G(y)，从A3中选取子句¬G(y)，进行归结，得到 (∃x)(D(x) ∧ G(x) ∧ ¬E(y)), 其中y是第1步中的普遍量化变量，x和y不相同。
-
从第3步中的归结结果中选取子句D(x)，从第1步中的归结结果中选取子句D(x)，进行归结，得到 G(x) ∧ (∀y)(F(x,y) → ¬H(y)) ∧ ¬E(y)，其中x和y不相同。
-
从第4步中的归结结果中选取子句¬E(y)，从A3中选取子句¬E(y) ∨ ¬G(y)，进行归结，得到 G(x) ∧ (∀y)(F(x,y) → ¬H(y)) ∧ ¬G(y)，其中x和y不相同。
-
从第5步中的归结结果中选取子句¬G(y)，从第2步中的归结结果中选取子句G(y)，进行归结，得到 (∃x)(D(x) ∧ G(x) ∧ H(y)), 其中y是第1步中的普遍量化变量，x和y不相同。
-
从第6步中的归结结果中选取子句H(y)，从假设的¬B中选取子句¬H(y)，进行归结，得到 假
由此，我们证明了A1∧A2∧A3→B成立。