基于机器学习分类算法的前提选择技术研究

摘要

前提选择是提高定理自动证明成功率的关键技术,可以根据证明目标的相关性选择最有可能成功证明当前猜想的引理.已有的前提选择算法推荐的引理相关度不高,无法进一步提高定理的自动证明能力.针对以上问题,文章提出一种基于机器学习分类算法的组合方案,从公式结构和符号之间的依赖关系出发,提取有效特征向量集,并在k-近邻算法和朴素贝叶斯算法的基础上引入LDA主题词提取技术,进一步捕捉符号和依赖项之间的相关性,使得最后的组合算法预测的准确性更高.实验结果表明,该方案推荐的引理比现有的前提选择算法相关性更高,可以有效提高定理自动证明的成功率.