归结反演##########
定义
应用归结原理（如Robinson）证明定理的过程称为归结反演
步骤
- 将已知前提表示为谓词公式F
- 将待证明的结论表示为谓词公式Q，并得到它的否定 非Q。
- 把谓词公式集 {F, 非Q}化为子句集S
- 用归结原理对子句集S中的子句进行归结，把得到的归结式并入S中，直到出现空子句就停止归结
示例
1. 前提 -> 谓词公式
2. 结论 -> 其否定
3. 公式 -> 子句集
4. 对子句集进行归结
还可有其他归结路径
图中归结出了空子句，所以结论成立
问题求解##########
定义
归结原理除了可用于定理证明外，还可用于问题求解
步骤
示例
