提出一种新算法,让机器推理更高效地发现矛盾。
Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
- 用三角几何框架统一多种矛盾构建方法
- 在多个标准测试集上表现优异,超越传统方法
- 适合研究逻辑推理与自动定理证明的学者
自动化推理是人工智能的核心,支撑定理证明、形式化验证和逻辑推理。尽管多年发展,推理完备性与计算效率的平衡仍是难题。传统基于二元归结的方法仅支持两式交互,限制了多式协同。2018年提出的矛盾分离扩展(CSE)框架首次提出动态多式推理理论,将推理视为矛盾分离过程。但其算法实现长期未正式发布。本文提出扩展三角法(ETM),一个广义的矛盾构造算法,形式化并拓展了矛盾分离机制。ETM在三角几何框架下统一多种矛盾构建策略,包括早期的标准扩展法,支持灵活的子句交互与动态协同。该算法作为核心被应用于多个高性能定理证明器(CSE、CSE-E、CSI-E、CSI-Enig),在标准一阶基准测试(TPTP问题集及CASC 2018–2015)中取得竞争性成果,实证验证了方法的有效性与普适性。通过连接理论抽象与实际实现,ETM推动矛盾分离范式走向通用、可扩展且具备实用竞争力的自动化推理模型,为未来逻辑推理研究提供新方向。
原文摘要 · Abstract (English)
Automated deduction lies at the core of Artificial Intelligence (AI), underpinning theorem proving, formal verification, and logical reasoning. Despite decades of progress, reconciling deductive completeness with computational efficiency remains an enduring challenge. Traditional reasoning calculi, grounded in binary resolution, restrict inference to pairwise clause interactions and thereby limit deductive synergy among multiple clauses. The Contradiction Separation Extension (CSE) framework, introduced in 2018, proposed a dynamic multi-clause reasoning theory that redefined logical inference as a process of contradiction separation rather than sequential resolution. While that work established the theoretical foundation, its algorithmic realization remained unformalized and unpublished. This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation. The ETM unifies multiple contradiction-building strategies, including the earlier Standard Extension method, within a triangular geometric framework that supports flexible clause interaction and dynamic synergy. ETM serves as the algorithmic core of several high-performance theorem provers, CSE, CSE-E, CSI-E, and CSI-Enig, whose competitive results in standard first-order benchmarks (TPTP problem sets and CASC 2018-2015) empirically validate the effectiveness and generality of the proposed approach. By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning, offering new directions for future research in logical inference and theorem proving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。