计算机科学 ›› 2024, Vol. 51 ›› Issue (1): 295-300.doi: 10.11896/jsjkx.230600009
臧珲1, 何星星1, 王成龙1, 李莹芳2, 李天瑞3
ZANG Hui1, HE Xingxing1, WANG Chenglong1, LI Yingfang2, LI Tianrui3
摘要： 归结原理是自动推理中一种简洁、可靠且完备的推理规则,标准矛盾体分离演绎理论是二元归结的一个延拓。矛盾体的结构非常复杂,现有的矛盾体种类和生成策略较少。针对该问题,文中基于命题逻辑的标准矛盾体分离演绎理论,首先通过复合两个或多个正则标准矛盾体,得到了生成新矛盾体的多个复合策略;其次,提出了一类特殊标准矛盾体结构——复合正则标准矛盾体,丰富了矛盾体的结构特征;然后讨论了复合得到的新矛盾体不同子句的可扩充性,进而得到相应的文字添加策略;最后,提出了矛盾体的生成算法,为进一步在计算机上实现新矛盾体的生成提供了参考。
中图分类号:
| [1]NICK.A Brief History of Artificial Intelligence[J].ScienceWriting,2018,1(3):96. [2]ROBINSON J A.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of the ACM(JACM),1965,12(1):23-41. [3]HERBRAND J.Researches in the theory of demonstration[C]//From Frege to Goedel:a source book in Mathematical Logic,Hoard University Press.1930:525-581. [4]BECKERT B,HAHNLE R.Reasoning and verification:State of the art and current trends[J].IEEE Intelligent System,2014,29(1):20-29. [5]WITHERELL P,KRISHNAMURTY S,GROSSE I R,et al.Improved knowledge management through first-order logic in engineering design ontologies[J].Artificial Intelligence for Engineering Design Analysis & Manufacturing,2010,24(2):245-257. [6]WANG Z,YAN S,WANG H,et al.An overview of microsoft deep qa system on stanford web questions benchmark[R].Microsoft Research,2014. [7]LIEBIG T.Reasoning with OWL-system support and insights [M].Germany:Springer Berlin Heidelberg,2013. [8]MARIA F,LUC D R,WOLFGANG B.Artificial Intelligence in a historical perspective[J].AI Communications,2014,27(1):87-102. [9]CEZARY K,JOSEF U.MizAR 40 for Mizar 40[J].Journal of Automated Reasoning,2015,55(3):245-256. [10]CEZARY K,JOSEF U.Learning-Assisted Automated Reaso-ning with Flyspeck[J].Journal of Automated Reasoning,2014,53(2):173- 213. [11]WOS L,ROBINSON G A,CARSON D F.Efficiency and Completeness of the Set of Support Strategy in Theorem Proving[J].Journal of the ACM,1965,12(4):536-541. [12]SLAGLE J R.Automatic theorem proving with renamable and semantic resolution[J].Journal of the ACM,1983,14(4):687-697. [13]LOVELAND D W.A linear format for resolution[C]//Procee-dings of Symposium on Automatic Demonstration.1970:163-190. [14]BOYER R S.Locking:A Restriction of Resolution(Disserta-tion),also ATP-05[M].University of Texas at Austin,1971. [15]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. [16]TANG L M,BAI M C,HE X X,et al.Complete contradiction and smallest contradiction based on propositional logic[J].Computer Science,2020,47(S2):83-85,105. [17]LI X Y,HE X X,MA X,et al.A new method of generating contradictions in propositional logic[J].Computer-Engineering & Science,2023,45(6):1134-1140. [18]LIU X H.Automatic Reasoning Based on the Reduced Method[M].Beijing:Science Press,1994. [19]XU Y,LIU J,CHEN S,et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462:93-113. [20]HE X X,LI Y F,FENG Y H.On structures of regular standardcontradictions in propositional logic[J].Information Sciences,2022,586:261-278. |
|
||
首页