繼7月13日在第21屆國際SAT競賽上獲得亞軍之后，7月14日，在英國牛津大學(xué)剛剛結(jié)束的第23屆國際自動定理證明器競賽 (ATP System Competition, CASC-J9)中，開云kaiyun開云官方網(wǎng)站，系統(tǒng)可信性自動驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室徐揚(yáng)教授團(tuán)隊(duì)提交的一階邏輯自動定理證明器獲得FOF(First Order Formula )組亞軍，取得開云在該領(lǐng)域的歷史性突破，并填補(bǔ)了中國在該領(lǐng)域的空白。

國際CASC（Conference on Automated Deduction ATP System Competition）競賽是自動定理證明器領(lǐng)域的最頂級賽事，每年舉辦一次，至今已舉辦了23屆。本屆CASC競賽首次有來自中國的證明器——kaiyun開云官方網(wǎng)站的證明器參加該項(xiàng)賽事。本屆競賽設(shè)有THF、TFA、FOF、FNT、EPR和LTB組，其中FOF組是參賽證明器最多（有13個證明器）、競爭最激烈的組別。該組參賽單位包括英國曼徹斯特大學(xué)、德國斯圖加特DHBW大學(xué)、美國愛荷華州大學(xué)、挪威奧斯陸大學(xué)、中國kaiyun開云官方網(wǎng)站、美國新墨西哥州大學(xué)、瑞典查爾莫斯理工大學(xué)、哈薩克斯坦那扎爾巴耶夫大學(xué)。

自動推理是邏輯學(xué)、數(shù)學(xué)和計(jì)算機(jī)科學(xué)的一個交叉學(xué)科，一直是人工智能領(lǐng)域重要的研究方向之一，主要研究如何讓計(jì)算機(jī)具備符號演算和演繹推理能力?；谶壿嫷淖詣佣ɡ碜C明是自動推理研究方向中非常重要的研究內(nèi)容，理論與現(xiàn)實(shí)中的許多問題，如數(shù)學(xué)定理證明、邏輯公式屬性判定、系統(tǒng)可信性驗(yàn)證、知識表示、組合優(yōu)化、信息安全、交通運(yùn)輸、管理與決策、社會管理、電子商務(wù)等一切可用邏輯表示的領(lǐng)域的問題，都可用基于邏輯的自動定理證明工具處理。一階邏輯是邏輯系統(tǒng)領(lǐng)域最基本、應(yīng)用最廣泛的邏輯系統(tǒng)。因此，對于一階邏輯自動定理證明器——這一基礎(chǔ)性工具的研究，不僅在理論上具有重要意義，同時(shí)具有廣泛的應(yīng)用前景。

徐揚(yáng)教授團(tuán)隊(duì)在基于邏輯的自動演繹推理相關(guān)領(lǐng)域研究多年，原創(chuàng)地提出了基于矛盾體分離的多元、協(xié)同、動態(tài)自動演繹推理理論與方法，從本質(zhì)上突破了現(xiàn)有的一階邏輯自動定理證明器普遍采用的二元、靜態(tài)推理方法，是自動演繹推理領(lǐng)域的一個重大突破?；谠摾碚?、方法已經(jīng)研發(fā)了100多個一階邏輯自動定理證明器（這次參賽的自動定理證明器是其中之一），用這些自動定理證明器已證明25.5萬多個來自于國際標(biāo)準(zhǔn)問題庫 TPTP 及 Mizar 的一階邏輯表示的定理（包括152個Rating為1——即難度系數(shù)最高、國際上其它所有證明器均未能證明的定理），其中有一個定理的證明過程用CPU時(shí)間34.36秒，形成文件9.083MB，如用A4紙打印出來有9762頁。這些定理涉及數(shù)學(xué)分析、代數(shù)學(xué)、拓?fù)鋵W(xué)、范疇論、組合數(shù)學(xué)、幾何學(xué)、數(shù)論、邏輯學(xué)、規(guī)劃、計(jì)算理論、管理科學(xué)、程序驗(yàn)證、集成電路驗(yàn)證、協(xié)議驗(yàn)證等方面。開云參加今年CASC-J9競賽的團(tuán)隊(duì)主要成員包括徐揚(yáng)、曹鋒、Jun Liu (英國Ulster大學(xué))、Stephan Schulz(德國斯圖加特DHBW大學(xué))、吳貫鋒、陳樹偉、鐘建、何星星、徐鵬、宋振明、劉清華、付慧敏、關(guān)效東、胡忠雪、陳秀蘭、劉婷等系統(tǒng)可信性自動驗(yàn)證國家地方聯(lián)合工程實(shí)驗(yàn)室的多名教師和研究生。

相關(guān)鏈接：http://www.cs.miami.edu/~tptp/CASC/J9/