Complexity, Formal Systems, and Linear-Time Computation

复杂性、形式系统和线性时间计算

• 批准号: 9011248
• 负责人: Kenneth Regan
• 金额: $ 3.5万
• 依托单位: SUNY College at Buffalo
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-07-01 至 1993-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9011248&HistoricalAwards=false
• 关键词: Complexity; Formal; Systems; Linear; Time

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.

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