Proof complexity, computation, and algorithms

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

This project supports research by Buss and his graduate students oncomputational complexity, proof complexity, algorithms, andnumerical methods. Buss investigates proof theory and proofcomplexity, especially aspects that are closely connected to openproblems in computational complexity including the P versus NPproblem. The relevant proof systems include bounded arithmetics,which are first-order theories tailored to have logical strengthrelated to feasible computability, and propositional proof systems,which have rich connections to bounded arithmetic and circuitcomplexity. Buss will work to establish lower bounds on proofcomplexity based on complexity assumptions such as the existence ofprovably secure cryptographic systems. He will work to prove newindependence results and separation results for weak proof systems.He will investigate what kinds of computational content can beextracted from proofs. Buss will investigate the proof complexity ofpropositional systems such as Frege systems, cutting planes systems,Nullstellensatz proof systems, counting axioms, the polynomialcalculus, and intuitionistic proof systems. Buss also works onnumerical and geometric algorithms arising from computer graphics.He will work on simulation methods for rigid multibodies usinghigher-order approximation methods over manifolds, on symplecticalgorithms and other energy-conserving algorithms for physicalsimulations, and on collision response algorithms.The project supports research by Buss and his students on problemsthat le at the interface between mathematics and computer science,as motivated by open questions concerning the fundamental limits ofcomputation. These open questions include the P versus NP problem,the mathematical feasibility of secure cryptographic coding, and theoptimality of particular algorithms and circuits for solvingcombinatorial problems. Busss addresses these questions byinvestigating computational complexity and proof complexity. Theproject studies questions about the tradeoffs between the strengthof a formal proof system and the size of optimal proofs. Good boundson proof complexity are closely related to upper and lower bounds onthe hardness of computation, as well as to the mathematicalunderpinnings of cryptography. The project also supports Buss'swork on algorithms for simulation of dynamical systems