4.3 归结反演系统（Refutation）

　　归结反演系统是用反演（反驳）或矛盾的证明法，使用归结推理规则建立的定理证明系统。这种证明系统是基于归结的反证法，故称归结反演系统。它不限于数学中的应用，其基本思想还可用在信息检索、常识性推理和自动程序设计等方面的问题。
　　上一节已经证明了反演法证明过程的正确性。下面来讨论该过程的产生式系统描述及其搜索策略。