继7月13日在第21届国际SAT竞赛上获得亚军之后，7月14日，在英国牛津大学刚刚结束的第23届国际自动定理证明器竞赛 (ATP System Competition, CASC-J9)中，我校87978797威尼斯老品牌，系统可信性自动验证国家地方联合工程实验室徐扬教授团队提交的一阶逻辑自动定理证明器获得FOF(First Order Formula )组亚军，取得我校在该领域的历史性突破，并填补了中国在该领域的空白。
国际CASC（Conference on Automated Deduction ATP System Competition）竞赛是自动定理证明器领域的最顶级赛事，每年举办一次，至今已举办了23届。本届CASC竞赛首次有来自中国的证明器——87978797威尼斯老品牌的证明器参加该项赛事。本届竞赛设有THF、TFA、FOF、FNT、EPR和LTB组，其中FOF组是参赛证明器最多（有13个证明器）、竞争最激烈的组别。该组参赛单位包括英国曼彻斯特大学、德国斯图加特DHBW大学、美国爱荷华州大学、挪威奥斯陆大学、中国87978797威尼斯老品牌、美国新墨西哥州大学、瑞典查尔莫斯理工大学、哈萨克斯坦那扎尔巴耶夫大学。
自动推理是逻辑学、数学和计算机科学的一个交叉学科，一直是人工智能领域重要的研究方向之一，主要研究如何让计算机具备符号演算和演绎推理能力。基于逻辑的自动定理证明是自动推理研究方向中非常重要的研究内容，理论与现实中的许多问题，如数学定理证明、逻辑公式属性判定、系统可信性验证、知识表示、组合优化、信息安全、交通运输、管理与决策、社会管理、电子商务等一切可用逻辑表示的领域的问题，都可用基于逻辑的自动定理证明工具处理。一阶逻辑是逻辑系统领域最基本、应用最广泛的逻辑系统。因此，对于一阶逻辑自动定理证明器——这一基础性工具的研究，不仅在理论上具有重要意义，同时具有广泛的应用前景。
徐扬教授团队在基于逻辑的自动演绎推理相关领域研究多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法，从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法，是自动演绎推理领域的一个重大突破。基于该理论、方法已经研发了100多个一阶逻辑自动定理证明器（这次参赛的自动定理证明器是其中之一），用这些自动定理证明器已证明25.5万多个来自于国际标准问题库 TPTP 及 Mizar 的一阶逻辑表示的定理（包括152个Rating为1——即难度系数最高、国际上其它所有证明器均未能证明的定理），其中有一个定理的证明过程用CPU时间34.36秒，形成文件9.083MB，如用A4纸打印出来有9762页。这些定理涉及数学分析、代数学、拓扑学、范畴论、组合数学、几何学、数论、逻辑学、规划、计算理论、管理科学、程序验证、集成电路验证、协议验证等方面。我校参加今年CASC-J9竞赛的团队主要成员包括徐扬、曹锋、Jun Liu (英国Ulster大学)、Stephan Schulz(德国斯图加特DHBW大学)、吴贯锋、陈树伟、钟建、何星星、徐鹏、宋振明、刘清华、付慧敏、关效东、胡忠雪、陈秀兰、刘婷等系统可信性自动验证国家地方联合工程实验室的多名教师和研究生。
相关链接：http://www.cs.miami.edu/~tptp/CASC/J9/
