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