This project supports research by Professor Buss and his graduate students in logic and computational complexity, particularly in computational complexity, propositional proof complexity, bounded arithmetic, randomness and approximation, and algorithm design. The central research topics concern propositional proof complexity and its interplay with computational complexity and first-order arithmetic. Propositional proof complexity forms a basis for nearly all formal systems that support logical reasoning and inference. Many aspects of proof complexity and weak theories of first-order arithmetic connect to open problems in computational complexity, including the P versus NP problem, questions about counting and derandomization, and open cryptographic questions about pseudorandom number generators. The PI will work to extend lower bounds on deterministic algorithms for satisfiability and other hard problems. His research will explore the mathematical foundations of proof search. He will develop and test new algorithms for propositional proof search. He will work on new witnessing algorithms for fragments of bounded arithmetic, such as logics that correspond to polynomial space reasoning. He will work to prove new independence results and separation results for weak proof systems. He will work on complexity lower bounds, especially for space-restricted computation.
Mathematical research on proof theory, logic, and algorithms has the goal of improving our understanding of fundamental limitations of feasible computability, feasible provability, and the mathematical security of cryptographic algorithms. The project supports the research of the PI and his students on these mathematical aspects of complexity of proofs and algorithms, with particular emphasis on establishing the complexity required for proofs and computations. The PI will also develop and evaluate new algorithms for satisfiability. These algorithms are the logical core of most presently deployed systems for software and hardware verification, and are an important part of several major research efforts to produce verifiably correct software and hardware. The project supports education and student research training in mathematics and computer science, especially in the methods and theory of computational complexity and mathematical logic.
