Proof Complexity and Computation

该项目支持巴斯和他的研究生在计算复杂性、证明复杂性、算法和数值方法方面的研究。Bus研究了证明理论和证明复杂性，特别是在计算复杂性方面与公开问题密切相关的方面，包括Thep与NP问题。相关的证明系统包括有界算术和命题证明系统，前者是为具有与可行可计算性相关的逻辑强度而定制的一阶理论，后者与有界算术和电路复杂性有着丰富的联系。Bus将致力于基于复杂性假设(例如存在可证明安全的密码系统)来建立证明复杂性的下界。他将致力于证明弱证明系统的新的独立结果和分离结果。他将研究从证明中可以提取哪些类型的计算内容。巴斯将研究命题系统的证明复杂性，如Frege系统、割平面系统、Nullstellensz证明系统、计数公理、多项式演算和直觉证明系统。Buss还研究源于计算机图形学的数值和几何算法。他将致力于刚性多体的高阶超流形模拟方法，物理模拟的辛算法和其他能量守恒算法，以及碰撞响应算法。这项研究的主要部分位于数学和计算机科学之间的界面上，并受到有关计算基本极限的开放问题的推动。这些悬而未决的问题包括P与NP问题，安全密码编码的数学可行性，以及解决组合问题的特定算法和电路的最优化。本项目通过调查计算复杂性和证明复杂性来解决这些问题。证明复杂性的上下界与计算难度的上下界密切相关。这反过来又与密码学的数学基础密切相关。

This project supports research by Buss and his graduatestudents on computational complexity, proof complexity,algorithms, and numerical methods. Buss investigates proof theoryand proof complexity, especially aspects that are closely connectedto open problems in computational complexity including theP versus NP problem. The relevant proof systems includebounded arithmetics, which are first-order theories tailored to havelogical strength related to feasible computability, andpropositional proof systems, which have rich connections to boundedarithmetic and circuit complexity. Buss will work to establishlower bounds on proof complexity based on complexity assumptionssuch as the existence of provably secure cryptographic systems.He will work to prove new independence results and separationresults for weak proof systems. He will investigate what kindsof computational content can be extracted from proofs.Buss will investigate the proof complexity of propositional systems such asFrege systems, cutting planes systems, Nullstellensatz proof systems,counting axioms, the polynomial calculus, and intuitionistic proof systems.Buss also works on numerical and geometric algorithms arisingfrom computer graphics. He will work on simulation methods forrigid multibodies using higher-order approximation methods overmanifolds, on symplectic algorithms and other energy-conservingalgorithms for physical simulations, and on collision responsealgorithms.The main part of this research lies at the interface between mathematics and computer science and is motivated by open questions concerning the fundamental limits of computation. These open questions include the P versus NP problem, the mathematicalfeasibility of secure cryptographic coding, and the optimalityof particular algorithms and circuits for solving combinatorial problems.This project addresses these questions by investigating computationalcomplexity and proof complexity. Lower and upper bounds onproof complexity are closely related to upper and lower boundson the hardness of computation. This in turn is closelyrelated to the mathematical underpinnings of crytography.