继在第21届国际SAT竞赛上获得亚军之后，在英国牛津大学举行的第23届国际自动定理证明器竞赛 (ATP System Competition, CASC-J9)中，西南交通大学数学学院，系统可信性自动验证国家地方联合工程实验室提交的一阶逻辑自动定理证明器获得FOF(First Order Formula )组亚军，取得我国在该领域的历史性突破，并填补了国内在该领域的空白。

国际CASC（Conference on Automated Deduction ATP System Competition）竞赛是自动定理证明器领域的最顶级赛事，每年举办一次，至今已举办了23届。本届CASC竞赛首次有来自中国的证明器——西南交通大学的证明器参加该项赛事。本届竞赛设有THF、TFA、FOF、FNT、EPR和LTB组，其中FOF组是参赛证明器最多（有13个证明器）、竞争最激烈的组别。该组参赛单位包括英国曼彻斯特大学、德国斯图加特DHBW大学、美国爱荷华州大学、挪威奥斯陆大学、中国西南交通大学、美国新墨西哥州大学、瑞典查尔莫斯理工大学、哈萨克斯坦那扎尔巴耶夫大学。

自动推理是逻辑学、数学和计算机科学的一个交叉学科，一直是人工智能领域重要的研究方向之一，主要研究如何让计算机具备符号演算和演绎推理能力。基于逻辑的自动定理证明是自动推理研究方向中非常重要的研究内容，理论与现实中的许多问题，如数学定理证明、逻辑公式属性判定、系统可信性验证、知识表示、组合优化、信息安全、交通运输、管理与决策、社会管理、电子商务等一切可用逻辑表示的领域的问题，都可用基于逻辑的自动定理证明工具处理。一阶逻辑是逻辑系统领域最基本、应用最广泛的逻辑系统。因此，对于一阶逻辑自动定理证明器——这一基础性工具的研究，不仅在理论上具有重要意义，同时具有广泛的应用前景。