计算机科学 ›› 2022, Vol. 49 ›› Issue (6A): 109-112.doi: 10.11896/jsjkx.210700036
李洁, 钟小梅
LI Jie, ZHONG Xiao-mei
摘要： 自动推理是人工智能领域研究的核心问题之一。由于在基于归结的自动推理过程中会产生大量的冗余文字和冗余子句,进而影响归结自动推理的效率,因此消除子句集中的冗余文字和冗余子句具有重要的意义。在命题逻辑中,依据必需文字、有用文字、无用文字的相关概念和性质,针对部分三元子句集,分类给出这些三元子句集中冗余文字的判别方法,并通过具体实例对这些判别方法进行说明。
中图分类号:
| [1] LIBERATORE P.Redundancy in logic I:CN propositional formulae[J].Artificial Intelligence,2005,163(2):203-232. [2] FOURDRINO Y O,ÉRIC G,MAZURE B.Eliminating Redundant Clauses in SAT Instances[C]//Proceedings of InternationalConference on Integration of Ai and Or Techniques in Constraint Programming for Combinatorial Optimization Problems.DBLP,2007:71-83. [3] HEULE M,M JARVISALO,BIERE A.Efficient CNF simplification based on binary implication graphs[C]//Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing.Springer Berlin Heidelberg,2011. [4] ZHAI C H,QIN K Y.Redundancy clause and redundancy literal of propositional logic[J].Computer Science,2013,40(5):48-50. [5] TANG SH H.Research redundancy of set of clauses in propositional logic[D].Chengdu:Southwest Jiaotong University,2014. [6] DENG P.The classification of set of clauses in propositionallogic[D].Chengdu:Southwest Jiaotong University,2015. [7] RINALDI D,SCHUSTER P,WESSEL D.Eliminating disjunc-tions by disjunction elimination[J].Bulletin of Symbolic Logic,2017,23(2):181-200. [8] LIU T.Research on redundant clauses and redundant literals in propositional logic[D].Chengdu:Southwest Jiaotong Univer-sity,2019. [9] ING X R,XU Y,CHEN Z S.Novel preprocessing clause elimination methods for propositional SAT solvers[J].Computer Integrated Manufacturing Systems,2020,26(8):2133-2142. [10] LIU X H.Automatic reasoning based on resolution method[M].Science Press,1994. [11] SHI CH Y,WANG J X.Mathematical logic and set theory[M].Beijing:Tsinghua University Press,2000. [12] HEULE M,RVISALO M,LONSING F.Clause elimination for SAT and QSAT[J].Journal of Artificial Intelligence Research,2015,53(1):127-168. [13] HEULE M,JRVISALO M,BIERE A.Clause Elimination Pro-cedures for CNF Formulas[C]//Logic for Programming,Artificial Intelligence,& Reasoning-international Conference,Lpar-17.DBLP,2010:357-371. [14] LIU J,ZHOU H H.New algebraic logic reduction method for boolean formula[J].Computer Science,2020,47(5):32-37. [15] WANG G J.Introduction to mathematical logic and resolution principle[M].Science Press,2003:17-22. |
| [1] | 唐雷明, 白沐尘, 何星星, 黎兴玉. 基于命题逻辑的完全标准矛盾体及最小标准矛盾体 Complete Contradiction and Smallest Contradiction Based on Propositional Logic 计算机科学, 2020, 47(11A): 83-85. https://doi.org/10.11896/jsjkx.200400072 |
| [2] | 刘婷, 徐扬, 陈秀兰. 命题逻辑中单元子句及其负文字和冗余子句 Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic 计算机科学, 2019, 46(8): 255-259. https://doi.org/10.11896/j.issn.1002-137X.2019.08.042 |
| [3] | 陈青山, 徐扬, 吴贯锋. 基于趋势强度的SAT问题学习子句评估算法 Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength 计算机科学, 2018, 45(12): 137-141. https://doi.org/10.11896／j.issn.1002-137X.2018.12.021 |
| [4] | 陈成,潘正华,吕永席. 一类具有3种否定的模糊模态命题逻辑 Fuzzy Modal Propositional Logic with Three Kinds of Negation 计算机科学, 2017, 44(4): 263-268. https://doi.org/10.11896/j.issn.1002-137X.2017.04.055 |
| [5] | 徐卫,李晓粉,刘端阳. 基于命题逻辑的关联规则挖掘算法L-Eclat Propositional Logic-based Association-rule Mining Algorithm L-Eclat 计算机科学, 2017, 44(12): 211-215. https://doi.org/10.11896/j.issn.1002-137X.2017.12.038 |
| [6] | 陈青山,徐扬,吴贯锋,何星星. 一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法 Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver 计算机科学, 2017, 44(11): 279-283. https://doi.org/10.11896/j.issn.1002-137X.2017.11.042 |
| [7] | 吴晓刚,潘正华. 基于模糊命题逻辑形式系统FLcom的模糊推理及应用 Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic 计算机科学, 2015, 42(Z11): 100-103. |
| [8] | 刘 熠,徐 扬,贾海瑞. 基于格值命题逻辑系统LP(X)的多元α-归结原理的注记 Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X) 计算机科学, 2015, 42(4): 249-252. https://doi.org/10.11896/j.issn.1002-137X.2015.04.051 |
| [9] | 张家锋，徐扬,何星星. 格值语义归结推理方法 Lattice-valued Semantic Resolution Reasoning Method 计算机科学, 2011, 38(9): 201-203. |
| [10] | 刘宏岚,高庆狮,杨炳儒. 集合代数是经典命题演算形式系统的语义解释 Set Algebra is Semantic Interpretation for Classical Formal System of Propositional Calculus 计算机科学, 2010, 37(9): 194-197. |
| [11] | 谷文祥,赵晓威,殷明浩. 知识编译研究 Knowledge Compilation Survey 计算机科学, 2010, 37(7): 20-26. |
| [12] | 田聪,段振华,王小兵. Einstein谜的SAT求解 Solving Einstein's Puzzle with SAT 计算机科学, 2010, 37(5): 184-186. |
| [13] | . 基于语言真值格值命题逻辑系统lvpl的推理规则 计算机科学, 2008, 35(9): 230-232. |
| [14] | . 纤维逻辑 计算机科学, 2006, 33(1): 1-3. |
| [15] | 季秋 王万森. 发生率计算理论的研究 计算机科学, 2005, 32(4): 79-80. |
|
||
首页