[1]邓鹏,徐扬.命题逻辑的子句集中文字的分类[J].智能系统学报编辑部,2015,10(5):736-740.[doi:10.11992/tis.201410005]
 DENG Peng,XU Yang.Classification of the characters in the set of clauses of propositional logic[J].CAAI Transactions on Intelligent Systems,2015,10(5):736-740.[doi:10.11992/tis.201410005]
点击复制

命题逻辑的子句集中文字的分类(/HTML)
分享到:

《智能系统学报》编辑部[ISSN:1673-4785/CN:23-1538/TP]

卷:
第10卷
期数:
2015年5期
页码:
736-740
栏目:
出版日期:
2015-10-25

文章信息/Info

Title:
Classification of the characters in the set of clauses of propositional logic
作者:
邓鹏12 徐扬12
1. 西南交通大学 数学学院, 四川 成都 611756;
2. 西南交通大学 智能控制开发中心, 四川 成都 610031
Author(s):
DENG Peng12 XU Yang12
1. School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China;
2. Intelligent Control Development Center, Southwest Jiaotong University, Chengdu 610031, China
关键词:
命题逻辑子句集冗余子句冗余文字可满足性
Keywords:
propositional logicset of clausesredundant clauseredundant charactersatisfiability
分类号:
TH186
DOI:
10.11992/tis.201410005
文献标志码:
A
摘要:
检测和消除命题逻辑公式中的冗余文字,是人工智能领域广泛研究的基本问题。针对命题逻辑的子句集中子句的划分,结合冗余子句和冗余文字的概念,将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字3类,并分别给出其定义。讨论3种文字与无冗余等价子集的性质,给出其等价子集的等价描述方法。得到题逻辑的子句集中必需文字、有用文字和无用文字的判定方法,借助子句集的可满足性得到3种文字与子句集的可满足性的等价条件。上述结果对命题逻辑中文字属性的判断提供了多种可选择方法,同时为命题逻辑公式的化简奠定了理论基础。
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.

参考文献/References:

[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. 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 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 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.

备注/Memo

备注/Memo:
收稿日期:2014-10-08;改回日期:。
基金项目:国家自然科学基金资助项目(61175055,61305074);四川省科技支撑计划资助项目(2011FZ0051).
作者简介:邓鹏,男,1989年生,硕士研究生,主要研究方向为逻辑与推理;徐扬,男,1956年生,教授,博士生导师, 主要研究方向为逻辑代数、代数逻辑、不确定性推理和自动推理。
通讯作者:邓鹏.E-mail:dengpengswjtu@163.com.
更新日期/Last Update: 2015-11-16