Mathematical Sciences: Proof Theory and Computational Complexity

9503247 Bus Bus将研究有界算术理论的公理和条件分离；命题证明系统的相对证明复杂性，包括Frege、Extended Frege、Constant-Depth Frege、Hilbert Nullstellensatz和割平面证明系统；基于序列演算的扩展设计计算机化定理证明器的问题；以及低级计算复杂性的各种问题。巴斯的研究涉及(I)数学逻辑的形式化系统和这种系统中证明的复杂性，以及(Ii)计算复杂性和可行复杂性。这项研究的一个中心目标是将证明系统的强度与计算的复杂性或难度联系起来。Bus的工作主要集中在与可行计算的函数相对应的证明系统上，特别是多项式时间计算的证明系统。巴斯还将研究命题逻辑和一阶逻辑的各种证明系统的相对有效性。这项研究是理解计算在数学中的力量的基础。***

9503247 Buss Buss will investigate axiomatics and conditional separations of bounded arithmetic theories; relative proof complexity of propositional proof systems including Frege, extended Frege, constant-depth Frege, Hilbert Nullstellensatz and cutting plane proof systems; problems in designing computerized theorem provers based on extensions of the sequent calculus; and various problems in low-level computational complexity. Buss' research concerns (i) formal systems of mathematical logic and the complexity of proofs in such systems and (ii) computational complexity and feasible complexity. A central goal for this research is to relate the strength of proof systems to the complexity or difficulty of computations. Buss' work centers on proof systems corresponding to functions which are feasibly computable, especially on proof systems for polynomial time computation. Buss will also investigate the relative effectiveness of various proof systems for propositional and first-order logic. This research is fundamental to understanding the power of computation in mathematics. ***