文章快速检索 高级检索

1. 西南交通大学 数学学院, 四川 成都 611756;
2. 西南交通大学 智能控制开发中心, 四川 成都 610031

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 预备知识

1)存在S′S，使S′S

2)S中含有冗余子句。

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

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

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

2 子句集中文字的分类

3 子句集中文字的判定

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

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

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

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

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

(必要性)假设(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

CAAI Transactions on Intelligent Systems, 2015, 10(05): 736-740.
http://dx.doi.org/10.11992/tis.201410005