Mathematical Sciences: Proof Theory and Computational Complexity

9503247 Buss将研究有界算术理论的公理化和条件分离；Frege、扩展Frege、定深Frege、Hilbert Nullstellensatz和切割平面证明等命题证明系统的相对证明复杂性；基于相继演算扩展的计算机定理证明器设计中的几个问题以及各种低级计算复杂度的问题。Buss的研究关注(i)数学逻辑的形式系统和这些系统中证明的复杂性，以及（ii）计算复杂性和可行复杂性。本研究的中心目标是将证明系统的强度与计算的复杂性或难度联系起来。巴斯的工作主要集中在可计算函数的证明系统，特别是多项式时间计算的证明系统。Buss还将研究命题逻辑和一阶逻辑的各种证明系统的相对有效性。这项研究是理解数学计算能力的基础。＊＊＊

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. ***