2025年7月28日10时7分（英国当地时间），我院系统可信性自动验证国家地方联合工程实验室徐扬教授团队在自动定理生成器领域取得突破性进展，该团队核心成员徐扬、郭海林、陈树伟和Jun Liu（英国Ulster大学）联合研发出一个命题逻辑和一阶逻辑自动定理生成器Δ1。当给Δ1输入一些逻辑文字后，它能很快生成大量（甚至难以计数）的不同逻辑定理。其逻辑定理的正确性不需要任何定理证明器和人工再做验证，Δ1中也没有内设自动定理证明器。这些逻辑定理可广泛应用于自然科学和社会科学各个领域。这表明机器可以自动产生大量的、甚至人类至今还不知道的知识。这将对人类的生产生活方式和科学研究与科学探索活动等产生巨大影响。据查，在国际上还未发现具有命题逻辑和一阶逻辑自动定理生成器Δ1能力的其它自动定理生成器。
徐扬教授团队在基于逻辑的自动定理证明与自动定理生成相关领域研究40多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理系列理论与系列方法，提出了标准矛盾体、三角形类标准矛盾体和矩形类标准矛盾体理论及其构建方法。本次发布的命题逻辑和一阶逻辑自动定理生成器Δ1是三角形标准矛盾体理论与方法的成功应用。
该命题逻辑和一阶逻辑自动定理生成器Δ1的成功发布得到了中国做爱直播
和英国Ulster大学计算机系的大力支持，特别得到了包括Chris Nugent（英国Ulster大学）、何星星、钟小梅、曹锋、刘沛瑶、曾国艳、吴贯锋、徐鹏、钟建、朱曼瑶、王恪铭、宋振明、李志辉、杨晗、潘小东、李天瑞、徐革、黄祥、黎定仕、杨洋、任鹏、关效东、严光银等国内外学者、师生及系统可信性自动验证国家地方联合工程实验室所有教师和历届研究生的特别关心与大力支持。
自动定理生成器Δ1可从GitHub网站//github.com/SWJTU-math/Automated_Theorem_Generator下载，免费使用。非常欢迎大家使用、并提出宝贵意见和建议。
