arXiv · cs.AI · Yang Xu, Shuwei Chen, Hailin Guo, Jun Liu · 12 小时前模型评分34
基于三角标准矛盾构造的一阶逻辑自动定理生成框架
Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions
导读
研究者提出一种一阶逻辑自动定理生成（ATG，Automated Theorem Generation）的构造式框架，从选定文字构造极小不可满足子句集，再以保留子句为前提、取某子句或子句合取的否定为结论，使定理在构造时即正确、无需逐条证明。该工作扩展此前的 Δ1 生成器，新增 Δ2–Δ8 共七种方法，形成八种方法的统一家族，其中 Δ1–Δ4 已实现并发布。组合分析显示该框架可系统生成大量不同定理。
分类置信度
中 · 待人工复核
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
应用领域：科学研究
事件类型：研究发布
证据摘录
- “We propose a constructive framework for ATG in first-order logic based on triangular standard contradictions.”
- “Four generators, $\Delta_1$--$\Delta_4$, have been implemented and released.”
来源：arXiv · cs.AI · arxiv.org