Proof Theory and Computational Complexity

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

This project focuses on some of the unexpectedly fruitful connections between proof theory and important open questions in computational complexity. In mathematical logic, Buss investigates proof theory and proof complexity, especially weak proof systems with close connections to open problems in computational complexity. He investigates aspects of theoretical computer science related to open questions such as the "P versus NP" problem and related problems in complexity including open problems in the mathematical foundations of cryptography. Buss studies the proof complexity of propositional systems such as Frege systems, cutting planes systems, Nullstellensatz proof systems, counting axioms, the polynomial calculus, and intuitionistic proof systems. He plans to extend previous work on bounded arithmetic and its relationships with proof complexity, computational complexity and cryptographic conjectures. The goals of this research are firstly to give bounds on proof size and on proof search algorithms, and to determine what kinds of computational content can be extracted from formal proofs; and secondly to investigate open problems in computational complexity from the viewpoint of mathematical logic.The work of this project is motivated by the desire to obtain a better understanding of open problems in computational complexity. These open problems include the "P versus NP" problem regarding the difficulty of solving a large range of combinatorial problems including scheduling and optimization; they also include establishing the possibility of mathematically secure cryptographic systems. It is commonly believed that many of the computational problems in NP and in cryptography are intractible, and it important for many applications that they be intractible. However, mathematical proofs of intractibility have not been obtained yet, in spite of extensive efforts. Buss works on aspect of these problems in the setting of mathematical logic and proof theory. His work addresses the logical and computational complexity of formal, symbolic proofs; this includes the analysis of proofs in a variety of proof systems corresponding to feasible computation, and the possibility of extracting computational information from proofs. This project will be supported by the Foundations program of the Division of Mathematical Sciences and the Theory of Computing program of the Division of Computer and Communications Research.