文章快速检索  
  高级检索
命题逻辑的子句集中文字的分类
邓鹏1,2, 徐扬1,2    
1. 西南交通大学 数学学院, 四川 成都 611756;
2. 西南交通大学 智能控制开发中心, 四川 成都 610031
基金项目: 国家自然科学基金资助项目(61175055,61305074);四川省科技支撑计划资助项目(2011FZ0051).    
摘要: 检测和消除命题逻辑公式中的冗余文字,是人工智能领域广泛研究的基本问题。针对命题逻辑的子句集中子句的划分,结合冗余子句和冗余文字的概念,将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字3类,并分别给出其定义。讨论3种文字与无冗余等价子集的性质,给出其等价子集的等价描述方法。得到题逻辑的子句集中必需文字、有用文字和无用文字的判定方法,借助子句集的可满足性得到3种文字与子句集的可满足性的等价条件。上述结果对命题逻辑中文字属性的判断提供了多种可选择方法,同时为命题逻辑公式的化简奠定了理论基础。
关键词: 命题逻辑     子句集     冗余子句     冗余文字     可满足性    
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, Southwest Jiaotong University, Chengdu 610031, China
Abstract: The detection and elimination of redundant clauses from prepositional logic formulas is a fundamental issue 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 categories: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 equivalent 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.
Key words: propositional logic     set of clauses     redundant clause     redundant character     satisfiability    

在人工智能领域,知识表示的方式多种多样,子句形式仍不失为一种重要的知识表达方式。子句表示广泛应用于机器定理证明、专家系统和知识库等领域。在一个知识库中,如果有部分知识可以删除并且不减少整个知识库携带的信息,那么称这个知识库是冗余的。冗余以及与其密切相关的化简已经成为具有重要现实意义的问题。命题逻辑中子句由文字的析取组成,因此能够对其中的文字进行科学合理的分类对研究冗余文字和冗余子句很有必要,这些理论为归结自动推理奠定了基础。

逻辑公式的化简是计算机科学和人工智能领域重要的研究方向。逻辑上的冗余问题已被许多学者广泛研究[1, 2, 3, 4],包括不同计算问题的复杂性的刻画。其中,主要包括冗余性在实际可满足性求解中的重要作用的研究[5, 6, 7, 8, 9, 10, 11]。 P.Liberatore[1]对命题逻辑中的子句集进行了分类,给出了冗余子句的一些等价条件和性质。翟翠红等[12]研究了命题逻辑中的冗余子句和冗余文字,讨论了子句集的无冗余等价子集。唐世辉[13]研究了命题逻辑中子句集的冗余性,将命题逻辑中子句分为绝对冗余、相对冗余和无冗余3类。因此,本文主要深入研究命题逻辑的子句集中文字的特征,将命题逻辑的子句集中的文字划分为有用文字、必需文字和无用文字,讨论3种文字的关系。最后得到有用文字、必需文字和无用文字的判定方法,为命题逻辑公式的化简提供理论支撑。

1 预备知识

在命题逻辑公式中,称原子公式及其否定叫做文字,有限多个文字的析取叫子句,只含有一个文字的子句称为单子句。

定义1[14]  设A(p1,p2,…,pm)∈F(S),则当A具有形式(Q11Q12∨…∨Q1n)∧…∧(Qm1Qm2∨…∨Qmn)时,称A为合取范式(conjunction normal form,CNF),这里Qij=pjQijpj (j=1,2,…,n;i=1,2,…,m)。

定义2[15]  设S={C1,C2,…,Cm,D}是命题逻辑中的子句集。显然,DS中的冗余子句,当且仅当C1C2∧…∧CmDC1C2∧…∧Cm

一个子句是冗余的,暗示此子句可以从子句集中删除,不会影响子句集所要表示的信息。同理,一个子句集是冗余的,可以定义为它和它的一个真子集等价。

定义3[1]  子句集S是冗余的,当且仅当存在S′S,使S′=S

在命题逻辑中,此定义和如下说法是等价的:

1)存在S′S,使S′S

2)S中含有冗余子句。

定义4[1]  设S是子句集,CS

1)称CS中是必需的(necessary),如果对于S的任一无冗余等价子集S′,有CS′

2)称CS中是有用的(useful),如果存在S的一个无冗余等价子集S′,使CS′

3)称C在S中是无用的(useless),如果对于S的任一无冗余等价子集S′,有CS′。

定理1[1]   设S是子句集,CSCS中是必需的当且仅当S-{C}⊭C

定理2[12]   设S是子句集,CSCS中是有用的当且仅当存在S的一个无冗余等价子集S′,使S′-{C}⊭C

定理3[12]   设S是子句集,CSCS中是无用的当且仅当S的无冗余等价子集恰为S-{C}的无冗余等价子集。

定理4[13]   设S={C1,C2,…,Cm,D}是命题逻辑中子句集,且D中不含互补文字。D是S中冗余子句当且仅当子句集S′={C1,C2,…,Cm}∪不可满足。

定义5[12]   设S={C1,C2,…,Cm,D}是命题逻辑中子句集,D=xD1,其中x是一文字,D1是一子句,如果DC1C2∧…∧Cm=D1C1C2∧…∧Cm,则称xD中关于S的冗余文字。

定理5[12]   设S={C1,C2,…,Cm,D}是命题逻辑中的子句集,D=xD1,如果D1S′={C1,C2,…,Cm,D1}中的冗余子句,则xD中关于S的冗余文字。

定理6[12]   设S={C1,C2,…,Cm,D}是命题逻辑中子句集,D=xD1xD中关于S的冗余文字当且仅当D1是子句集S′={D1,x,C1,C2,…,Cm}中的冗余子句。

定理7[12]   设S={C1,C2,…,Cm,D}是命题逻辑中子句集,且D中不含互补文字。DS中冗余子句当且仅当子句集S′={C1-D,C2-D,…,Cm-D}不可满足。

对于子句集S,令S|x={C|CS且{xx}∩C∅}∪{C\{¬x}|CS且¬xC},S|A=(…((S|x1)|x2)…|xn),其中A={x1,x2,…,xn}。

定理8[13]   设S={C1,C2,…,Cm,D}是命题逻辑中子句集,子句集S′={C1,C2,…,Cm}∪不可满足当且仅当子句集(S\{D})|不可满足。

2 子句集中文字的分类

定义6   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,若有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且x不是Ci中关于S的冗余文字,则称xS中的必需文字。

定义7   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果存在S中的一个子句Ci,若有Ci=xD(i∈{1,2,…,m}),其中x是一文字,D是一子句,且x不是Ci中关于S的冗余文字,则称xS中的有用文字。

定义8   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,若有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且xCi中关于S的冗余文字,则称xS中的无用文字。

从定义6~8可以看出,子句集中的必需文字一定是有用文字,有用文字不一定是必需文字,同时有用和无用是2个相对的概念,子句集中的必需文字一定是非冗余文字,子句集中的无用文字一定是冗余文字。

定理9   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,若有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,xS中的必需文字当且仅当S′i-{Di}⊭DiS′i={Di,x,C1,…,Ci-1,Ci+1,…,Cm}(i∈{1,2,…,m})。

证明   因为xS中的必需文字,所以x一定不是Ci关于S的冗余文字,由定理6知x不是Ci中关于S的冗余文字当且仅当Di不是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}(i∈{1,2,…,m})中的冗余子句,因此DiSi′中是必需的,由定理1知DiSi′中是必需的当且仅当Si′-{Di}⊭Di

推论1   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果存在S中的一个子句Ci,若有Ci=xD(i∈{1,…,m}),其中x是一文字,D是一子句,则xS中的有用文字当且仅当S′-{D}⊭D,其中S′={D,x,C1,…,Ci-1,Ci+1,Cm}。

定理10   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果存在S中的一个子句Ci,若有Ci=xD(i∈{1,2,…,m}),其中x是一文字,D是一子句,则xS中的有用文字当且仅当存在S′的一个无冗余等价子集S″使S″-{D}⊭D,其中S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}。

证明   因为xS中的有用文字,所以x一定不是Ci关于S的冗余文字,由定理6知x不是Ci中关于S的冗余文字当且仅当D不是子句集S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,因此DS′中是有用的,由定理2知DS′中是有用的当且仅当存在S′的一个无冗余等价子集S″使S″-{D}⊭DS′={D,x,C1,…,Ci-1,Ci+1,…,Cm}。

定理11   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,若有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,则称xS中的无用文字当且仅当Si′的无冗余等价子集恰为Si′-{Di}的无冗余等价子集,其中S′i={Di,x,C1,…,Ci-1,Ci+1,…,Cm}(i∈{1,2,…,m})。

证明   因为xS中的无用文字,所以x一定是Ci关于S的冗余文字,由定理6知xCi中关于S的冗余文字当且仅当Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}(i∈{1,…,m})中的冗余子句,因此DiSi′中是无用的,由定理3知DiSi中是无用的当且仅当Si′的无冗余等价子集恰为Si′-{Di}的无冗余等价子集。

3 子句集中文字的判定

根据子句集中文字的分类和冗余子句与子句集的可满足性判定的关系可以得到如下定理。

定理12   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则xS中的无用文字当且仅当子句集{x,C1-Di,…,Ci-1-Di,Ci+1-Di,…,Cm-Di}(i∈{1,2,…,m})不可满足。

证明   若xS中的无用文字,则一定存在CiSCi=xDi,使xCi中关于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=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则xS中的必需文字当且仅当子句集{x,C1-Di,…,Ci-1-Di,Ci+1-Di,…,Cm-Di}(i∈{1,2,…,m})可满足。

证明7   (充分性)若x不是S中的必需文字,则存在CiSCi=xDi,使xCi中关于S的冗余文字,则Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,即DixC1∧…∧Ci-1Ci+1∧…∧Cm=xC1∧…∧Ci-1Ci+1∧…∧Cm。又因为Ci=xDi,所以xDi,即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=xD(i∈{1,2,…,m}),其中x是一文字,D是一子句,则xS中的有用文字当且仅当子句集{x,C1-D,…,Ci-1-D,Ci+1-D,…,Cm-D}可满足。

证明   (充分性)若x不是S中的有用文字,则存在CiSCi=xD,使xCi中关于S的冗余文字,则D是子句集S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,即DxC1∧…∧Ci-1Ci+1∧…∧Cm=xC1∧…∧Ci-1Ci+1∧…∧Cm。又因为Ci=xD,所以xD,于是由定理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=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则xS中的无用文字当且仅当子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪不可满足。

证明   若xS中的无用文字,则一定存在CiSCi=xDi,使xCi中关于S的冗余文字,由定理1.6知xCi中关于S的冗余文字当且仅当Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,于是再由定理4知Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句当且仅当子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪不可满足。

定理16   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,有Ci=xDi(i∈{1,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则xS中的必需文字当且仅当子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪{Di}可满足。

证明   (充分性)若x不是S中的必需文字,则存在CiSCi=xDi,使xCi中关于S的冗余文字,则Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,于是由定理4知子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪不可满足,这显然与已知矛盾。

(必要性)假设子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪不可满足,那么由定理4知Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,则x不是S中的必需文字,矛盾。

定理17   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果存在S中的一个子句Ci,若有Ci=xD(i∈{1,2,…,m}),其中x是一文字,D是一子句,则xS中的有用文字当且仅当子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪可满足。

证明   (充分性)若x不是S中的有用文字,则存在Ci∈S且Ci=x∨D,使x是Ci中关于S的冗余文字,则D是子句集S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,于是由定理4知子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪{D}不可满足,这显然与已知矛盾。

(必要性)假设子句集{x,C1,…,Ci-1,Ci+1,…,Cm}∪不可满足,那么由定理4知D是子句集S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,则x不是S中的有用文字,矛盾。

定理18   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,有Ci=xDi(i∈{1,2,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则xS中的无用文字当且仅当子句集(S′i\{Di})|不可满足,其中Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}。

证明   由于CiSCi=xDixS中的无用文字,由定义知xCi中关于S的冗余文字,所以Di是子句集Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,再由定理4和定理8可以得出充要条件。

定理19   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果对于S中的任一子句Ci,有Ci=xDi(i∈{1,…,m}),其中x是一文字,Di是一子句,且Di中不含互补文字,则x是S中的必需文字当且仅当子句集(Si′\{Di})|可满足,其中Si′={Di,x,C1,…,Ci-1,Ci+1,…,Cm}。

证明   (充分性)由于CiSCi=xDi,假设x不是S中的必需文字,由定义可以知xCi中关于S的冗余文字,所以Di是子句集Si={Di,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,再由定理4和定理8可以得出子句集(Si′\{Di})|不可满足,矛盾。

(必要性)假设(S′i\{Di})|不可满足由定理4和定理8可知x一定是Ci关于S的冗余文字,这与xS中的必需文字矛盾。

定理20   设S={C1,C2,…,Cm}是命题逻辑中的子句集,如果存在S中的一个子句Ci,若有Ci=xD(i∈{1,2,…,m}),其中x是一文字,D是一子句,则xS中的有用文字当且仅当子句集(S′\{D})可满足,其中S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}。

证明   (充分性)由于CiSCi=xD,假设x不是S中的有用文字,由定义知x一定是Ci中关于S的冗余文字,所以D是子句集S′={D,x,C1,…,Ci-1,Ci+1,…,Cm}中的冗余子句,再由定理4和定理8可以得出子句集(S′\{D})|不可满足,矛盾。

(必要性)假设(S′D})|D不可满足由定理4和定理8可知x一定是Ci中关于S的冗余文字,这与xS中的有用文字矛盾。

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 Ⅱ: 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. Eliminating redundant clauses in sat instances[M]// Integration 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 Ⅱ: 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 extension 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 Systems, 2013, 6(5): 943-953.
[12] 翟翠红, 秦克云. 命题逻辑公式中的冗余子句及冗余文字[J]. 计算机科学, 2013, 40(5): 48-50.

ZHAI Cuihong, QIN Keyun. Redundancy clause and redundancy literal of propositional logic[J]. Computer Science, 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 Jiaotong University, 2014: 30-35.
[14] 王国俊. 数理逻辑引论与归结原理[M]. 北京: 科学出版社, 2006: 16-25.

WANG Guojun. Introduction to mathematical logic and resolution principle[M]. Beijing: Science Press, 2006: 16-25.

[15] MUGGLETON S. Inductive logic programming[J]. New Generation Computing, 1991, 8(4): 295-318.
http://dx.doi.org/10.11992/tis.201410005
中国科学技术协会主管、中国测绘地理信息学会主办。
0

文章信息

邓鹏, 徐扬
DENG Peng, XU Yang
命题逻辑的子句集中文字的分类
Classification of the characters in the set of clauses of propositional logic
智能系统学报,2015,10(05):736-740
CAAI Transactions on Intelligent Systems, 2015, 10(05): 736-740.
http://dx.doi.org/10.11992/tis.201410005

文章历史

收稿日期:2014-10-08
网络出版日期: 2015-10-08

相关文章

工作空间