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

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

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

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

相關鏈接：http://www.cs.miami.edu/~tptp/CASC/J9/