4.10 小结

　　1．一阶谓词演算在人工智能系统中可作为知识表示的工具，其演绎推理方法可用来建立自动定理证明系统、问答系统和基于规则的演绎系统等。在定理证明系统中，反演法简单有效，系统不是直接证明F1∧F2∧…∧Fn→W为永真，而是去证明F＝F1∧F2∧…∧Fn∧~W为永假，这等价于证明公式F对应的Skolem化标准形子句集S＝S0∪{~W}为不可满足的。
　　2．归结反演系统是应用归结（消解）原理建立的产生式系统，它把子句集S作为初如数据库，不断应用归结推理规则生成出归结式来，当出现空子句（目标条件）的归结式时过程结束，这说明了S是不可满足的，从而使定理得到证明。
实现归结过程的搜索策略有支持集策略、单元子句优先策略、线性输入形策略和祖先过滤策略等，主要是解决提高搜索空子句的效率问题。
　　3．可以利用归结反演过程来提取问答，方法是先将询问表示成要证明的目标公式，再根据反演法求归结反演树，最后按反演树的过程构造修改证明树，其根部的子句就是要提取的回答。
　　4．基于规则的演绎系统是一个直接证明系统，主要强调直接使用规则进行演绎，以便使求解过程易于为人们所理解和接受。
　　正向演绎系统是从事实表达式出发，通过正向匹配应用规则进行推理，直到推出目标表达式。演绎过程是把事实表达式化为与或形表示，并按规定的与或关系表示成与或树形式来进行。
逆向演绎系统是从目标表达式出发，通过逆向匹配应用规则进行推理，直到推出事实表达式。演绎过程也是把目标表达式化为与或形表示，其与或关系是正向系统的对偶形式，其他过程类同。
　　5．一般来说，归结法也是一种问题的求解方法。可以把需要求解的问题用定理证明的形式来表示，然后用归结法证明，并通过修改证明树提取回答，从而可得到问题的解。