Proof complexity, computation, and algorithms

University Of California-San Diego, La Jolla CA

Investigators

Abstract

This project supports research by Buss and his graduate students on computational complexity, proof complexity, algorithms, and numerical methods. Buss investigates proof theory and proof complexity, especially aspects that are closely connected to open problems in computational complexity including the P versus NP problem. The relevant proof systems include bounded arithmetics, which are first-order theories tailored to have logical strength related to feasible computability, and propositional proof systems, which have rich connections to bounded arithmetic and circuit complexity. Buss will work to establish lower bounds on proof complexity based on complexity assumptions such as the existence of provably secure cryptographic systems. He will work to prove new independence results and separation results for weak proof systems. He will investigate what kinds of computational content can be extracted from proofs. Buss will investigate 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. Buss also works on numerical and geometric algorithms arising from computer graphics. He will work on simulation methods for rigid multibodies using higher-order approximation methods over manifolds, on symplectic algorithms and other energy-conserving algorithms for physical simulations, and on collision response algorithms. The project supports research by Buss and his students on problems that le at the interface between mathematics and computer science, as motivated by open questions concerning the fundamental limits of computation. These open questions include the P versus NP problem, the mathematical feasibility of secure cryptographic coding, and the optimality of particular algorithms and circuits for solving combinatorial problems. Busss addresses these questions by investigating computational complexity and proof complexity. The project studies questions about the tradeoffs between the strength of a formal proof system and the size of optimal proofs. Good bounds on proof complexity are closely related to upper and lower bounds on the hardness of computation, as well as to the mathematical underpinnings of cryptography. The project also supports Buss's work on algorithms for simulation of dynamical systems