逻辑公式的可满足性问题在工程技术、交通运输、军事及自然科学等领域有着广泛的应用。随着计算机求解问题容量的逐渐增大、求解的问题愈加复杂,命题逻辑中逻辑公式的冗余越来越多,浪费大量的储存空间和计算时间。检测并消除逻辑公式中的冗余可以有效的提高计算机储存空间利用效率和削减计算时间。本文研究逻辑公式的冗余性质及其判定,以期为冗余的消除提供一定的理论基础。主要的研究工作如下:一、研究冗余子句的性质,提出冗余子句的判定方法。首先,引用二元子句定义的隐藏文字及其相关性质提出逻辑公式中冗余子句的概念。然后,分别得到子句集中是否存在单元子句的判定方法;基于冗余子句的概念,讨论了逻辑公式中子句冗余的问题,推导出冗余子句与其相对应的子句集的可满足性的等价条件。最后,利用子句集间的等价性,得到了冗余子句的相应判定条件。二、研究了冗余文字的性质,提出冗余文字的判定方法。首先,根据二元子句中隐藏文字的添加规则,提出了子句集中冗余文字的概念,并得到冗余文字与其相对应的子句集的可满足性之间的关系。然后,根据冗余子句的相关性质,推导出冗余子句与冗余文字的相互关系。最后,根据子句集间的等价性,提出了判定冗余子句和冗余文字的方法。