计算机科学

计算机科学 ›› 2025, Vol. 52 ›› Issue (12): 200-208.doi: 10.11896/jsjkx.250200060

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

一阶逻辑中一类多线型标准矛盾体的结构

曾丹1, 何星星1, 李莹芳2, 李天瑞3   

  1. 1 西南交通大学数学学院 成都 611756
    2 西南财经大学计算机与人工智能学院 成都 611130
    3 西南交通大学计算机与人工智能学院 成都 611756
  • 收稿日期:2025-02-17 修回日期:2025-05-06 出版日期:2025-12-15 发布日期:2025-12-09
  • 通讯作者: 李莹芳(liyf@swufe.edu.cn)
  • 作者简介:(2654596400@qq.com)
  • 基金资助:
    国家自然科学基金(12102369);中央高校基本科研业务费专项资金(2682024ZTPY041);四川省科技计划项目(2024YFHZ031);成都市科技项目(2023-RK00-00080-ZF)

Structures of Multi-line Standard Contradictions in First-order Logic

ZENG Dan1, HE Xingxing1, LI Yingfang2, LI Tianrui3   

  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 School of Computing and Artificial Intelligence, Southwest Jiaotong University, Chengdu 611756, China
  • Received:2025-02-17 Revised:2025-05-06 Published:2025-12-15 Online:2025-12-09
  • About author:ZENG Dan,born in 1999,master.Her main research interests include standard contradiction and graph auto-encoder.
    LI Yingfang,born in 1985,Ph.D,asso-ciate professor.Her main research in-terests include processing,intelligent decision making and control,measurement and analysis of uncertain information,reasoning and problem solving.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China(12102369),Fundamental Research Funds for the Central Universities (2682024ZTPY041),Science and Technology Support Project of Sichuan Province (2024YFHZ031) and Science and Technology Project Supported by Chengdu Government(2023-RK00-00080-ZF).

PDF (PC)

14

摘要： 自动推理是人工智能的重要研究领域,推理规则是影响其效率的关键因素。基于矛盾体分离的演绎推理是一种可靠且完备的推理规则,具有多文字、多子句协同和动态演绎等优势。矛盾体构造方法对演绎效率至关重要。基于此,提出基于命题逻辑一类矛盾体结构——多线型标准矛盾体,给出此类矛盾体在不同情况下的复合策略,即利用两个多线型标准矛盾体生成新的标准矛盾体的条件与方法,并对复合性质上的共性结论和特性结论进行区分;指出通过向子句添加特定文字,多线型标准矛盾体可以转换为更多条线的标准矛盾体,并给出此类矛盾体的文字添加策略;设计在命题逻辑中生成多线型标准矛盾体的算法;给出双线型矛盾体及完全标准矛盾体基于一阶逻辑的结构与性质。

关键词: 命题逻辑, 一阶逻辑, 标准矛盾体, 多线型标准矛盾体, 复合策略, 文字添加策略

Abstract: Automatic reasoning constitutes a critical research domain in artificial intelligence,where inference rules play a pivotal role in determining its efficiency.Deductive reasoning based on the separation of contradictions represents a reliable and complete inference rule,offering advantages such as multi-literal collaboration,multi-clause integration,and dynamic deduction.The construction method of contradictions significantly impacts the efficiency of deduction.In light of this,this paper first introduces a type of contradiction structure grounded in propositional logic,i.e.,multi-line standard contradictions,and elaborates on the compound strategies for such contradictions under various scenarios.Specifically,it outlines the conditions and methods for generating new standard contradictions by leveraging two multi-line standard contradictions,while distinguishing between common and characteristic conclusions regarding their compound properties.Secondly,the paper highlights that incorporating specific literals into clauses can transform multi-line standard contradictions into more streamlined linear standard contradictions,providing lite-rals addition strategies tailored to such contradictions.Additionally,an algorithm for generating multi-line standard contradictions within propositional logic is designed.Finally,the structure and properties of double-line contradictions and complete standard contradictions based on first-order logic are presented.

Key words: Propositional logic, First-order logic, Standard contradiction, Multi-lines standard contradiction, Composite strategy, Literals addition strategy

中图分类号: 

  • TP181
[1]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.
[2]ROBINSON J A.A machine-Oriented logic based on the resolution principle[J].Journal of the ACM,1965,12(1):23-41.
[3]PLAISTED D A.History and prospects for first-order automated deductionC]// International Conference on Automated Deduction.Springer,2015:3-28.
[4]VORONKOV A.The anatomy of vampire[J].Journal of Automated Reasoning,1995,15(2):237-265.
[5]SCHULZ S.E-a brainiac theorem prover[J].AI Communica-tions,2002,15(2/3):111-126.
[6]KOROVIN K,STICKSEL C.iProver-Eq:An instantiation-based theorem prover with equality[C]//Automated Reasoning:5th International Joint Conference.Berlin:Springer,2010:196-202.
[7]OTTEN J,BIBEL W.leanCoP:lean connection-based theorem proving[J].Journal of Symbolic Computation,2003,36(1/2):139-161.
[8]OTTEN J.Restricting backtracking in connection calculi[J].AI Communications,2010,23:159-182.
[9]WERNHARD C,BIBEL W.Investigations into proof structures[J].Journal of Automated Reasoning,2024,68(4):1-70.
[10]WERNHARD C.Craig interpolation with clausal first-order ta-bleaux[J].Journal of Automated Reasoning,2021,65(5):647-690.
[11]FÄRBER M,KALISZYK C,URBAN J.Machine learning gui-dance for connection tableaux[J].Journal of Automated Reaso-ning,2021,65:287-320.
[12]XU Y,LIU J,CHEN S,et al.Contradiction separation based dynamic multi-clause synergized automated deduction[J].Information Sciences,2018,462:93-113.
[13]CAO F,XU Y,CHEN S,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.
[14]LIU P,CHEN S,LIU J,et al.An efficient contradiction separation based automated deduction algorithm for enhancing reaso-ning capability[J].Knowledge-Based Systems,2023,261:110217.
[15]LIU P,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]SUTCLIFFE G,DESHARNAIS M.The 11th IJCAR automated theorem proving system competition-CASC-J11[J].AI Communications,2023,36(2):73-91.
[17]BENZMÜLLER C,HEULE M J H,SCHMIDT R A.Automated Reasoning:12th International Joint Conference,IJCAR 2024,Nancy,France,July 3-6,2024,Proceedings,Part I[M].Springer Nature,2024.
[18]SUTCLIFFE G,SUTTNER C,KOTTHOFF L,et al.An empi-rical assessment of progress in automated theorem proving[C]//International Joint Conference on Automated Reasoning.Cham:Springer,2024:53-74.
[19]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.
[20]HE X,LI Y,FENG Y.On structures of regular standard contra-dictions in propositional logic[J].Information Sciences,2022,586:261-278.
[21]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.
[22]ZANG H,HE X,WANG C,et al.Construction and compounding of a class of regular standard contradictions in propositional logic[J].Computer Science,2024,51(1):295-300.
[23]WANG C,HE X,ZANG H.Literal chunk contradiction andclause regular contradiction in propositional logic[J].Computer Science,2024,51(7):272-277.
[24]LIU X H.Automatic reasoning based on the reduced method[M].Beijing:Science Press,1994.
[25]XU M.Lectures on symbolic logic[M].Wuhan:Wuhan University Press,2008:252-253.
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
本系统由北京玛格泰克科技发展有限公司设计开发