定理机器证明是通过计算机实现定理自动证明。自上世纪五十年代以来定理自动证明一直是计算机科学研究的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用。其中检测和删除逻辑公式中的冗余子句是该方向广泛研究的基本问题。基于已有的研究工作,本文围绕命题逻辑中子句和文字的相关知识,取得的主要研究结果如下：1、将命题逻辑的子句集中文字划分为三类,即有用文字、必需文字和无用文字,分别给出了三种文字的定义,同时得到了相应的等价描述方法,进而得到了三种文字之间的相互关系。得到了子句集中的必需文字是非冗余文字,子句集中的无用文字是冗余文字。2、基于子句集中文字的划分,得到了有用文字、必需文字和无用文字的判别方法,借助子句集的可满足性给出了三种文字与子句集的可满足性的等价条件。给出了有用文字、必需文字和无用文字的判定定理并设计相应算法。3、研究了命题逻辑的子句集中冗余子句的性质,得到了命题逻辑的子句集中冗余子句的等价定理,给出了命题逻辑的子句集中的有用子句、必需子句和无用子句的相关性质。根据子句集的可满足性得到了一种判断有用子句、必需子句和无用子句的判别方法,通过实例说明了该方法的有效性。