arXiv:2509.07026cs.LOcs.AI2025-09

提出构建标准矛盾的新方法,提升自动推理系统能力。

Contradictions

  • 基于矛盾分离理论,系统构造两类标准矛盾结构。
  • 给出最大三角形矛盾中嵌套子矛盾数量的计算公式。
  • 为多子句自动推理提供新范式,适合形式化验证研究者。

可信AI需要强大、透明且可靠的推理系统。自动化定理证明(ATP)是形式化推理的核心,但经典二元归结受限于每步仅处理两个子句且最多消除两个文字。2018年提出标准矛盾与基于矛盾分离的演绎理论以突破此瓶颈。本文进一步推进该框架,聚焦标准矛盾的系统构造,研究两种主要形式:最大三角形标准矛盾与三角形类型标准矛盾。基于这些结构,提出通过最大标准矛盾判断子句集可满足性与不可满足性的方法,并推导出在最大三角形与三角形类型标准矛盾中嵌套标准子矛盾数量的计算公式。研究成果为基于矛盾分离的动态多子句自动演绎提供了方法基础,使自动推理系统表达与演绎能力超越经典二元范式。

原文摘要 · Abstract (English)

Trustworthy AI requires reasoning systems that are not only powerful but also transparent and reliable. Automated Theorem Proving (ATP) is central to formal reasoning, yet classical binary resolution remains limited, as each step involves only two clauses and eliminates at most two literals. To overcome this bottleneck, the concept of standard contradiction and the theory of contradiction-separation-based deduction were introduced in 2018. This paper advances that framework by focusing on the systematic construction of standard contradictions. Specially, this study investigates construction methods for two principal forms of standard contradiction: the maximum triangular standard contradiction and the triangular-type standard contradiction. Building on these structures, we propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction. Furthermore, we derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction. The results presented herein furnish the methodological basis for advancing contradiction-separation-based dynamic multi-clause automated deduction, thereby extending the expressive and deductive capabilities of automated reasoning systems beyond the classical binary paradigm.

自动推理逻辑演绎形式验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。