2021年7月15日，在網(wǎng)上舉辦的第28屆國際自動演繹會議(28th International Conference on Automated Deduction )組委會公布了2021年度國際自動定理證明（Automated Theorem Proving）競賽結果，開云kaiyun開云官方網(wǎng)站系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊取得好成績，劉沛瑤、曹鋒、陳樹偉、曾國艷等人研發(fā)的一階邏輯自動定理證明器“CSE-E 1.3”進入競爭最激烈的FOF組前三強獲得第三名。
自動定理證明是人工智能領域既經(jīng)典又前沿的研究方向之一，涉及數(shù)學、邏輯學、計算機科學等領域，廣泛應用于自然科學、技術科學、社會科學等領域，特別是數(shù)學定理的證明與發(fā)現(xiàn)。自動定理證明器屬基礎性工具，具有重要的科學與應用價值。
國際自動定理證明競賽是國際上自動演繹推理領域的最頂級賽事，自1996年以來每年舉辦一次。本次賽事設有: THF、FOF、FNT、UEQ、SLH、LTB、TNE、TEQ、FNE、FEQ、FNN、FNQ、UEQ、SLH 和JJT組，其中kaiyun開云官方網(wǎng)站參加的FOF組有16個證明器參賽，是競爭最激烈的一組。參賽國家或單位包括：中國kaiyun開云官方網(wǎng)站，美國愛荷華大學（University of Iowa）、佛羅里達大學（University of Florida）、Articulate Software、新墨西哥大學（University of New Mexico），西班牙，德國巴登符騰堡雙元制應用技術大學（Duale Hochschule Baden-Wuerttemberg)，愛沙尼亞塔林理工大學（Tallinn University of Technology），英國曼徹斯特大學大學（University of Manchester），丹麥奧爾堡大學(Aalborg University)，瑞典查爾姆斯理工大學（Chalmers University of Technology），荷蘭阿姆斯特丹自由大學（Vrije Universiteit Amsterdam）。
相關鏈接：
第28屆國際自動演繹會議主頁：http://www.tptp.org/CASC/28/
