第5期 邓鹏，等：命题逻辑的子句集中文字的分类 ·737. 文字的析取组成，因此能够对其中的文字进行科学 3)称C在S中是无用的(useless),如果对于S 合理的分类对研究冗余文字和冗余子句很有必要， 的任一无冗余等价子集S',有C主S'。 这些理论为归结自动推理奠定了基础。 定理1)设S是子句集，C∈S,C在S中是必 逻辑公式的化简是计算机科学和人工智能领域 需的当且仅当S-{C≠C。 重要的研究方向。逻辑上的冗余问题已被许多学者 定理2】设S是子句集，C∈S。C在S中是 广泛研究4)，包括不同计算问题的复杂性的刻画。 有用的当且仅当存在S的一个无冗余等价子集$”， 其中，主要包括冗余性在实际可满足性求解中的重 使S-{C}≠C。 要作用的研究[s)。P.Liberatore!)对命题逻辑中的 定理3)设S是子句集，C∈S。C在S中是 子句集进行了分类，给出了冗余子句的一些等价条 无用的当且仅当S的无冗余等价子集恰为S-{C} 件和性质。翟翠红等]研究了命题逻辑中的冗余 的无冗余等价子集。 子句和冗余文字，讨论了子句集的无冗余等价子集。 定理4)设S={C1,C2,…,Cn,D}是命题逻 唐世辉]研究了命题逻辑中子句集的冗余性，将命 辑中子句集，且D中不含互补文字。D是S中冗余 题逻辑中子句分为绝对冗余、相对冗余和无冗余3 子句当且仅当子句集S={C,C2,…,Cm}U{D}不 类。因此，本文主要深入研究命题逻辑的子句集中 可满足。 文字的特征，将命题逻辑的子句集中的文字划分为 定义5]设S={C1,C2,…,Cm,D}是命题逻 有用文字、必需文字和无用文字，讨论3种文字的关 辑中子句集，D=xVD,其中x是一文字，D1是一子 系。最后得到有用文字、必需文字和无用文字的判 句，如果DAC,AC2∧…ACm=D1AC1 定方法，为命题逻辑公式的化简提供理论支撑。 C2∧…八Cm,则称x是D中关于S的冗余文字。 1预备知识 定理5I12)设S={C1,C2,…,Cm,D}是命题逻 辑中的子句集，D=xVD,如果D1是S={C1,C2, 在命题逻辑公式中，称原子公式及其否定叫做 …,Cm,D}中的冗余子句，则x是D中关于S的冗 文字，有限多个文字的析取叫子句，只含有一个文字 余文字 的子句称为单子句。 定义1设A(P1,P2,…P)eF(S),则当A 定理6设S={C1,C2,…,C.,D}是命题逻 辑中子句集，D=xVD,x是D中关于S的冗余文字 具有形式(Q,VQ2V…VQ)A…∧(QVoV 当且仅当D1是子句集S={D1,x,C,C2,…,Cm}中 …VQn)时，称A为合取范式(conjunction normal 的冗余子句。 form,CNF),这里Q,=p或Q,=P(ji=1,2,…,n; 定理7]设S={C,C2,…,Cn,D}是命题逻 i=1,2,…,m)。 辑中子句集，且D中不含互补文字。D是S中冗余 定义21s1设S={C1,C2,…,C.,D}是命题逻 子句当且仅当子句集S={C,-D,C2-D,…,CmD} 辑中的子句集。显然，D是S中的冗余子句，当且仅 不可满足。 当C,AC2A…∧CmAD=C,AC2A…ACm。 对于子句集S,令Sl,={C1C∈S且{x,x}∩ 一个子句是冗余的，暗示此子句可以从子句集 C=☑}U{C\{x}IC∈S且x∈C},SIx= 中删除，不会影响子句集所要表示的信息。同理，一 （((S1x）13)…1x,),其中4={x1,x2,…,x}。 个子句集是冗余的，可以定义为它和它的一个真子 定理81)设S={C1,C2,…,Cm,D}是命题逻 集等价。 定义3川子句集S是冗余的，当且仅当存在 辑中子句集，子句集S={C1,C2,…,Cm}U{D}不 S'CS,使S'=S。 可满足当且仅当子句集(S1{D})方不可满足。 在命题逻辑中，此定义和如下说法是等价的： 2子句集中文字的分类 1)存在SCS,使S=S: 2)S中含有冗余子句。 定义6设S={C1,C2,…,Cm}是命题逻辑中 定义4)设S是子句集，C∈S 的子句集，如果对于S中的任一子句C:,若有C:= 1)称C在S中是必需的(necessary),如果对于 xVD(ie{1,2,…,m}),其中x是一文字，D是一 S的任一无冗余等价子集S',有C∈S'; 子句，且x不是C:中关于S的冗余文字，则称x是S 2)称C在S中是有用的(useful),如果存在S 中的必需文字。 的一个无冗余等价子集S',使C∈S': 定义7设S={C1,C2,…,C}是命题逻辑中文字的析取组成，因此能够对其中的文字进行科学 合理的分类对研究冗余文字和冗余子句很有必要， 这些理论为归结自动推理奠定了基础。 逻辑公式的化简是计算机科学和人工智能领域 重要的研究方向。 逻辑上的冗余问题已被许多学者 广泛研究［１⁃４］ ，包括不同计算问题的复杂性的刻画。 其中，主要包括冗余性在实际可满足性求解中的重 要作用的研究［５⁃１１］ 。 Ｐ．Ｌｉｂｅｒａｔｏｒｅ ［１］ 对命题逻辑中的 子句集进行了分类，给出了冗余子句的一些等价条 件和性质。 翟翠红等［１２］ 研究了命题逻辑中的冗余 子句和冗余文字，讨论了子句集的无冗余等价子集。 唐世辉［１３］研究了命题逻辑中子句集的冗余性，将命 题逻辑中子句分为绝对冗余、相对冗余和无冗余 ３ 类。 因此，本文主要深入研究命题逻辑的子句集中 文字的特征，将命题逻辑的子句集中的文字划分为 有用文字、必需文字和无用文字，讨论 ３ 种文字的关 系。 最后得到有用文字、必需文字和无用文字的判 定方法，为命题逻辑公式的化简提供理论支撑。 １ 预备知识 在命题逻辑公式中，称原子公式及其否定叫做 文字，有限多个文字的析取叫子句，只含有一个文字 的子句称为单子句。 定义 １ ［１４］ 设 Ａ（ｐ１ ，ｐ２ ，…，ｐｍ ）∈Ｆ（Ｓ），则当 Ａ 具有形式（Ｑ１１∨Ｑ１２∨…∨Ｑ１ｎ ）∧…∧（Ｑｍ１∨Ｑｍ２∨ …∨Ｑｍｎ ） 时，称 Ａ 为合取范式（ ｃｏｎｊｕｎｃｔｉｏｎ ｎｏｒｍａｌ ｆｏｒｍ， ＣＮＦ），这里Ｑｉｊ ＝ ｐｊ 或Ｑｉｊ ＝ ¬ ｐｊ（ ｊ ＝ １，２，…，ｎ； ｉ ＝ １，２，…，ｍ）。 定义 ２ ［１５］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中的子句集。 显然，Ｄ 是 Ｓ 中的冗余子句，当且仅 当Ｃ１∧Ｃ２∧…∧Ｃｍ∧Ｄ≡Ｃ１∧Ｃ２∧…∧Ｃｍ 。 一个子句是冗余的，暗示此子句可以从子句集 中删除，不会影响子句集所要表示的信息。 同理，一 个子句集是冗余的，可以定义为它和它的一个真子 集等价。 定义 ３ ［１］ 子句集 Ｓ 是冗余的，当且仅当存在 Ｓ′⊂Ｓ，使 Ｓ′＝ Ｓ。 在命题逻辑中，此定义和如下说法是等价的： １）存在 Ｓ′⊂Ｓ，使 Ｓ′⊨Ｓ； ２）Ｓ 中含有冗余子句。 定义 ４ ［１］ 设 Ｓ 是子句集，Ｃ∈Ｓ， １） 称 Ｃ 在 Ｓ 中是必需的（ｎｅｃｅｓｓａｒｙ），如果对于 Ｓ 的任一无冗余等价子集 Ｓ′，有 Ｃ∈Ｓ′； ２）称 Ｃ 在 Ｓ 中是有用的（ ｕｓｅｆｕｌ），如果存在 Ｓ 的一个无冗余等价子集 Ｓ′，使 Ｃ∈Ｓ′； ３）称 Ｃ 在 Ｓ 中是无用的（ｕｓｅｌｅｓｓ），如果对于 Ｓ 的任一无冗余等价子集 Ｓ′，有 Ｃ∉Ｓ′。 定理 １ ［１］ 设 Ｓ 是子句集，Ｃ∈Ｓ，Ｃ 在 Ｓ 中是必 需的当且仅当 Ｓ－｛Ｃ｝⊨／ Ｃ。 定理 ２ ［１２］ 设 Ｓ 是子句集，Ｃ∈Ｓ。 Ｃ 在 Ｓ 中是 有用的当且仅当存在 Ｓ 的一个无冗余等价子集 Ｓ′， 使 Ｓ′－｛Ｃ｝⊨／ Ｃ。 定理 ３ ［１２］ 设 Ｓ 是子句集，Ｃ∈Ｓ。 Ｃ 在 Ｓ 中是 无用的当且仅当 Ｓ 的无冗余等价子集恰为 Ｓ－｛Ｃ｝ 的无冗余等价子集。 定理 ４ ［１３］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，且 Ｄ 中不含互补文字。 Ｄ 是 Ｓ 中冗余 子句当且仅当子句集 Ｓ′ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝∪｛Ｄ｝不 可满足。 定义 ５ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，Ｄ＝ ｘ∨Ｄ１ ，其中 ｘ 是一文字，Ｄ１ 是一子 句，如果 Ｄ ∧ Ｃ１ ∧ Ｃ２ ∧ … ∧ Ｃｍ ＝ Ｄ１ ∧ Ｃ１ ∧ Ｃ２ ∧… ∧ Ｃｍ ， 则称 ｘ 是 Ｄ 中关于 Ｓ 的冗余文字。 定理 ５ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中的子句集，Ｄ ＝ ｘ∨Ｄ１ ，如果 Ｄ１ 是 Ｓ′ ＝ ｛Ｃ１ ，Ｃ２ ， …，Ｃｍ ，Ｄ１ ｝中的冗余子句，则 ｘ 是 Ｄ 中关于 Ｓ 的冗 余文字。 定理 ６ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，Ｄ＝ ｘ∨Ｄ１ ，ｘ 是 Ｄ 中关于 Ｓ 的冗余文字 当且仅当 Ｄ１ 是子句集 Ｓ′ ＝ ｛Ｄ１ ，ｘ，Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝中 的冗余子句。 定理 ７ ［１２］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，且 Ｄ 中不含互补文字。 Ｄ 是 Ｓ 中冗余 子句当且仅当子句集 Ｓ′ ＝ ｛Ｃ１ －Ｄ，Ｃ２ －Ｄ，…，Ｃｍ －Ｄ｝ 不可满足。 对于子句集 Ｓ，令 Ｓ ｜ ｘ ＝ ｛Ｃ ｜ Ｃ∈Ｓ 且｛ ｘ，¬ ｘ｝∩ Ｃ ＝∅｝ ∪ ｛ Ｃ ＼ ｛ ¬ ｘ｝ ｜ Ｃ ∈ Ｓ 且 ¬ ｘ ∈ Ｃ｝， Ｓ ｜ Ａ ＝ （…（（Ｓ ｜ ｘ１ ） ｜ ｘ２ ）… ｜ ｘｎ ），其中Ａ ＝ ｛ｘ１ ，ｘ２ ，…，ｘｎ ｝。 定理 ８ ［１３］ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ，Ｄ｝是命题逻 辑中子句集，子句集 Ｓ ′ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝ ∪｛Ｄ｝ 不 可满足当且仅当子句集（Ｓ ＼｛Ｄ｝） ｜ Ｄ不可满足。 ２ 子句集中文字的分类 定义 ６ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 的子句集，如果对于 Ｓ 中的任一子句 Ｃｉ，若有 Ｃｉ ＝ ｘ∨Ｄｉ（ｉ∈｛１，２，…，ｍ｝），其中 ｘ 是一文字，Ｄｉ 是一 子句，且 ｘ 不是 Ｃｉ 中关于 Ｓ 的冗余文字，则称 ｘ 是 Ｓ 中的必需文字。 定义 ７ 设 Ｓ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｍ ｝是命题逻辑中 第 ５ 期 邓鹏，等：命题逻辑的子句集中文字的分类 ·７３７·