计算机科学

计算机科学 ›› 2024, Vol. 51 ›› Issue (7): 272-277.doi: 10.11896/jsjkx.230500237

• 人工智能 • 上一篇    下一篇

命题逻辑中文字块矛盾型及子句正则矛盾体

王成龙1, 何星星1, 臧珲1, 李莹芳2, 王丹琛3, 李天瑞4   

  1. 1 西南交通大学数学学院 成都 611756
    2 西南财经大学计算机与人工智能学院 成都 611130
    3 四川省数字经济研究中心 成都 610021
    4 西南交通大学计算机与人工智能学院 成都 611756
  • 收稿日期:2023-05-31 修回日期:2023-10-12 出版日期:2024-07-15 发布日期:2024-07-10
  • 通讯作者: 李莹芳(liyf@swufe.edu.cn)
  • 作者简介:(1084256157@qq.com)
  • 基金资助:
    中央高校基本科研业务费专项资金(2682020ZT107);国家自然科学基金(62106206);教育部人文社科项目(19YJCZH048,20XJCZH016);四川省科技计划(2023YFH0066)

Literal Chunk Contradiction and Clause Regular Contradiction in Propositional Logic

WANG Chenglong1, HE Xingxing1, ZANG Hui1, LI Yingfang2, WANG Danchen3, LI Tianrui4   

  1. 1 School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China
    2 School of Computing and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China
    3 Sichuan Digital Economy Research Center,Chengdu 610021,China
    4 School of Computing and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China
  • Received:2023-05-31 Revised:2023-10-12 Online:2024-07-15 Published:2024-07-10
  • About author:WANG Chenglong,born in 1999,master.His main research interests include propositional logic and deep learning.
    LI Yingfang,born in 1985,Ph.D,asso-ciate professor.Her main research interests include intelligent information processing,intelligent decision making and control,measurement and analysis of uncertain information,reasoning and problem solving and so on.
  • Supported by:
    Basic Research Funds for Central Universities(2682020ZT107),National Natural Science Foundation of China(62106206),Humanities and Social Sciences Project of Ministry of Education(19YJCZH048,20XJCZH016) and Science and Technology Program of Sichuan Province(2023YFH0066).

PDF (PC)

420

摘要： 归结原理是自动推理中一种简洁、可靠且完备的推理规则。基于矛盾体分离的自动演绎理论是归结原理的延伸,矛盾体是该理论的核心部分。由于矛盾体结构复杂且生成策略较少,因此文中提出了一种新的生成矛盾体的策略,即利用多个标准矛盾体生成文字块矛盾型,再通过添加互补矛盾集得到新的矛盾体。重点讨论了具有特殊结构的文字块矛盾型生成的矛盾体,即子句正则矛盾体的性质,这些性质说明了具有特定结构的子句正则矛盾体添加子句后仍然是矛盾体。最后,提出了矛盾体的生成算法,为在计算机上实现新的矛盾体的生成提供参考。

关键词: 标准矛盾体, 命题逻辑, 文字块矛盾型, 子句正则矛盾体

Abstract: The resolution principle is a concise,reliable,and complete inference rule in automatic reasoning.The contradiction sepa-ration-based dynamic multi-clause synergized automated deduction is an extension of the resolution principle,and the contradiction is the theory's core part.Due to the complex structure of the contradiction and the few generation strategies,a new strategy for generating the contradiction is proposed,i.e.,multiple standard contradictions are used to generate the literal chunk contradiction.Then,a new contradiction is obtained by adding complementary contradiction sets.The focus is on the nature of the contradiction generated by the literal chunk contradiction with a special structure,i.e.,the clause regular contradiction,which shows that the clause regular contradiction with a specific structure is still a contradiction after adding the clause.Finally,an algorithm for generating contradiction is proposed,which provides a reference for generating new contradictions on computers.

Key words: Standard contradiction, Propositional logic, Literal chunk contradiction, Clause regular contradiction

中图分类号: 

  • TP181
[1]BECKERT B,HAHNLE R.Reasoning and verification:State ofthe art and current trends[J].IEEE Intelligent Systems,2014,29(1):20-29.
[2]WITHERELL P,KRISHNAMURTY S,GROSSE I R,et al.Improved knowledge management through first-order logic in engineering design ontologies[J].AI EDAM,2010,24(2):245-257.
[3]WANG Z,YAN S,WANG H,et al.An overview of microsoft deep qa system on stanford webquestions benchmark[J/OL].[2018-09-15].https://www.microsoft.com/en-us/research/publication/an-overview-of-microsoft-deep-qa-system-on-stanford-webquestionsbenchmark,2014.
[4]BIBEL W.Artificial Intelligence in a historical perspective[J].AI Communications,2014,27(1):87-102.
[5]KALISZYK C,URBAN J.Mizar 40 for mizar 40[J].Journal of Automated Reasoning,2015,55(3):245-256.
[6]KALISZYK C,URBAN J.Learning-assisted automated reaso-ning with Flyspeck[J].Journal of Automated Reasoning,2014,53:173-213.
[7]ZOU L,LIU D,ZHENG H L.(α,β)-Generalized Lock Resolution of Intuitionistic Fuzzy Logic[J].Journal of Frontiers of Computer Science and Technology,2015,9(8):1004-1009.
[8]MENG J.Resolution-based Automated Reasoning in Linguistic2-Tuple[D].Liaoning:Liaoning Normal University,2018.
[9]LI X N.The Study of (α,β)-Linear Resolution Method for Intui-tionistic Fuzzy Logic[D].Liaoning:Liaoning normal University,2017.
[10]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.
[11]CAO F,XU Y,LIU J,et al.CSE_E 1.0:Anintegrated automated theorem prover for first-order logic[J].Symmetry,2019,11(9):1142.
[12]CAO F,XU Y,CHEN S W,et al.A contradiction separation dynamic deduction algorithm based on optimized proof search[J].International Journal of Computational Intelligence Systems,2019,12(2):1245-1254.
[13]CAO F,XU Y,LIU J,et al.A multi-clause dynamic deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2021,566:281-299.
[14]ZHONG J,XU Y,CAO F.A Novel Combinational ATP Based on Contradiction Separation for First-Order Logic[J].International Journal of Computational Intelligence Systems,2020,13(1):672-680.
[15]LIU P Y,XU Y,LIU J,et al.Fully reusing clause deduction algorithm based on standard contradiction separation rule[J].Information Sciences,2023,622:337-356.
[16]TANG L M,BAI M C,HE X X,et al.Complete contradictionand smallest contradiction based on propositional logic[J].Computer Science,2020,47(S2):83-85,105.
[17]HE X X,LI Y F,FENG Y F.On structures of regular standard contradictions in propositional logic[J].Information Sciences,2022,586:261-278.
[18]LI X Y,HE X X,MA X,et al.A new contradiction generation method in propositional logic[J].Computer Engineering & Science,2023,45(6):1134-1140.
[19]LIU X H.Automatic Reasoning Based on the Reduced Method[M].Beijing:Science Press,1994.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市渝北区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发