新西兰奥克兰理工大学任教的我系98级逻辑专业系友阮吉老师报告了将模型检测方法应用于信息不完全的全局游戏的工作。他以机器下国际象棋的历史为例介绍了：全局游戏竞赛（General Game Playing Competition）是国际人工智能协会（AAAI）主办的一项旨在测试程序解决全局游戏（general game）问题能力的竞赛。参加竞赛的程序需要在给定了以一种被称为“游戏描述语言”（Game Description Language）的逻辑编程语言描述的游戏规则后，在没有人介入的情况下独立寻找赢得游戏的策略。阮吉老师以圈叉棋（或三连棋，tic-tac-toe）为例具体讲解了以GDL表达的规则描述，以及几种常见的搜索方法。最后，他介绍了将模型检测方法用于检测用GDL给出的这种一般游戏是否满足一定的形式条件，特别是正确性（correctness），其中包括了终结（termination）、可玩性（playability）、可赢性（winnability）。

（撰稿人：万美文）