鄧鵬，徐揚(yáng)

（1．西南交通大學(xué)數(shù)學(xué)學(xué)院，四川成都611756；2．西南交通大學(xué)智能控制開發(fā)中心，四川成都610031）

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

鄧鵬1，2，徐揚(yáng)1，2

（1．西南交通大學(xué)數(shù)學(xué)學(xué)院，四川成都611756；2．西南交通大學(xué)智能控制開發(fā)中心，四川成都610031）

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

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

在人工智能領(lǐng)域，知識(shí)表示的方式多種多樣，子句形式仍不失為一種重要的知識(shí)表達(dá)方式。子句表示廣泛應(yīng)用于機(jī)器定理證明、專家系統(tǒng)和知識(shí)庫等領(lǐng)域。在一個(gè)知識(shí)庫中，如果有部分知識(shí)可以刪除并且不減少整個(gè)知識(shí)庫攜帶的信息，那么稱這個(gè)知識(shí)庫是冗余的。冗余以及與其密切相關(guān)的化簡已經(jīng)成為具有重要現(xiàn)實(shí)意義的問題。命題邏輯中子句由文字的析取組成，因此能夠?qū)ζ渲械奈淖诌M(jìn)行科學(xué)合理的分類對(duì)研究冗余文字和冗余子句很有必要，這些理論為歸結(jié)自動(dòng)推理奠定了基礎(chǔ)。

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

1 預(yù)備知識(shí)

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

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

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

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

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

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

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

2）S中含有冗余子句。

定義4［1］設(shè)S是子句集，C∈S，

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

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

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

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

定理2［12］設(shè)S是子句集，C∈S。C在S中是有用的當(dāng)且僅當(dāng)存在S的一個(gè)無冗余等價(jià)子集S′，使S′－｛C｝?／C。

定理3［12］設(shè)S是子句集，C∈S。C在S中是無用的當(dāng)且僅當(dāng)S的無冗余等價(jià)子集恰為S－｛C｝的無冗余等價(jià)子集。

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

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

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

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

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

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

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

2 子句集中文字的分類

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

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

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

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

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

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

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

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

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

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

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

3 子句集中文字的判定

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

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

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

定理13 設(shè)S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對(duì)于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補(bǔ)文字，則x是S中的必需文字當(dāng)且僅當(dāng)子句集｛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中關(guān)于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。又因?yàn)镃i＝x∨Di，所以x?Di，即x－Di＝x。于是由定理7知子句集｛x，C1－Di，…，Ci－1－Di，Ci＋1－Di，…，Cm－Di｝（i∈｛1，2，…，m｝）不可滿足，矛盾。

（必要性）假設(shè)子句集｛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 設(shè)S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果存在S中的一個(gè)子句Ci，若有Ci＝x∨D（i∈｛1，2，…，m｝），其中x是一文字，D是一子句，則x是S中的有用文字當(dāng)且僅當(dāng)子句集｛x，C1－D，…，Ci－1－D，Ci＋1－D，…，Cm－D｝可滿足。

證明 （充分性）若x不是S中的有用文字，則存在Ci∈S且Ci＝x∨D，使x是Ci中關(guān)于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。又因?yàn)镃i＝x∨D，所以x?D，于是由定理7知子句集｛x，C1－D，…，Ci－1－D，Ci＋1－D，…，Cm－D｝不可滿足，矛盾。

（必要性）假設(shè)子句集｛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 設(shè)S＝｛C1，C2，…，Cm｝是命題邏輯中的子句集，如果對(duì)于S中的任一子句Ci，有Ci＝x∨Di（i∈｛1，2，…，m｝），其中x是一文字，Di是一子句，且Di中不含互補(bǔ)文字，則x是S中的無用文字當(dāng)且僅當(dāng)子句集｛x，C1，…，Ci－1，Ci＋1，…，Cm｝∪不可滿足。

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

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

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

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

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

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

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

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

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

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

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

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

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

4 結(jié)束語

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

［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］張建．邏輯公式的可滿足性判定——方法、工具及應(yīng)用［M］．北京：科學(xué)出版社，2000：22?30．

［9］許有軍．基于擴(kuò)展規(guī)則的若干SAT問題研究［D］．長春：吉林大學(xué)，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］．計(jì)算機(jī)科學(xué)，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］．成都：西南交通大學(xué)，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］王國俊．?dāng)?shù)理邏輯引論與歸結(jié)原理［M］．北京：科學(xué)出版社，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

鄧鵬，徐揚(yáng)．命題邏輯的子句集中文字的分類［J］．智能系統(tǒng)學(xué)報(bào)，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年生，碩士研究生，主要研究方向?yàn)檫壿嬇c推理。

徐揚(yáng)，男，1956年生，教授，博士生導(dǎo)師，主要研究方向?yàn)檫壿嫶鷶?shù)、代數(shù)邏輯、不確定性推理和自動(dòng)推理。

2014?10?08．

日期：2015?10?08．

國家自然科學(xué)基金資助項(xiàng)目（61175055，61305074）；四川省科技支撐計(jì)劃資助項(xiàng)目（2011FZ0051）．

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