封面新闻记者从西南交通大学了解到，继7月13日在第21届国际SAT竞赛上获得亚军之后，日前，在英国牛津大学刚刚结束的第23届国际自动定理证明器竞赛 (ATP System Competition, CASC-J9)中，该校数学学院系统可信性自动验证国家地方联合工程实验室徐扬教授团队提交的一阶逻辑自动定理证明器获得FOF(First Order Formula )组亚军，填补了中国在该领域的空白。
国际CASC竞赛到底有多牛？据了解，该比赛是自动定理证明器领域的最顶级赛事，至今已举办了23届。本届CASC竞赛首次有来自中国的证明器——西南交通大学的证明器参与，并与英国曼彻斯特大学、德国斯图加特DHBW大学、美国爱荷华州大学等学校的13个证明器进行激烈比拼。
自动定理是逻辑学、数学和计算机科学的交叉学科，是人工智能领域重要研究方向之一。
自动定理看起来高深，其实是逻辑学、数学和计算机科学的一个交叉学科，是人工智能领域重要的研究方向之一，主要研究如何让计算机具备符号演算和演绎推理能力。而一阶逻辑是逻辑系统领域最基本、应用最广泛的逻辑系统。
封面新闻记者了解到，西南交大徐扬教授团队在基于逻辑的自动演绎推理相关领域研究多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法，从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法，是自动演绎推理领域的一个重大突破。基于该理论、方法已经研发了100多个一阶逻辑自动定理证明器（这次参赛的自动定理证明器是其中之一），用这些自动定理证明器已证明25.5万多个来自于国际标准问题库 TPTP 及 Mizar 的一阶逻辑表示的定理（包括152个Rating为1——即难度系数最高、国际上其它所有证明器均未能证明的定理），其中有一个定理的证明过程用CPU时间34.36秒，形成文件9.083MB，如用A4纸打印出来有9762页。这些定理涉及数学分析、代数学、拓扑学、范畴论、组合数学、几何学、数论、逻辑学、规划、计算理论、管理科学、程序验证、集成电路验证、协议验证等方面。
来源：封面新闻7月18日https://m.thecover.cn/news_details.html?from=iosapp&id=950924
