命題邏輯的子句集中文字的分類

鄧鵬，徐揚

（1．西南交通大學數學學院，四川成都611756；2．西南交通大學智能控制開發中心，四川成都610031）

命題邏輯的子句集中文字的分類

鄧鵬1，2，徐揚1，2

（1．西南交通大學數學學院，四川成都611756；2．西南交通大學智能控制開發中心，四川成都610031）

檢測和消除命題邏輯公式中的冗余文字，是人工智能領域廣泛研究的基本問題。針對命題邏輯的子句集中子句的劃分，結合冗余子句和冗余文字的概念，將命題邏輯的子句集中的文字分為必需文字、有用文字和無用文字3類，并分別給出其定義。討論3種文字與無冗余等價子集的性質，給出其等價子集的等價描述方法。得到題邏輯的子句集中必需文字、有用文字和無用文字的判定方法，借助子句集的可滿足性得到3種文字與子句集的可滿足性的等價條件。上述結果對命題邏輯中文字屬性的判斷提供了多種可選擇方法，同時為命題邏輯公式的化簡奠定了理論基礎。

命題邏輯；子句集；冗余子句；冗余文字；可滿足性

在人工智能領域，知識表示的方式多種多樣，子句形式仍不失為一種重要的知識表達方式。子句表示廣泛應用于機器定理證明、專家系統和知識庫等領域。在一個知識庫中，如果有部分知識可以刪除并且不減少整個知識庫攜帶的信息，那么稱這個知識庫是冗余的。冗余以及與其密切相關的化簡已經成為具有重要現實意義的問題。命題邏輯中子句由文字的析取組成，因此能夠對其中的文字進行科學合理的分類對研究冗余文字和冗余子句很有必要，這些理論為歸結自動推理奠定了基礎。

邏輯公式的化簡是計算機科學和人工智能領域重要的研究方向。邏輯上的冗余問題已被許多學者廣泛研究［1?4］，包括不同計算問題的復雜性的刻畫。其中，主要包括冗余性在實際可滿足性求解中的重要作用的研究［5?11］。P．Liberatore［1］對命題邏輯中的子句集進行了分類，給出了冗余子句的一些等價條件和性質。翟翠紅等［12］研究了命題邏輯中的冗余子句和冗余文字，討論了子句集的無冗余等價子集。唐世輝［13］研究了命題邏輯中子句集的冗余性，將命題邏輯中子句分為絕對冗余、相對冗余和無冗余3類。因此，本文主要深入研究命題邏輯的子句集中文字的特征，將命題邏輯的子句集中的文字劃分為有用文字、必需文字和無用文字，討論3種文字的關系。最后得到有用文字、必需文字和無用文字的判定方法，為命題邏輯公式的化簡提供理論支撐。

1 預備知識

在命題邏輯公式中，稱原子公式及其否定叫做文字，有限多個文字的析取叫子句，只含有一個文字的子句稱為單子句。

定義1［14］設A（p1，p2，…，pm）∈F（S），則當A具有形式（Q11∨Q12∨…∨Q1n）∧…∧（Qm1∨Qm2∨…∨Qmn）時，稱A為合取范式（conjunction normal form，CNF），這里Qij＝pj或Qij＝?pj（j＝1，2，…，n；i＝1，2，…，m）。

定義2［15］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中的子句集。顯然，D是S中的冗余子句，當且僅當C1∧C2∧…∧Cm∧D≡C1∧C2∧…∧Cm。

一個子句是冗余的，暗示此子句可以從子句集中刪除，不會影響子句集所要表示的信息。同理，一個子句集是冗余的，可以定義為它和它的一個真子集等價。

定義3［1］子句集S是冗余的，當且僅當存在S′?S，使S′＝S。

在命題邏輯中，此定義和如下說法是等價的：

1）存在S′?S，使S′?S；

2）S中含有冗余子句。

定義4［1］設S是子句集，C∈S，

1）稱C在S中是必需的（necessary），如果對于S的任一無冗余等價子集S′，有C∈S′；

2）稱C在S中是有用的（useful），如果存在S的一個無冗余等價子集S′，使C∈S′；

3）稱C在S中是無用的（useless），如果對于S的任一無冗余等價子集S′，有C?S′。

定理1［1］設S是子句集，C∈S，C在S中是必需的當且僅當S－｛C｝?／C。

定理2［12］設S是子句集，C∈S。C在S中是有用的當且僅當存在S的一個無冗余等價子集S′，使S′－｛C｝?／C。

定理3［12］設S是子句集，C∈S。C在S中是無用的當且僅當S的無冗余等價子集恰為S－｛C｝的無冗余等價子集。

定理4［13］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中子句集，且D中不含互補文字。D是S中冗余子句當且僅當子句集不可滿足。

定義5［12］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中子句集，D＝x∨D1，其中x是一文字，D1是一子句，如果D∧C1∧C2∧…∧Cm＝D1∧C1∧C2∧…∧Cm，則稱x是D中關于S的冗余文字。

定理5［12］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中的子句集，D＝x∨D1，如果D1是S′＝｛C1，C2，…，Cm，D1｝中的冗余子句，則x是D中關于S的冗余文字。

定理6［12］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中子句集，D＝x∨D1，x是D中關于S的冗余文字當且僅當D1是子句集S′＝｛D1，x，C1，C2，…，Cm｝中的冗余子句。

定理7［12］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中子句集，且D中不含互補文字。D是S中冗余子句當且僅當子句集S′＝｛C1－D，C2－D，…，Cm－D｝不可滿足。

對于子句集S，令S｜x＝｛C｜C∈S且其中

定理8［13］設S＝｛C1，C2，…，Cm，D｝是命題邏輯中子句集，子句集不可滿足當且僅當子句集可滿足。

2 子句集中文字的分類

定義6 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，若有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且x不是Ci中關于S的冗余文字，則稱x是S中的必需文字。

定義7 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，且x不是Ci中關于S的冗余文字，則稱x是S中的有用文字。

定義8 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，若有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且x是Ci中關于S的冗余文字，則稱x是S中的無用文字。

從定義6～8可以看出，子句集中的必需文字一定是有用文字，有用文字不一定是必需文字，同時有用和無用是2個相對的概念，子句集中的必需文字一定是非冗余文字，子句集中的無用文字一定是冗余文字。

定理9 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，若有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，x是S中的必需文字當且僅當S′i－｛Di｝?／Di，S′i＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝（i∈｛1，2，…，m｝）。

證明 因為x是S中的必需文字，所以x一定不是Ci關于S的冗余文字，由定理6知x不是Ci中關于S的冗余文字當且僅當Di不是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝（i∈｛1，2，…，m｝）中的冗余子句，因此Di在Si′中是必需的，由定理1知Di在Si′中是必需的當且僅當Si′－｛Di｝?／Di。

推論1 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當且僅當S′－｛D｝?／D，其中S′＝｛D，x，C1，…，Ci－1，Ci＋1，Cm｝。

定理10 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當且僅當存在S′的一個無冗余等價子集S″使S″－｛D｝?／D，其中S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝。

證明 因為x是S中的有用文字，所以x一定不是Ci關于S的冗余文字，由定理6知x不是Ci中關于S的冗余文字當且僅當D不是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，因此D在S′中是有用的，由定理2知D在S′中是有用的當且僅當存在S′的一個無冗余等價子集S″使S″－｛D｝?／D，S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝。

定理11 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，若有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，則稱x是S中的無用文字當且僅當Si′的無冗余等價子集恰為Si′－｛Di｝的無冗余等價子集，其中S′i＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝（i∈｛1，2，…，m｝）。

證明 因為x是S中的無用文字，所以x一定是Ci關于S的冗余文字，由定理6知x是Ci中關于S的冗余文字當且僅當Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝（i∈｛1，…，m｝）中的冗余子句，因此Di在Si′中是無用的，由定理3知Di在Si中是無用的當且僅當Si′的無冗余等價子集恰為Si′－｛Di｝的無冗余等價子集。

3 子句集中文字的判定

根據子句集中文字的分類和冗余子句與子句集的可滿足性判定的關系可以得到如下定理。

定理12 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的無用文字當且僅當子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝（i∈｛1，2，…，m｝）不可滿足。

證明 若x是S中的無用文字，則一定存在Ci∈S且Ci＝x∨Di，使x是Ci中關于S的冗余文字，則Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，于是由定理7知Di是子句集Si′＝｛Di，x，C1…，Ci－1，Ci＋1，…，Cm｝中的冗余子句當且僅當子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝不可滿足。

定理13 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的必需文字當且僅當子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝（i∈｛1，2，…，m｝）可滿足。

證明7 （充分性）若x不是S中的必需文字，則存在Ci∈S且Ci＝x∨Di，使x是Ci中關于S的冗余文字，則Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，即Di∧x∧C1∧…∧Ci－1∧Ci＋1∧…∧Cm＝x∧C1∧…∧Ci－1∧Ci＋1∧…∧Cm。又因為Ci＝x∨Di，所以x?Di，即x－Di＝x。于是由定理7知子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝（i∈｛1，2，…，m｝）不可滿足，矛盾。

（必要性）假設子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝不可滿足，由定理7知Di是子句集Si′＝｛Di，x，Ci，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，則x不是S中的必需文字，矛盾。

定理14 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當且僅當子句集｛x，C1－D，…，Ci－1－D，Ci＋1－D，…，Cm－D｝可滿足。

證明 （充分性）若x不是S中的有用文字，則存在Ci∈S且Ci＝x∨D，使x是Ci中關于S的冗余文字，則D是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，即D∧x∧C1∧…∧Ci－1∧Ci＋1∧…∧Cm＝x∧C1∧…∧Ci－1∧Ci＋1∧…∧Cm。又因為Ci＝x∨D，所以x?D，于是由定理7知子句集｛x，C1－D，…，Ci－1－D，Ci＋1－D，…，Cm－D｝不可滿足，矛盾。

（必要性）假設子句集｛x，C1－D，…，Ci－1－D，Ci＋1－D，…，Cm－D｝不可滿足，由定理7知D是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，則x不是S中的有用文字，矛盾。

定理15 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的無用文字當且僅當子句集｛x，C1，…，Ci－1，Ci＋1，…，Cm｝∪不可滿足。

證明 若x是S中的無用文字，則一定存在Ci∈S且Ci＝x∨Di，使x是Ci中關于S的冗余文字，由定理1．6知x是Ci中關于S的冗余文字當且僅當Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，于是再由定理4知Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句當且僅當子句集不可滿足。

定理16 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的必需文字當且僅當子句集可滿足。

證明 （充分性）若x不是S中的必需文字，則存在Ci∈S且Ci＝x∨Di，使x是Ci中關于S的冗余文字，則Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，于是由定理4知子句集｛x，不可滿足，這顯然與已知矛盾。

（必要性）假設子句集｛x，C1，…，Ci－1，Ci＋1，…，不可滿足，那么由定理4知Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，則x不是S中的必需文字，矛盾。

定理17 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當且僅當子句集｛x，C1，可滿足。

證明 （充分性）若x不是S中的有用文字，則存在Ci∈S且Ci＝x∨D，使x是Ci中關于S的冗余文字，則D是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，于是由定理4知子句集｛x，C1，不可滿足，這顯然與已知矛盾。

（必要性）假設子句集｛x，C1，…，Ci－1，Ci＋1，…，不可滿足，那么由定理4知D是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，則x不是S中的有用文字，矛盾。

定理18 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的無用文字當且僅當子句集可滿足，其中Si′＝僅當子句集可滿足，其中Si′＝｛Di，x， C1，…，Ci－1，Ci＋1，…，Cm｝。

證明 （充分性）由于Ci∈S，Ci＝x∨Di，假設x不是S中的必需文字，由定義可以知x是Ci中關于S的冗余文字，所以Di是子句集S′i＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，再由定理4和定理

證明 由于Ci∈S且Ci＝x∨Di，x是S中的無用文字，由定義知x是Ci中關于S的冗余文字，所以Di是子句集Si′＝｛Di，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，再由定理4和定理8可以得出充要條件。

定理19 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補文字，則x是S中的必需文字當且

定理20 設S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當且僅當子句集可滿足，其中S′＝｛D，x，C1，…，Ci－1， Ci＋1，…，Cm｝。

證明 （充分性）由于Ci∈S，Ci＝x∨D，假設x不是S中的有用文字，由定義知x一定是Ci中關于S的冗余文字，所以D是子句集S′＝｛D，x，C1，…，Ci－1，Ci＋1，…，Cm｝中的冗余子句，再由定理4和定理8可以得出子句集不可滿足，矛盾。

4 結束語

本文主要研究命題邏輯的子句集中必需文字、有用文字和無用文字的特征，討論它們相應的等價條件。然后運用冗余文字和冗余子句的知識，得到必需文字、有用文字和無用文字與子句集可滿足性的判定方法。該方法豐富了命題邏輯的子句集中文字的分類方法，得到子句集中文字特征的判定方法，為命題邏輯公式的化簡奠定了理論基礎。但是目前的冗余文字判定方法對子句集中文字屬性的判斷處理過程比較復雜，下一步將繼續深入研究子句集的分類，為命題邏輯中子句集的化簡和高效的歸結自動推理提供理論支撐。

［1］LIBERATORE P．Redundancy in logic I：CNF propositional formulae［J］．Artificial Intelligence，2005，163（2）：203?232．

［2］LIBERATORE P．Redundancy in logic II：2CNF and Horn propositional formulae［J］．Artificial Intelligence，2008，172（2／3）：265?299．

［3］BOUFKHAD Y，ROUSSEL O．Redundancy in random SAT formulas［C］／／Proceedings of the 7th National Conference on Artificial Intelligence．［S．l．］，2000：273?278．

［4］FOURDRINOY O，GRéGOIRE é，MAZURE B，et al．E?liminating redundant clauses in sat instances［M］／／Integra?tion of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems．Berlin／Heidelberg：Springer，2007：71?83．

［5］KULLMANN O．Constraint satisfaction problems in clausal form II：Minimal unsatisability and conict structure［J］．Fundamenta Informaticae，2011，109（1）：83?119．［6］MANTHEY N．Coprocessor 2．0—A flexible CNF simplifier［J］．Theory and Applications of Satisfiability Testing－SAT，2012，7317：436?441．

［7］BELOV A，JANOTA M，LYNCE I，et al．On computing minimal equivalent subformulas［J］．Principles and Practice of Constraint Programming，2012，7514：158?174．

［8］張建．邏輯公式的可滿足性判定——方法、工具及應用［M］．北京：科學出版社，2000：22?30．

［9］許有軍．基于擴展規則的若干SAT問題研究［D］．長春：吉林大學，2011：15?28．XU Youjun．Research on several SAT issues based on exten?sion rule［D］．Changchun，China：Jilin University，2011：15?28．

［10］CHANG C L，LEE R C T．Symbolic logic and mechanical theorem proving［M］．New York：Academic Press，1973：19?73，22?25．

［11］LIU Yi，JIA Hairui，XU Yang．Determination of 3?Ary α?resolution in lattice?valued propositional logic LP（X）［J］．International Journal of Computational Intelligence Sys?tems，2013，6（5）：943?953．

［12］翟翠紅，秦克云．命題邏輯公式中的冗余子句及冗余文字［J］．計算機科學，2013，40（5）：48?50．ZHAI Cuihong，QIN Keyun．Redundancy clause and re?dundancy literal of propositional logic［J］．Computer Sci?ence，2013，40（5）：48?50．

［13］唐世輝．命題邏輯中子句集的冗余性研究［D］．成都：西南交通大學，2014：30?35．TANG Shihui．Research redundancy of set of clauses in propositional logic［D］．Chengdu，China：Southwest Jiao?tong University，2014：30?35．

［14］王國俊．數理邏輯引論與歸結原理［M］．北京：科學出版社，2006：16?25．WANG Guojun．Introduction to mathematical logic and res?olution principle［M］．Beijing：Science Press，2006：16?25．

［15］MUGGLETON S．Inductive logic programming［J］．New Generation Computing，1991，8（4）：295?318．

Classification of the characters in the set of clauses of propositional logic

DENG Peng1，2，XU Yang1，2

（1．School of Mathematics，Southwest Jiaotong University，Chengdu 611756，China；2．Intelligent Control Development Center，South?west Jiaotong University，Chengdu 610031，China）

The detection and elimination of redundant clauses from prepositional logic formulas is a fundamental is?sue that has been widely researched in artificial intelligence（AI）．The concept for division in the set of clauses of propositional logic is combined with the concepts of redundant clause and redundant character so as to research the classification of the characters in the set of clauses of propositional logic．The characters are classified into three cat?egories：necessary characters，useful characters，and useless characters，and thereby definitions of them are given，respectively．The property of three kinds of characters and irredundant equivalent subsets is discussed，some equiv?alent descriptions of these three kinds of characters and non?redundant equivalent subsets are given respectively．The judging method for these three kinds of characters in the set of clauses of propositional logic is obtained，and by virtue of the satisfiability of the set of clauses，the equivalent conditions of satisfiability for these three kinds of characters and the set of clauses are derived．These results provide a variety of alternative methods for judging the attributes of the characters of the set of clauses in propositional logic，laying a theoretical foundation for simplifying propositional logic formulas．

propositional logic；set of clauses；redundant clause；redundant character；satisfiability

TH186

A

1673?4785（2015）05?0736?05

10．11992／tis．201410005

http：／／www．cnki．net／kcms／detail／23．1538．tp．20151008．1000．006．html

鄧鵬，徐揚．命題邏輯的子句集中文字的分類［J］．智能系統學報，2015，10（5）：736?740．

英文引用格式：DENG Peng，XU Yang．Classification of the characters in the set of clauses of propositional logic［J］．CAAI Transac?tions on Intelligent Systems，2015，10（5）：736?740．

鄧鵬，男，1989年生，碩士研究生，主要研究方向為邏輯與推理。

徐揚，男，1956年生，教授，博士生導師，主要研究方向為邏輯代數、代數邏輯、不確定性推理和自動推理。

2014?10?08．

日期：2015?10?08．

國家自然科學基金資助項目（61175055，61305074）；四川省科技支撐計劃資助項目（2011FZ0051）．

鄧鵬．E?mail：dengpengswjtu＠163．com．