高思存：计算理论中两个困难的逻辑问题

6月10下午我中心全体师生聚集在系一楼会议室，聆听高思存关于计算理论方面的讲座。目前他正在卡内基梅隆理论与应用逻辑专业读博士学位的。该讲座主要为我们简要介绍计算理论中的两个主要问题：1. P/NP问题与有限模型论 (P/NP and Finite Model Theory) 2. 实闭域上一阶理论的量词消解问题 (Efficient Quantifier Elimination for the First-order Theory over Real Closed Fields)。在开始报告之前，周北海教授致欢迎词，很高兴高思存可以抽时间给我们介绍一下他自己目前的工作，以及国外最新的学术动态和热点问题。

报告的第一部分内容是P/NP问 题与有限模型论。高思存首先简单说明什么是有限模型论，并且指出限模型并不像人们原先以为的那样简单，其实是一个很有意思的研究课题。初看来，有限模型是 很简单的，因为任何一个有限模型都可以用一阶逻辑表达式唯一地刻画，对一个确定的基数也只有有限多个不同的有限模型。但实际上在很多方面，有限模型表现出 很特殊的性质。最简单的例子有：紧致性定理在有限模型类上是不可能成立的；通过构造对图灵机的一阶描述，可以证明停机问题可判定当且仅当有限模型类上有效 的一阶语句集是递归集，那么一个容易的推论便是对于有限模型类，不存在能行的一阶公理系统。进一步地，如果把有限模型看做有限图，那么一个一阶逻辑表达式 可以分辨的模型规模与它所含的量词数目呈线性关系。这也就是说大量的关于有限模型的性质是一阶不可定义的，例如奇偶性，连通性等。

接下来，他又介绍二阶逻辑可以对应到P/NP问题。P问题是指确定性的图灵机在多项式时间内可解决的问题；NP问题则是指不确定图灵机在多项式时间内可解决的问题。由Fagin等人的著名结果，只使用二阶存在量词的二阶逻辑（即所谓的existential second order logic）的语句集(ESO)可以完整对应到NP问题类上，相应地只使用二阶全称量词的二阶逻辑（即所谓的universal second order logic）则可对应到coNP类。这样一来，如果可以找到有限模型类分离ESO和USO，则可以分离NP和coNP，进而可以证明P不等于NP。更有意思的是，对于只涵一元谓词的二阶逻辑，这个结论已经被证明，目前集中需要解决的问题便是如何推广到多元谓词上。或许这是一个解决P/NP问题这个关键问题的一个比较有前景的途径。这时也可以发现，理论计算机的问题也可以完全限制在逻辑范围内，解决这个问题不需要了解图灵机问题，而只需要熟悉一阶逻辑和二阶逻辑。这也为我们表明逻辑学在计算机研究中的作用在哪些方面。

报告的第二部分是关于实闭域上一阶逻辑理论的量词消解问题。这个问题是混成系统的模型检测中的核心理论问题，有非常广泛的应用。早在1950年 代塔斯基给出了实闭域上的量词消解算法，进而证明了实数上一阶理论的完全性和可判定性。这一结果在当时的震动很大，因为看起来实数要比自然数复杂，而自然 数上一阶理论的不完全性是人们早已由哥德尔定理接受的事实。但塔斯基最初的算法复杂性过高，只有理论价值。在七十年代出现的CAD算法把复杂度降到了双指数时间内，相应的应用研究也开始开展。但直到现在，该算法的速度与大规模的实际应用仍有很大距离。近期的研究集中引入更多实闭域上的代数几何方法。

另一个在目前非常热门的问题是命题逻辑的可满足性问题，即SAT-solver问题。这个基本上每一年都会有一个竞赛，以推进这一个问题的解决。目前的研究已可以处理数以百万计的命题变元。

这 次报告让我们了解到如何把一个计算中的算法问题转换成逻辑问题，也让我们知道逻辑非常直接和具体的应用。这与非单调逻辑、信念逻辑、认知逻辑等等的研究套 路很不一样。也可以看出来，经典逻辑坐的相当成熟，已经不需要停留在建模上，而是直接关注求解就可以了。高思存回答了在场师生的各类问题，并且进一步介绍 了国内外课程设置方面的不一样，这些对我们进一步的学习和研究都有所启发。在最后，大家以热烈的掌声感谢他所做的报告。

（傅庆芳)