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.
