Complexity, Formal Systems, and Linear-Time Computation

该项目的目标是开展基础研究， 复杂性理论和逻辑，侧重于形式的地位， P=？NP问题。 这个问题涉及数百个长期研究的 计算机决策问题，并问他们是否可以解决， 时间效率的方法，或不。 该项目的第一部分是 为“结构”复杂性理论建立统一的基础， 它改进了目前用于研究多项式的技术， 时间 取得进展的一个关键思想是， 可以锐化研究线性时间计算，其中结果 类似于“P = NP”是已知的，并且其中基本性质 在形式逻辑中有更简单的表示。 预期结果是a 更好的分类问题可解决的线性或“近似” 线性”时间，并对回答问题的障碍有了更深入的了解 多项式时间的主要开放问题。 第二部分 将复杂性理论与逻辑学家开发的技术相结合， 分析某些特定的正式系统，那些能够建模的系统， 理论计算机科学中的许多当前工作。 几 研究人员提出了“目前的方法在 计算机科学”可能无法解决“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.