互补比子句选择算法

破解44道级难题

面向一阶逻辑自动推理的子句选择策略，可集成至现有主流证明器并显著提升其性能。

Guoyan, Zeng · 陈树伟 · Liu, Jun · 徐扬 · Peiyao, Liu

Knowledge-Based Systems 2024

参数信息

破解难题数

44

技术优势

能破解其他系统无法解决的难题

集成新算法后，证明器能够解决44道评级为1的问题，这些问题是其他现有系统无法处理的。

提升主流系统性能

在CASC 2020–2022竞赛中，新算法提高了E和Vampire系统的性能。

无需重新设计底层引擎

该算法可以作为模块部署在现有的最佳一阶自动推理系统之上，而无需改动其核心设计。

应用场景

• 自动定理证明：将新策略集成到现有证明器中，增强复杂问题的求解能力。
• 形式化验证：通过更强的一阶推理能力，加速软件和硬件验证任务。
• AI推理引擎：为推理引擎提供更高效的子句选择机制，提高整体推理效率。
• 逻辑推理系统：优化逻辑推理系统中的多子句矛盾分离过程，提升自动演绎性能。