11月21日，《International Journal of Computational Intelligence Systems》（国际计算智能系统杂志）以徐扬、郭海林、陈树伟（西南交通大学数学学院系统可信性自动验证国家地方联合工程实验室）和Jun Liu（英国Ulster大学计算机系）为共同第一作者发表了“Δ1：An Automated Theorem Generator（Δ1：一个自动定理生成器）”。这项最新研究成果——命题逻辑和一阶逻辑自动定理生成器Δ1，是中国西南交通大学和英国Ulster大学在自动定理生成方面合作取得的突破进展。
当给命题逻辑和一阶逻辑自动定理生成器Δ1输入任意多个、任意复杂的逻辑文字或一阶闭公式后，它能自动地直接很快生成海量的、逻辑上有意义的、逻辑上互不等价的非平凡逻辑定理。其逻辑定理的正确性自我确保，不需要任何定理证明器和人工再做验证，且也没有在Δ1内设置自动定理证明器。这样，Δ1直接避开了一阶逻辑Turing Machine停机问题、Church的一阶逻辑定理不可判定性、一阶逻辑子句集不可满足性不可判定性、一阶逻辑不可满足子句集极小性不可判定性、一阶逻辑定理之间等价性不可判定性。
这项成果标志着计算机可以自动快速生成大量的、甚至人类至今还不知道的知识。这是逻辑学、计算机科学和人工智能领域的一项颠覆性突破，为科学指导、引导人类的创新、创造活动，为人类发现、获得新知识提供了一条全新的自动化途径，将对人类的生产生活方式和科学研究与科学探索活动等产生巨大影响。
据该团队介绍，自2025年9月7日以来，他们已分别在国际上公开发布了5个版本不同功能的命题逻辑和一阶逻辑自动定理生成器。他们还将陆续在国际上公开发布系列的命题逻辑和一阶逻辑自动定理生成器。这些自动定理生成器都能像Δ1一样自动、直接、快速生成海量的、互不等价的逻辑上有意义的非平凡逻辑定理，其逻辑定理的正确性都能自我确保，不需要任何定理证明器和人工再做验证，且都没有在系统内设置自动定理证明器。据查，至今在国际上还未发现具有该团队发布的命题逻辑和一阶逻辑自动定理生成器能力的其它自动定理生成系统。
该团队在逻辑学和基于逻辑的自动定理证明与自动定理生成相关领域研究40多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理系列理论与系列方法，提出了标准矛盾体、三角形类标准矛盾体和矩形类标准矛盾体理论、构建方法和应用方案。他们发布的命题逻辑和一阶逻辑自动定理生成器都是标准矛盾体理论与方法的成功应用。
命题逻辑和一阶逻辑自动定理生成器的研发得到了中国西南交通大学数学学院和英国Ulster大学计算机系的大力支持。
