计算机科学 ›› 2020, Vol. 47 ›› Issue (11A): 83-85.doi: 10.11896/jsjkx.200400072
唐雷明1, 白沐尘2, 何星星1, 黎兴玉1
TANG Lei-ming1, BAI Mu-chen2, HE Xing-xing1, LI Xing-yu1
摘要: 归结是自动推理中简洁、可靠且完备的推理规则。标准矛盾体分离规则是归结原理的一个重要延拓。基于命题逻辑的标准矛盾体分离演绎推理,对标准矛盾体的性质进行进一步研究,提出了两类特殊标准矛盾体——完全标准矛盾体和最小标准矛盾体,得到了相应的性质和定理。这些性质定理主要描述了:1)各类标准矛盾体的本质特征;2)完全标准矛盾体中添加子句后另添加文字的策略及子句非扩充性的变化规律;3)完全标准矛盾体添加子句及相关文字后,其最小标准矛盾体呈现出的规律;4)最小标准矛盾体可扩充为完全标准矛盾体。这些结论使完全标准矛盾体与最小标准矛盾体能通过添加新子句或相关文字完成互相转换。这一性质为标准矛盾体演绎理论进一步应用于计算机求解提供了一定的理论支撑。
中图分类号:
[1] ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of theAcm,1965,12(1):23-41. [2] HARRISON J.Handbook of practical logic and automated reasoning[M].New York:Cambridge University Press,2009:631-667. [3] PLAISTED D A.History and Prospects for First-Order Automated Deduction[C]//International Conference on Automated Deduction.Springer Verlag,2015,9195:3-28. [4] ROBINSON J A.Handbook of Automated Reasoning[M].New York:MIT Press,2001. [5] BURESH-OPPENHEIM J,PITASSI T.The Complexity ofResolution Refinements[J].Journal of Symbolic Logic,2007,72(4):1336-1352. [6] CHANG C L,RICHARD C T.Symbolic Logic and MechanicalTheorem Proving[M].New York:Academic Press,1973. [7] RUBIN N,HARRISON M C.Another Generalization of Resolution[J].Journal of the ACM(JACM),1978,25(3):341-351. [8] REGER G,SUDA M,VORONKOV A,et al.Selecting the selection[C]//The 8th International Joint Conference on Automated Reasoning(IJCAR2016).Coimbra,Portugal,2016:313-329. [9] SCHULZ S,MOHRMANN M.Performance of clause selection heuristics for saturation-based theorem proving[C]//The 8th International Joint Conference on Automated Reasoning(IJCAR2016).2016:330-345. [10] SUTCLIFFE G.The TPTP problem library and associated infrastructure:the FOF and CNF parts,v2.10.0[J].Journal of Automated Reasoning,2009,43(4):337-362. [11] KALISZYK C,SCHULZ S,URBAN J,et al.System Descrip-tion:E.T.0.1[C]//Proceedings of the 25th International Conference on AutomatedDeduction(CADE-25).Berlin:Springer International Publishing,2015:389-398. [12] GOZNY J,PALEO B W.Towards the compression of first-order resolution proofs by lowering unit clauses[C]//Automated Deduction(CADE-25).Berlin:Springer International Publishing,2015:356-366. [13] XU Y,LIU J,CHEN S W,et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462:93-113. [14] CAO F,XU Y,CHEN S W,et al.Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J].Chinese Journal of Southwest Jiaotong University,2020,55(2):401-408. [15] CAO F,XU Y,WU G F,et al.Application of multi-clause dynamic deduction in Prover9[J].Chinese Computer Engineering &Science,2019,41(9):1686-1692. |
[1] | 李洁, 钟小梅. 命题逻辑中三元子句集的冗余文字 Redundant Literals of Ternary Clause Sets in Propositional Logic 计算机科学, 2022, 49(6A): 109-112. https://doi.org/10.11896/jsjkx.210700036 |
[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. |
|