2021年7月15日，在网上举办的第28届国际自动演绎会议(28th International Conference on Automated Deduction )组委会公布了2021年度国际自动定理证明（Automated Theorem Proving）竞赛结果，我校金沙威尼斯欢乐娱人城系统可信性自动验证国家地方联合工程实验室徐扬教授团队取得好成绩，刘沛瑶、曹锋、陈树伟、曾国艳等人研发的一阶逻辑自动定理证明器“CSE-E 1.3”进入竞争最激烈的FOF组前三强获得第三名。
自动定理证明是人工智能领域既经典又前沿的研究方向之一，涉及数学、逻辑学、计算机科学等领域，广泛应用于自然科学、技术科学、社会科学等领域，特别是数学定理的证明与发现。自动定理证明器属基础性工具，具有重要的科学与应用价值。
国际自动定理证明竞赛是国际上自动演绎推理领域的最顶级赛事，自1996年以来每年举办一次。本次赛事设有: THF、FOF、FNT、UEQ、SLH、LTB、TNE、TEQ、FNE、FEQ、FNN、FNQ、UEQ、SLH 和JJT组，其中金沙威尼斯欢乐娱人城参加的FOF组有16个证明器参赛，是竞争最激烈的一组。参赛国家或单位包括：中国金沙威尼斯欢乐娱人城，美国爱荷华大学（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/
