基于目标演绎距离的一阶逻辑子句集预处理方法曹锋

一阶逻辑定理证明是人工智能领域的重要基础，研究高效的自动定理证明器及其预算法具备重要学术价值。现有自动定理证明器通常先通过子句集预减少规模，再进行演绎判定。

传统预方法多聚焦于目标子句项符号的相关性，忽略了子句间文字互补对关系对演绎的重要影响。针对这一不足，提出了目标演绎距离概念，用以刻画子句与目标子句之间的演绎关联。

该方法通过冗余子句约简与纯文字删除规则精简原始子句集。随后计算剩余子句中文字和整体对子句的目标演绎距离，基于设定的阈值进一步筛选子句，从而优化预效果。

将该预方法集成到顶尖证明器Vampire中，并以 2017 年国际一阶逻辑自动定理证明竞赛的标准问题集测试。结果表明，优化后的 Vampire4.1 在限定时间内能证明更多定理，尤其弥补了原版本未能证明的部分，提升了证明效率和覆盖率。

这一策略强调预阶段应充分考虑子句间的演绎关系，更有针对性的输入，促进后续演绎过程的性能提升。该研究为一阶逻辑自动定理证明的子句预了新的理论与方法支持。

结合相关领域的研究成果，如一阶逻辑的演绎推理技术及基于格值与稳定度的项评估方法，可进一步丰富预策略。借鉴命题逻辑向一阶逻辑的子句消去技术，有望提升自动证明器复杂逻辑问题的能力。

利用子句集预优化自动定理证明过程，在逻辑推理与人工智能交叉领域具有广阔应用前景。此类方法促进智能系统逻辑推理效率提升，推动人工智能理论及应用的发展。