子句集简化是自动推理领域中命题逻辑可满足性问题求解和一阶逻辑定理证明的重要研究内容,而在子句集简化的过程中,人们必须保证简化的正确性和合理性,因而对命题逻辑和一阶逻辑子句集的冗余性研究是必不可少的。探讨命题逻辑和一阶逻辑子句集中各个部分之间的关系,以便确定子句集中变量、文字或者子句的冗余性,不管在理论层面还是在应用层面都有重要意义。本文主要针对命题逻辑和一阶逻辑子句集的冗余性进行深入研究,进而研究其应用。首先分析研究了命题逻辑和一阶逻辑子句集中子部分之间的关系,建立了多种层层递进的子句消去合一原则;证明了这些子句消去合一原则的可靠性;依据合一原则,提出了多种子句消去方法;探讨了这些子句消去方法的性质;最后,选取了一部分子句消去方法设计实际算法并优化,作为命题逻辑可满足性问题求解器预处理方法,检验这些方法对命题逻辑子句集的简化效果。主要取得了以下研究成果:第一部分建立了命题逻辑蕴涵模归结子句消去合一原则,证明了该原则在命题逻辑中的可靠性;基于该原则,提出了多种子句消去方法,证明了这些子句消去方法在命题逻辑中的可靠性;对这些子句消去方法设计具体算法,作为命题逻辑可满足性问题求解器的预处理方法进行实验,实验表明新型的子句消去方法比已有的子句消去方法化简子句集的能力更强。第二部分提出了命题逻辑多文字蕴涵模归结子句消去合一原则;证明了该原则在命题逻辑子句集中的可靠性;基于该原则,提出了多种子句消去方法,且这些方法在命题逻辑子句集中具有可靠性;在当前主流的封锁子句消去方法的算法框架上进行改进,提出了集合封锁子句消去方法的优化算法。第三部分构建了一阶逻辑等词蕴涵模归结子句消去合一原则;将多种不带等词子句集上的子句消去方法提升至一阶逻辑带等词子句集上,包括等词归结不对称有效子句消去方法、等词归结包含子句消去方法和等词覆盖子句消去方法;证明了这些子句消去方法在一阶逻辑带等词子句集上的可靠性;探讨了这些子句消去方法的各类性质;除此之外,凭借该原则证明了已有子句消去方法—谓词消去方法和等词封锁子句消去方法的可靠性。第四部分定义了一阶逻辑中四种新型冗余性质:集合封锁子句、扩展集合封锁子句、等词集合封锁子句和扩展等词集合封锁子句;前两者是不带等词子句集上的冗余性质,后两者是带等词子句集上的冗余性质,证明了这四种冗余性质在对应子句集上的可靠性;并且对集合封锁子句、扩展封锁子句、等词集合封锁子句和扩展等词集合封锁子句的性质进行了探讨。第五部分建立了一阶逻辑多文字蕴涵模归结子句消去合一原则和等词多文字蕴涵模归结合一原则;分别证明了多文字蕴涵模归结合一原则在一阶逻辑不带等词子句集和等词多文字蕴涵模归结合一原则在一阶逻辑带等词子句集上的可靠性;证明了这两种合一原则比一阶逻辑中的蕴涵模归结合一原则和等词蕴涵模归结合一原则更为高效;此外,基于这两种原则,提出了多种子句消去方法,分别比较了新型子句消去方法与蕴涵模归结合一原则和等词蕴涵模归结合一原则下子句消去方法的高效性;最后经由这两个原则证明了第四部分中的集合封锁子句消去方法和等词集合封锁子句消去方法的可靠性。