[1]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]
Copy

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

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 10 Number of periods: 2015 5 Page number: 736-740 Column: 学术论文—自然语言处理与理解 Public date: 2015-10-25
Title:
Classification of the characters in the set of clauses of propositional logic
Author(s):
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
Keywords:
propositional logic; set of clauses; redundant clause; redundant character; satisfiability
CLC:
TH186
DOI:
10.11992/tis.201410005
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.
Similar References:

Memo

-

Last Update: 2015-11-16

Copyright © CAAI Transactions on Intelligent Systems