解答提取过程的一般步骤
下面列出解答提取过程的一般步骤
（1）生成反演树，并对树中的合一加以标记。
（2）在目标公式否定式的子句中，用新的变量代替其中的Skolem函数。
（3）把目标公式否定的子句化为重言式，即附加其本身的否定式。
（4）仿照反演数的结构生成修改证明树，每个归结所用的合一集由反演树中相应的归结所使用的合一基来决定。
（5）修改证明树的根结点的子句即为解答语句。
习题
1、本章中虽然使用与或图来表示一些公式，但我们并没有提倡对定理证明使用可分解的系统。例如分解一个合取目标公式并独立的处理每一个合取公式的想法错误是什么？在什么情况下分解才是一个合理的策略？