arXiv 人工智能· Yang Xu, Shuwei Chen, Hailin Guo, Jun Liu·· 1 日前AI スコア35
基于三角标准矛盾的一阶逻辑自动定理生成
Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions
未翻訳のため中国語で表示しています。
AI ガイド
研究者提出一种基于三角标准矛盾的一阶逻辑自动定理生成（ATG）构造性框架，通过构建极小不可满足子句集，实现定理无需独立证明即可“构造即正确”。该研究在已有 $\Delta_1$ 生成器基础上拓展出 $\Delta_2$ 至 $\Delta_8$ 等 7 种方法，构建了包含 8 种方法的生成体系，并已开源发布 $\Delta_1$ 至 $\Delta_4$ 四个生成器。
出典：arXiv 人工智能 · arxiv.org