基于符号权重的一阶逻辑前提选择方法  

First-Order Logical Premise Selection Method Based on Symbol Weight

作　　者：刘清华 李瑞杰 朱绪胜 陈代鑫 LIU Qinghua;LI Ruijie;ZHU Xusheng;CHEN Daixin(Avic Chengdu Aircraft Industrial(Group)Co.Ltd.,Chengdu 610091,China;School of Transportation and Logistics,Southwest Jiaotong University,Chengdu 611756,China)

机构地区：[1]成都飞机工业(集团)有限责任公司,四川成都610091 [2]西南交通大学交通运输与物流学院,四川成都611756

出　　处：《西南交通大学学报》2023年第3期704-710,共7页Journal of Southwest Jiaotong University

基　　金：国家自然科学基金(72101217)。

摘　　要：为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同时,研究自适应相关度边界,用于判断前提与给定的结论是否相关;最后,在自动定理证明器中交互地结合前提选择和自动推理两个过程,可在充分选择相关前提的情况下及时停止前提选择过程.实验结果表明:在最优情况下,新提出的前提选择方法能够把参与证明的平均前提数量从1 876个降低到174个;与广泛使用的前提选择方法 E-SInE和Vampire-SInE相比,使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.To enhance the ability of automated theorem provers to select relevant premises from large-scale premises of first-order logic problems,a symbol weight calculation formula is first proposed,obtaining various weights corresponding to different symbols based on the frequency of symbols in the problem.Secondly,the correlation calculation formula is proposed,using assigned symbol weights to compute the correlation between a premise and the conjecture in a problem.At the same time,the adaptive correlation boundary is studied,which is used to determine whether the premise is correlated with the given conjecture.Finally,both processes of premise selection and automated reasoning are interactively combined in automated theorem provers,achieving the goal of stopping the premise selection process in time when the relevant premises are fully selected.The experimental results show that in the optimal case,the proposed premise selection method can reduce the average number of premises involving in proving process from 1876 to 174,and compared with widely used premise selection methods E-SInE and Vampire-SInE in automated theorem provers,the propoed method can help the automated theorem prover E improve the proof rate by 19.49%and 10.49%respectively on the MPTP2078 benchmark.

关 键 词：前提选择 自动定理证明 一阶逻辑 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]