自动推理是人工智能重要的组成部分,主要包括命题逻辑求解和一阶逻辑定理证明。一阶逻辑系统相比命题逻辑系统具有更丰富的表达能力,许多的现实问题都可用一阶逻辑表示。因此,对于一阶逻辑自动定理证明器的研究具有重要的学术价值和广泛的应用前景。目前一阶逻辑自动定理证明器普遍采用浸透算法演绎框架和二元归结方法。浸透算法是一种局部的演绎框架,其子句的选择效率对于启发式策略的要求非常高。二元归结方法每次有且只有2个子句进行归结,只消去一组互补对文字,导致归结式文字数较多,其演绎机制存在潜在的提升空间。矛盾体分离规则是徐扬教授提出的一种多元演绎方法,该方法突破了传统二元归结方法每次限定只有2个子句参与演绎,每次只消去1组互补对文字的限制,具有很多优良的演绎特性。本文重点研究了基于矛盾体分离理论的一阶逻辑自动定理证明器的各个组成部分、系统构建、演绎过程验证和实验评估,设计实现了基于矛盾体分离演绎的一阶逻辑自动定理证明器、基于矛盾体分离演绎的一阶逻辑自动定理证明融合系统、基于矛盾体分离演绎的一阶逻辑自动定理证明验证检查工具,包含了用于一阶逻辑自动定理证明的整个体系。在矛盾体分离理论方面,提出了一种矛盾体分离演绎子句约简规则,能通过分析演绎特点高效地对子句进行约简,并证明了方法的可靠性。提出了几种矛盾体分离演绎方法,缩减了矛盾体分离演绎的路径搜索空间。在一阶逻辑子句集预处理方法上,针对当前一阶逻辑自动定理证明器中的预处理技术采用基于符号相关性的方法,提出了一种基于刻画文字间演绎距离的子句集预处理方法,能有效地对子句集进行约简。将该方法应用于一阶逻辑自动定理证明器Vampire(国际证明器竞赛排名第一)中,一定程度上提高了其定理证明的能力。研究了基于矛盾体分离演绎的启发式策略,通过分析矛盾体分离演绎过程中的路径搜索决策,提出了子句选择策略、文字选择策略、矛盾体分离式评估策略、矛盾体分离式演绎控制策略,有效地优化了矛盾体分离演绎路径的搜索。基于不同的路径搜索方案,提出了3种有效的矛盾体分离演绎算法,分别称为基于较优子句的矛盾体分离演绎算法、基于优化演绎路径的矛盾体分离演绎算法,基于充分使用子句的矛盾体分离演绎算法。在演绎过程中能通过回溯机制搜索较优的路径,从而提高了路径搜索的效率。在定理证明过程中,提出了一种基于起步子句迭代演绎的路径搜索算法,有效地规划了矛盾体分离演绎的搜索路径,且能提升子句参与矛盾体分离演绎的充分性。设计和实现了基于矛盾体分离演绎的一阶逻辑自动定理证明器CSE,并正式发布3个符合国际标准的版本(CSE 1.0、CSE 1.1和CSE 1.2),并参加了近2年的国际一阶逻辑自动定理证明竞赛,其性能都超过了知名证明器Prover9。CSE证明器可用于对一阶逻辑定理进行自动证明,支持命令行运行方式和界面运行方式,支持策略的多种使用方法。以来自TPTP中的定理作为测试例,CSE证明器超过了许多知名的一阶逻辑自动定理证明器,能证明一些其它证明器无法证明的定理。研究了CSE与其它证明器的融合方法,提出了2种融合方法用于不同难度系数的一阶逻辑定理判定。选取了一阶逻辑自动定理证明器Vampire(国际证明器竞赛排名第一)和Eprover(国际证明器竞赛排名第二)进行融合,设计实现了2套融合系统CSE＿V和CSE＿E,其中CSE＿E在参与的2018年国际一阶逻辑自动定理证明器竞赛中获得了第二名(标准一阶逻辑问题组)。支持不可满足问题和可满足问题判定。以一阶逻辑自动定理证明器国际竞赛例进行测试评估,CSE＿V和CSE＿E定理证明能力都超过了融合的证明器本身(Vampire、Eprover)。此外,CSE融合系统还证明了一批Rating等于1的定理。研究了CSE证明器和CSE融合系统的演绎过程验证方法,设计实现了2套系统的演绎过程验证检查工具,有效地保障了演绎的正确性。