arXiv · AI· Yang Xu, Shuwei Chen, Hailin Guo, Jun Liu·· 7 小时前AI 评分24
基于三角标准矛盾的一阶逻辑自动定理生成构造框架
Automated Theorem Generation in First-Order Logic by Construction from Triangular Standard Contradictions
AI 导读
提出基于三角标准矛盾的自动化定理生成（ATG）构造框架，确保定理正确性无需单独证明。 方法从不可满足子句集构建定理，引入七种方法 $\Delta_2$–$\Delta_8$ 形成八方法统一族，已实现并发布前四种生成器。 该框架为自动化定理发现提供原则性基础，支持逻辑保证的知识构建。
来源：arXiv · AI · arxiv.org