检测和消除命题逻辑公式中的冗余子句,是许多应用领域(包括人工智能)广泛研究的基本问题。基于已有的研究工作,本文主要探讨命题逻辑公式中的冗余子句及冗余文字。本文的主要研究工作包括：1.将子句集中的子句划分为三类：无冗余子句、相对冗余子句和绝对冗余子句,并分别给出了一些等价描述方法：S是命题逻辑中子句集,C∈Sred,C在S中是相对冗余的当且仅当存在S的一个无冗余等价子集S’,使S’{C}|≠C；C在S中是绝对冗余的当且仅当S的无冗余等价子集恰为S\{C}的无冗余等价子集。2.当命题逻辑公式蕴涵某一文字时,给出了子句集中某几类子句是冗余子句的一些等价结论。若S是命题逻辑中子句集,S|=l,C∈S,l∈C,则C在S中是冗余的当且仅当C在(S\S(l))U{1}是冗余的。此外,进一步得到了子句集中包含冗余文字的一些等价结论,以及子句集中子句中的文字是冗余文字的等价描述,即S={C1,C2,…,Gn,D}是命题逻辑中子句集,D=x∨D1,x是D中关于S的冗余文字当且仅当D1S’={D1,x,C1,C2,…,Cn}中的冗余子句。3.从子句集的极小不可满足子集与可满足核两个方面讨论同子句集冗余性的关系,并利用子句集的可满足性提出了一种判定子句集中冗余子句和冗余文字的方法,即若S={C1,C2,…,Cn,D>是命题逻辑中子句集,且D中不含互补文字,D是S中冗余子句当且仅当子句集S’={C1,C2,…,Cn>∪D不可满足；若D=x∨D1,x是D中关于S的冗余文字当且仅当子句集{x,C1,C2,...,Cn}∪D1不可满足。