基于命题逻辑的完全标准矛盾体及最小标准矛盾体

doi:10.11896/jsjkx.200400072

计算机科学 ›› 2020, Vol. 47 ›› Issue (11A): 83-85.doi: 10.11896/jsjkx.200400072

基于命题逻辑的完全标准矛盾体及最小标准矛盾体

唐雷明¹, 白沐尘², 何星星¹, 黎兴玉¹

1 西南交通大学数学学院成都 611756
2 上海奈胜自动化有限公司上海 200949

出版日期:2020-11-15 发布日期:2020-11-17
通讯作者: 何星星(x.he@home.swjtu.edu.cn)
作者简介:287350507@qq.com
基金资助:
国家自然科学基金项目(61603307,61673320,61473239);教育部人文社科项目(19YJCZH048,20XJCZH016);中央高校基本科研业务费专项资金(JBK2003006);四川省科技计划项目(2020YFG0045,2020YFG0238)

Complete Contradiction and Smallest Contradiction Based on Propositional Logic

TANG Lei-ming¹, BAI Mu-chen², HE Xing-xing¹, LI Xing-yu¹

1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
2 Shanghai Naisheng Automation Co.,LTD,Shanghai 200949,China

Online:2020-11-15 Published:2020-11-17
About author:TANG Lei-ming,born in 1996,master.His main research interests include propositional logic and SAT problem.
HE Xing-xing,born in 1982,Ph.D,associate professor,is a member of China Computer Federation.His main research interests include automated reasoning based on logic and so on.
Supported by:
This work was supported by the National Natural Science Foundation of China (61603307,61673320,61473239),Ministry of Education,Humanities and Social Science Projects(19YJCZH048,20XJCZH016),Fundamental Research Funds for the Central Universities of Ministry of Education of China (JBK2003006) and Science and Technology Project of Sichuan Province,China (2020YFG0045,2020YFG0238).

摘要/Abstract

摘要： 归结是自动推理中简洁、可靠且完备的推理规则。标准矛盾体分离规则是归结原理的一个重要延拓。基于命题逻辑的标准矛盾体分离演绎推理,对标准矛盾体的性质进行进一步研究,提出了两类特殊标准矛盾体——完全标准矛盾体和最小标准矛盾体,得到了相应的性质和定理。这些性质定理主要描述了:1)各类标准矛盾体的本质特征;2)完全标准矛盾体中添加子句后另添加文字的策略及子句非扩充性的变化规律;3)完全标准矛盾体添加子句及相关文字后,其最小标准矛盾体呈现出的规律;4)最小标准矛盾体可扩充为完全标准矛盾体。这些结论使完全标准矛盾体与最小标准矛盾体能通过添加新子句或相关文字完成互相转换。这一性质为标准矛盾体演绎理论进一步应用于计算机求解提供了一定的理论支撑。

关键词: 标准矛盾体, 命题逻辑, 完全标准矛盾体, 最小标准矛盾体

Abstract: Resolution is a simple,reliable and complete reasoning rule in automatic reasoning.Contradiction is an important extension of the principle of resolution.Based on the deductive reasoning of the contradiction of the propositional logic,this paperstu-dies the nature of the contradiction,puts forward the concept of the complete contradiction and the smallest contradiction and gains related properties and theorems.The main contents of these properties and theorems are as follows:1)Characteristics of each special contradiction;2)Strategies for adding literals and non-extended changes of clauses when adding a clause to the complete contradiction;3)The law of the smallest contradiction in the complete contradiction when adding clause and related literals;4)Smallest contradiction can be extended to complete contradiction.These conclusions enable complete contradiction and Smallest contradiction to be converted to each other by adding new clauses or related literals.This property provides a certain theoretical support for the further application of deductive reasoning of contradiction to computer solving.

Key words: Complete contradiction, Contradiction, Propositional logic, Smallest contradiction

中图分类号:

TP181

唐雷明, 白沐尘, 何星星, 黎兴玉. 基于命题逻辑的完全标准矛盾体及最小标准矛盾体[J]. 计算机科学, 2020, 47(11A): 83-85. https://doi.org/10.11896/jsjkx.200400072

TANG Lei-ming, BAI Mu-chen, HE Xing-xing, LI Xing-yu. Complete Contradiction and Smallest Contradiction Based on Propositional Logic[J]. Computer Science, 2020, 47(11A): 83-85. https://doi.org/10.11896/jsjkx.200400072

参考文献

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

相关文章 15

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

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

基于命题逻辑的完全标准矛盾体及最小标准矛盾体

Complete Contradiction and Smallest Contradiction Based on Propositional Logic

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0