Proof complexity, computation, and algorithms

该项目支持巴斯和他的研究生在计算复杂性、证明复杂性、算法和数值方法方面的研究。Buss研究证明理论和证明复杂性，特别是与计算复杂性中的开放问题密切相关的方面，包括P与np问题。相关的证明系统包括有界算术和命题证明系统，前者是一阶理论，具有与可行可计算性相关的逻辑优势，后者与有界算术和电路复杂性有着丰富的联系。Buss将基于复杂性假设（例如存在可证明安全的加密系统）建立证明复杂性的下限。他将致力于证明弱证明系统的新依赖结果和分离结果。他将研究可以从证明中提取哪些计算内容。Buss将研究命题系统的证明复杂性，如Frege系统、切割平面系统、Nullstellensatz证明系统、计数公理、多项式微积分和直觉证明系统。巴斯还研究由计算机图形学产生的数值和几何算法。他将研究用流形上的高阶近似方法模拟刚体的方法，研究物理模拟的辛算法和其他节能算法，以及碰撞响应算法。该项目支持巴斯和他的学生对数学和计算机科学之间的接口问题的研究，这些问题的动机是关于计算的基本限制的开放问题。这些开放问题包括P对NP问题，安全密码编码的数学可行性，以及解决组合问题的特定算法和电路的最优性。Busss通过研究计算复杂性和证明复杂性来解决这些问题。该项目研究了形式证明系统的强度与最优证明的大小之间的权衡问题。良好的边界证明复杂度与计算难度的上界和下界以及密码学的数学基础密切相关。该项目还支持巴斯在动态系统仿真算法方面的工作

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