6月20日上午，来自卡内基梅隆大学的高思存博士为我们做了题为“判定算法与模型分析”的报告。
      高思存博士首先大致介绍了逻辑学各分支在计算机科学中的应用状况，证明论方面主要是类型论和范畴论，应用于计算机程序设计方面，模型论方面主要包括一阶模型论、模态模型论，模态模型论主要用于传统的模型检测，表达能力比较弱，很多工程问题无法用其解决。一阶整数理论如皮亚诺算术是不可判定的，一阶实数理论如特征为零的实闭域理论，塔斯基在上世纪五十年代证明是可判定的，也就是说，只带加法和乘法的实数理论是可判定的，其判定算法虽经反复改进，但被证明其计算复杂性的下界仍然是双指数级的，所以也不可能直接实际应用，更严重的是，如果加进去三角函数，则立即变得不可判定了，因为利用三角函数可以很容易的定义出整数来。高思存博士在其博士论文中发展了一种逼近策略，引进了某种极小误差界内的delta转化，证明任一实数域公式phi，要么phi是不可满足的，要么phi的某个delta变种phi’是可判定的，phi’处于phi的一个很小的误差震荡界内，所以对实际应用来说是可以接受的，而且其判定算法可以非常迅速。给定任一实际工程问题，如保障某车两地间的平稳运行问题等等，可以首先借助自动机理论对其进行建模，然后高思存博士试图借助这种判定算法，给出一种统一的方式将其转化成可直接执行的程序，这意味着很多复杂动力系统或控制理论的问题都可以统一解决，剩下的就只是针对具体的工程问题进行形式建模了，这可以将人的工作减到最低。
      总之，可以看出，对实数域上的判定算法的研究，必将在很多工程领域，如航空航天、生物医药、机器人控制等领域起着至关重要的作用，有着广泛的应用前景。