记者18日从西南交大获悉，在英国牛津大学举办的第23届国际自动定理证明器竞赛(ATPSystemCompetition,CASC-J9)中，西南交大数学学院系统可信性自动验证国家地方联合工程实验室徐扬教授团队提交的一阶逻辑自动定理证明器获得FOF(FirstOrderFormula)组亚军。
据了解，该比赛是自动定理证明器领域的最顶级赛事，至今已举办了23届。本届CASC竞赛首次有来自中国的证明器——西南交通大学的证明器参与，并与英国曼彻斯特大学、德国斯图加特DHBW大学、美国爱荷华州大学等学校的13个证明器进行激烈比拼。
自动推理是逻辑学、数学和计算机科学的一个交叉学科，一直是人工智能领域重要的研究方向之一，主要研究如何让计算机具备符号演算和演绎推理能力。基于逻辑的自动定理证明是自动推理研究方向中非常重要的研究内容，理论与现实中的许多问题，如数学定理证明、逻辑公式属性判定、系统可信性验证、知识表示、组合优化、信息安全、交通运输、管理与决策、社会管理、电子商务等一切可用逻辑表示的领域的问题，都可用基于逻辑的自动定理证明工具处理。
一阶逻辑是逻辑系统领域最基本、应用最广泛的逻辑系统。西南交大徐扬教授团队在基于逻辑的自动演绎推理相关领域研究多年，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法，从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法，是自动演绎推理领域的一个重大突破。(完)
来源：中新网7月18日http://www.sc.chinanews.com/bwbd/2018-07-18/86536.html?qq-pf-to=pcqq.c2c
