An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
Yang Xu, Peiyao Liu, Shuwei Chen, Jun Liu
目前,缺乏严格的理论体系来系统地产生非平凡和逻辑上有效的定理。 解决这一关键差距,本文进行研究,提出一种新的自动化定理生成理论和工具。 基于具有独特演绎优势的标准矛盾概念,本文首次定义并证明了一种被称为矩形标准矛盾的新逻辑结构。 以这种结构为中心,提出了一个完整的自动理论生成(ATG)理论。 理论证明澄清了矩形标准矛盾的两个核心属性:第一,它是一个标准矛盾(必然不满足);第二,它表现出非冗余(其余条款集在删除任何子句后变得令人满意)。 利用这些属性,本文证明,将一个矩形标准矛盾分割成一个前提子集A,否定其补体H,可以形成有效的定理A ⊢ H,并且所有这些定理在逻辑上是等价的。 为了实现这一理论,设计了一个高效的基于模板的ATG算法,并开发了矩形自动定理生成器。 这项研究使机器能够从“验证者”过渡到“发现者”,为逻辑和人工智能领域的基础研究开辟了新的途径。
Currently, there is a lack of rigorous theoretical system for systematically generating non-trivial and logically valid theorems. Addressing this critical gap, this paper conducts research to propose a novel automated theorem generation theory and tool. Based on the concept of standard contradiction which possesses unique deductive advantages, this paper defines and proves, for the first time, a new logical structure known as rectangular standard contradiction. Centered on this structure, a comp...