我要投搞

标签云

收藏小站

爱尚经典语录、名言、句子、散文、日志、唯美图片

当前位置:王中王 > 定理证明器 >

西南交通大学数学学院徐扬教授团队夺得第23届国际一阶逻辑自动定

归档日期:04-30       文本归类:定理证明器      文章编辑:爱尚语录

  继7月13日在第21届国际SAT竞赛上获得亚军之后,7月14日,在英国牛津大学刚刚结束的第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大学、美国爱荷华州大学、挪威奥斯陆大学、中国西南交通大学、美国新墨西哥州大学、瑞典查尔莫斯理工大学、哈萨克斯坦那扎尔巴耶夫大学。

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

  徐扬教授团队在基于逻辑的自动演绎推理相关领域研究多年,原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法,从本质上突破了现有的一阶逻辑自动定理证明器普遍采用的二元、静态推理方法,是自动演绎推理领域的一个重大突破。基于该理论、方法已经研发了100多个一阶逻辑自动定理证明器(这次参赛的自动定理证明器是其中之一),用这些自动定理证明器已证明25.5万多个来自于国际标准问题库 TPTP 及 Mizar 的一阶逻辑表示的定理(包括152个Rating为1——即难度系数最高、国际上其它所有证明器均未能证明的定理),其中有一个定理的证明过程用CPU时间34.36秒,形成文件9.083MB,如用A4纸打印出来有9762页。这些定理涉及数学分析、代数学、拓扑学、范畴论、组合数学、几何学、数论、逻辑学、规划、计算理论、管理科学、程序验证、集成电路验证、协议验证等方面。西南交通大学参加今年CASC-J9竞赛的团队主要成员包括徐扬、曹锋、Jun Liu (英国Ulster大学)、Stephan Schulz(德国斯图加特DHBW大学)、吴贯锋、陈树伟、钟建、何星星、徐鹏、宋振明、刘清华、付慧敏、关效东、胡忠雪、陈秀兰、刘婷等系统可信性自动验证国家地方联合工程实验室的多名教师和研究生。(通讯员:杨育鸿 周伟)

  曲阜师范大学新增列2个山东省一流学科 一流学科建设总数位居省属高校第三

  白城师范学院教师在吉林省第三届高校就业创业优秀论文征文评比活动中喜获佳绩

  四川省高校第二十六届新入职教师职业技能培训暨高校新任教师职业素养提升机制改革试点启动大会在四川师范大学召开

  中山大学南方学院商学院第四学生党支部被命为广东省高校学习型、服务型、创新型党支部

  常州机电职业技术学院龙狮队在江苏省第十九届省运会高校部比赛中取得优异成绩

  笃学笃行 致真致远湛江幼儿师范专科学校校训

  齐鲁师范学院组织开展山东省委统战部2018年“同心光彩助学行动”

本文链接:http://brazil-run.com/dinglizhengmingqi/207.html