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

First-Order Logical Premise Selection Method Based on Symbol Weight

为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力,首先,提出符号权重计算公式,基于符号在问题中出现的频率获取不同符号对应的权重;其次,提出相关度计算公式,利用分配的符号权重计算问题中前提和结论间的相关度;同时,研究自适应相关度边界,用于判断前提与给定的结论是否相关;最后,在自动定理证明器中交互地结合前提选择和自动推理两个过程,可在充分选择相关前提的情况下及时停止前提选择过程.实验结果表明:在最优情况下,新提出的前提选择方法能够把参与证明的平均前提数量从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.