ACM通信
技术视角:寻求多项式时间计算的逻辑
计算和逻辑之间的相互作用可以追溯到计算机科学的早期开端，在20世纪30年代，随着可计算性理论的发展，由A.图灵，K. Gödel, A. Church, S. Kleene和那个时代其他伟大的逻辑学家提出。在最近的几十年里，计算和逻辑之间的交互已经跨越了计算机科学的整个领域，从编程语言到人工智能，从计算复杂性到数据库系统。例如，考虑Pvs。NP问题，它被认为是理论计算机科学中的中心开放问题。1正式,P与NP问题问是否类NP非确定性图灵机可在多项式时间内求解的所有算法问题的P类与确定性图灵机可在多项式时间内求解的所有算法问题的P类重合。非正式地,P与NP问题问的是，每个算法问题的解是否可以被有效地验证，它的解是否也可以被有效地计算。逻辑在这个问题的研究中起了关键作用。事实上，在1971年，S. Cook通过证明NP中“最难”问题的存在布尔可满足性，命题逻辑的一个基本问题，是np完全的。这意味着P = NP当且仅当存在一种有效的算法来判断一个给定的布尔公式是否具有令人满意的真值赋值。
在库克的开创性发现之后不久，费金发现了逻辑和NP之间更紧密的联系，他指出NP与所有算法问题的一类相一致，这些算法问题可以用一种逻辑形式主义来指定存在二阶逻辑简而言之,或ESO．为了说明这个结果，考虑一下3-Colorability，这是另一个突出的np完全问题，它询问给定的图是否G(即一组节点V和一组边E)可以通过给它的每个节点分配三种颜色中的一种来着色，比如蓝、红、黄，这样由一条边连接的两个节点就不会有相同的颜色。可以指定此问题ESO公式显示在页面底部。
直观上，这个公式断言集合V的节点可以划分为三个子集(颜色类)B R,Y这样，如果两个节点x而且y是由边连接的吗E (x, y),然后x而且y不能在同一个颜色班级。费金的结果加强了计算和逻辑之间的统一，它提供了一种基于逻辑的、无需机器的NP描述，而不涉及计算资源(时间)或计算资源的边界(多项式)。
P有逻辑吗?换句话说，是否存在逻辑形式主义l在所有图的类上，这样的P与图上的所有算法问题的类相重合l？这个问题是由Y. Gurevich在1984年提出的，他实际上推测存在没有A. Chandra和D. Harel在1982年提出了P. A相关的(本质上等价的)问题的逻辑，他们问:是否有一种算法可以列举图的所有多项式时间可计算性质?有一个逻辑l因为P将使我们有可能将P与NP的问题重铸为一个纯粹逻辑的问题，即是否的问题ESO而且l对所有图形的集合具有相同的表达能力。此外,逻辑lfor P将作为一种高级规范语言，用于精确地表示图的算法问题，这些算法问题的解可以被有效地计算出来。
在过去的30年里，对所有图类中P的逻辑的探索一直在进行。虽然这个问题到目前为止仍未解决，但这一探索已经引发了一段迷人的旅程，它汇集了几个不同的研究方向。下面这篇由Martin Grohe撰写的论文描述了迄今为止在所有图的类上寻找P的逻辑时所得到的最复杂和最美丽的结果之一。简而言之，Grohe表明，对于许多具有算法兴趣和数学意义的大类图，P确实存在一个逻辑。更准确地说，他的结果断言存在一个P为的逻辑每一个一类图，由所有图组成，其中不包括某个固定的图作为子图，即通过子图上的边收缩得到的图。这一结果极大地推广了早期的工作，即P的逻辑存在于大量的图类中，包括所有平面图的类。
在Grohe的结果中使用的逻辑是带计数的定点逻辑，它是一阶逻辑的自然扩展，具有递归和基数计数机制，在计算机科学的其他领域，特别是数据库中有许多应用。从技术的角度来看，Grohe的证明是一个真正的杰作，它需要发展更深层次的图论机制，以揭示排除余子图的结构的新见解。此外，逻辑和图论的相互作用还带来了另一个好处，即对于每一类不包含余子的图，可以通过一个简单的组合算法在多项式时间内解决图同构问题。所有图类上的图同构问题是否存在多项式时间算法是计算机科学中另一个未解决的主要问题。
©2011 acm 0001-0782/11/0600 $10.00
允许为个人或课堂使用部分或全部作品制作数字或硬拷贝，但不得为盈利或商业利益而复制或分发，且副本在首页上附有本通知和完整的引用。除ACM外，本作品的其他组件的版权必须受到尊重。允许有信用的文摘。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，都需要事先获得特定的许可和/或费用。请求发布的权限permissions@acm.org传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2011 ACM, Inc.