Complexity, Formal Systems, and Linear-Time Computation

这个项目的目标是开展复杂性理论和逻辑的基础研究，重点是P=？NP问题。这个问题涉及数百个长期研究的计算机决策问题，问题是这些问题是否可以用省时的方法来解决。该项目的第一部分是为“结构”复杂性理论开发一个统一的基础，该理论改进了目前用于研究多项式时间的技术。取得进展的一个关键想法是，这些技术中的许多可以被改进以研究线性时间计算，其中类似于“P=NP”的结果已经知道，并且基本性质在形式逻辑中具有更简单的表示。预期的结果是对可在线性或“近线性”时间内解决的问题进行更好的分类，并更深入地理解在多项式时间内回答主要开放问题的障碍。第二部分将复杂性理论与逻辑学家开发的技术相结合，用于分析某些特定的形式系统，这些系统能够对理论计算机科学中的许多当前工作进行建模。一些研究人员提出了一种可能性，即“计算机科学中的现有方法”可能不能解决“P=？NP”和相关问题；这个项目从这些形式系统的角度寻求一个明确的答案。另一个目标是开发这些系统可能缺乏的技术，这得益于最近的经验，即一些具体的结果本质上需要“抽象”的方法，以及计算机辅助定理证明的进步。

The objective of this project is to carry out fundamental research in complexity theory and logic, focusing on the formal status of the P=? NP question. This question involves hundreds of long-studied computer decision problems, and asks whether they can be solved by time-efficient methods, or not. The first part of the project is to develop a uniform foundation for "structural" complexity theory, one which refines the techniques currently used to investigate polynomial time. A key idea for making progress is that many of these techniques can be sharpened to study linear time computation, where results analogous to "P = NP" are already known, and where basic properties have simpler representations in formal logic. Expected results are a better classification of problems solvable in linear or "nearly linear" time, and a deeper understanding of the obstacles to answering the major open questions for polynomial time. The second part combines complexity theory with techniques developed by logicians for analyzing certain specific formal systems, ones capable of modeling much current work in theoretical computer science. Several researchers have raised the possibility that "current methods in computer science" may be incapable of resolving "P =? NP" and related questions; this project seeks a definite answer in terms of these formal systems. A further goal is to develop those techniques which these systems may lack, aided by recent evedence that some concrete results essentially require "abstract" methods, and by advances in computer-assisted theorem proving.