西南交通大学新闻中心主办
发布时间:2018-07-18  来源:未知  作者:admin
继7月13日在第21届国际SAT比赛上取得亚军之后,7月14日,在英国牛津大学刚停止的第23届国际自动定理证实器竞赛 (ATPSystem Competition, CASCJ9)中,我校数学学院,体系可托性自动验证国度处所结合工程试验室徐扬教学团队提交的一阶逻辑主动定理证明器失掉FOF(First Order Formula )组亚军,获得我校在该范畴的历史性冲破,并弥补了中国在该领域的空缺。


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


自动推理是逻辑学、数学和计算机科学的一个穿插学科,始终是人工智能领域重要的研究方向之一,主要研究如何让计算机具备符号演算和演绎推理才能。基于逻辑的自动定理证明是自动推理研究方向中十分主要的研究内容,理论与事实中的很多问题,如数学定理证明、逻辑公式属性断定、系统可信性验证、常识表示、组合优化、信息保险、交通运输、管理与决议、社会管理、电子商务等所有可用逻辑表示的领域的问题,都可用基于逻辑的自动定理证明工具处置。一阶逻辑是逻辑系统领域最基础、利用最广泛的逻辑系统。因而,对一阶逻辑自动定理证明器??这一基本性工具的研究,不仅在理论上具备重要意思,同时存在普遍的运用远景。


徐扬传授团队在基于逻辑的自动演绎推理相关领域研究多年,原创地提出了基于抵触体分别的多元、协同、动态自动演绎推理理论与办法,从实质上突破了现有的一阶逻辑自动定理证明器广泛采取的二元、静态推理方式,是自动演绎推理领域的一个重大打破。基于该实践、方法已经研发了100多个一阶逻辑自动定理证明器(这次参赛的自动定理证明器是其中之一),用这些自动定理证明器已证明25.5万多个来自于国际尺度问题库 TPTP 及 Mizar 的一阶逻辑表现的定理(包括152个Rating为1??即难度系数最高、国际上其它所有证明器均未能证明的定理),其中有一个定理的证明进程用CPU时光34.36秒,构成文件9.083MB,如用A4纸打印出来有9762页。这些定理波及数学剖析、代数学、拓扑学、范围论、组合数学、多少何学、数论、逻辑学、计划、盘算理论、治理迷信、程序验证、集成电路验证、协定验证等方面。我校加入今年CASCJ9竞赛的团队重要成员包含徐扬、曹锋、Jun Liu (英国Ulster大学)、Stephan Schulz(德国斯图加特DHBW大学)、吴贯锋、陈树伟、钟建、何星星、徐鹏、宋振明、刘清华、付慧敏、关效东、胡忠雪、陈秀兰、刘婷等系统可信性自动验证国家地方联合工程实验室的多名老师跟研讨生。






相干链接:cs.miami.edu/~tptp/CASC/J9/


上一篇:聪明反被聪明误 违法停车 竟被记12分
下一篇:没有了