Proof Complexity and Computation

该项目支持巴斯和他的研究生在计算复杂性、证明复杂性、算法和数值方法方面的研究。巴斯研究证明理论和证明复杂性，特别是与计算复杂性中的开放问题密切相关的方面，包括p与NP问题。相关证明系统包括有界算法和命题证明系统，有界算法是一阶理论，具有与可行可计算性相关的逻辑强度，命题证明系统与有界算法和电路复杂性有丰富的联系。巴斯将根据复杂性假设（例如存在可证明安全的加密系统）建立证明复杂性的下限。他将致力于为弱证明系统证明新的独立结果和分离结果。他将研究从证明中可以提取出什么样的计算内容。Buss将研究命题系统的证明复杂性，如frege系统、切面系统、Nullstellensatz证明系统、计数公理、多项式演算和直觉证明系统。巴斯还研究由计算机图形学产生的数值和几何算法。他将研究使用流形上的高阶近似方法模拟刚体的方法，研究物理模拟的辛算法和其他节能算法，以及碰撞响应算法。这项研究的主要部分在于数学和计算机科学之间的接口，并受到有关计算基本限制的开放问题的激励。这些开放问题包括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.