自动推理作为人工智能研究领域中一个经典且非常重要的研究方向,在人工智能蓬勃发展的今天,面临着新的发展与挑战。不同于基于神经网络与概率统计的机器学习,自动推理是一种建立在严谨逻辑推理基础上的演绎系统,在知识表达、知识推理以及形式化验证方面受到越来越多学者的关注。基于一阶逻辑的自动定理证明系统（Automatic Theorem Prover,ATP）作为自动推理基础理论研究与实际应用工具研究中的重要内容,一直是广泛关注的研究热点。近年来,一阶逻辑证明器的研究取得了较大进展,不少学者研究并开发了各自的一阶逻辑证明器。但是,大多数一阶逻辑证明器都是基于归结原理,归结过程中采用传统二元归结方式,即一次只用两个子句进行归结,忽视了多子句间的协同演绎能力。因此,这些一阶逻辑证明器普遍存在推理能力过于依赖特定的启发式策略、生成大量归结子句易导致搜索空间组合爆炸等问题。本文针对传统一阶逻辑证明器两个子句归结效率低、缺少多子句协同性等问题,提出并设计了基于动态多元协同演绎的一阶逻辑证明系统以及相关算法。论文的主要创新性研究工作包括以下几点:（1）提出了一种适用于动态多元协同演绎的“分层式项共享”数据结构及相关算法。该数据结构能有效避免多子句协同演绎时,由于变元更名操作导致的子句重复拷贝问题。在此基础上,针对含变元项较多的一阶逻辑公式,提出了一种“变元项完全共享”数据结构及相关算法。实验结果显示,与传统数据结构相比平均节省了大约70%的内存空间。（2）提出了基于一阶逻辑Herbrand语义特征的“项稳定度”和“项关联度”定义。从语义的角度分析了一阶逻辑项在合一替换中的影响因素,给出了一种项替换的稳定度评估算法。结合动态多元协同演绎特征,给出了基于项稳定度的文字和子句选择策略,将该策略应用于子句集的归入冗余检查。实验结果表明,该方法能较好地刻画一阶逻辑中的项特征,与基于项序的传统文字选择方法相比,其检查次数平均减少50.8%,运行时间平均缩短53.3%。（3）提出了一种基于矛盾体分离演绎推理理论的动态多元协同演绎算法架构,结合表语义（Tableau）与浸透归结（Saturation）两种传统证明空间搜索方法,提出了适用于动态多元协同演绎算法的证明空间搜索策略:基于强化学习的主动演绎策略和基于子句充分使用的被动演绎策略。将多子句协同演绎引入证明过程,设计了一种新的基于动态多元协同演绎的自动定理证明器MC-SCS,共证明了TPTP问题库中3863例一阶逻辑结论,其中有5个一阶逻辑公式是国际上其他证明器至今无法证明。（4）将MC-SCS证明器与传统二元归结证明器相结合,提出了一种基于动态多元协同演绎的结合证明算法。对结合证明系统演绎特征进行分析,提出了适用于结合证明的启发式策略,针对性的生成有利于二元归结的引理,从而提升了二元归结方法的演绎推理能力。设计了基于动态多元协同演绎的一阶逻辑结合证明系统Co Prover。实验结果显示,与独立使用传统二元归结证明器相比,Co Prover能大幅提高一阶逻辑公式的演绎推理能力。其中,相比独立使用Prover9证明器,与Prover9相结合的Co Prover结合证明系统,演绎推理能力平均提高了65%,并且成功证明了国际上其他证明器无法证明的103个结论。