Proof Theory and Computational Complexity

点击翻译按钮获取中文摘要

The research of Buss deals with the mathematical aspects of computational complexity and logic, especially the relationships between computational complexity and circuit complexity and formal systems of mathematical logic and proof complexity. The logical systems to be investigated include fragments of arithmetic, propositional logics, first-order logics, and second-order logics. The computational classes to be investigated include polynomial time, alternating logarithmic time, low-level circuit classes, and cryptographic protocols. The proposed research is aimed at proving new upper and lower bounds on the complexity of proofs and the complexity of computations, and the development of interactions between these two problems.Past research has developed intimate connections between formal proof systems and formal models of computation. Buss's research on proof theory includes investigations into the efficiency of proof systems, both in terms of the size of optimal proofs and in terms of the difficulty of proof search. These problems are closely related to some of the most important open problems in computational complexity, e.g., to the P versus NP question and to the mathematical foundations of cryptography. These open problems are of fundamental importance to computability theory since, until they are resolved, it will be impossible to mathematically prove good lower bounds on computational complexity; for instance, it will be impossible to mathematically prove the security of cryptographic systems without resolving some of these open questions. Prior research of Buss and others has established direct links between proof complexity and these problems in the foundations of computability. The main thrust of the research supported by this grant is the investigation of proof complexity and proof search, and the relationship between proof complexity and computational/circuit complexity.