2021年7月15日，在網(wǎng)上舉辦的第28屆國際自動演繹會議(28th International Conference on Automated Deduction )組委會公布了2021年度國際自動定理證明（Automated Theorem Proving）競賽結(jié)果，開云kaiyun開云官方網(wǎng)站系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團(tuán)隊取得好成績，劉沛瑤、曹鋒、陳樹偉、曾國艷等人研發(fā)的一階邏輯自動定理證明器“CSE-E 1.3”進(jìn)入競爭最激烈的FOF組前三強(qiáng)獲得第三名。

  自動定理證明是人工智能領(lǐng)域既經(jīng)典又前沿的研究方向之一，涉及數(shù)學(xué)、邏輯學(xué)、計算機(jī)科學(xué)等領(lǐng)域，廣泛應(yīng)用于自然科學(xué)、技術(shù)科學(xué)、社會科學(xué)等領(lǐng)域，特別是數(shù)學(xué)定理的證明與發(fā)現(xiàn)。自動定理證明器屬基礎(chǔ)性工具，具有重要的科學(xué)與應(yīng)用價值。

  國際自動定理證明競賽是國際上自動演繹推理領(lǐng)域的最頂級賽事，自1996年以來每年舉辦一次。本次賽事設(shè)有: THF、FOF、FNT、UEQ、SLH、LTB、TNE、TEQ、FNE、FEQ、FNN、FNQ、UEQ、SLH 和JJT組，其中kaiyun開云官方網(wǎng)站參加的FOF組有16個證明器參賽，是競爭最激烈的一組。參賽國家或單位包括：中國kaiyun開云官方網(wǎng)站，美國愛荷華大學(xué)（University of Iowa）、佛羅里達(dá)大學(xué)（University of Florida）、Articulate Software、新墨西哥大學(xué)（University of New Mexico），西班牙，德國巴登符騰堡雙元制應(yīng)用技術(shù)大學(xué)（Duale Hochschule Baden-Wuerttemberg)，愛沙尼亞塔林理工大學(xué)（Tallinn University of Technology），英國曼徹斯特大學(xué)大學(xué)（University of Manchester），丹麥奧爾堡大學(xué)(Aalborg University)，瑞典查爾姆斯理工大學(xué)（Chalmers University of Technology），荷蘭阿姆斯特丹自由大學(xué)（Vrije Universiteit Amsterdam）。

  相關(guān)鏈接：

  第28屆國際自動演繹會議主頁：http://www.tptp.org/CASC/28/