Mathematical Sciences: Proof Theory and Computational Complexity

Samuel Buss的研究涉及的是 数学逻辑和低层次的复杂性， 这些主题之间的相互关系。 逻辑系统， 包括算术的片段，特别是有界的 算术，纯一阶逻辑和命题逻辑。 要研究的低级复杂性类包括交替 log time和polynomial time hierarchy。 他特别 致力于发展新的富有成效的联系， 计算复杂性和形式系统的证明理论。 过去的研究已经建立了 这些地区 本项目主要涉及（1）形式理论 与各种紧密相关的证明理论强度 计算复杂度类和（2）第一- 顺序和命题证明，特别是证明的长度。 证明论关注的是证明的性质， 他们的长度，正确性被理解和视为理所当然。 因此，一个典型的结果可能断言命题P是一个 比命题Q更深的结果，在这个意义上， P（在特定的形式系统中）比某些已知的证明长 Q（在同一系统中）。 一种稍微复杂一点的结果 考虑命题P1，P2，P3，...，Pn，...，所有 在形式系统F和形式系统G中都可证明。 例如，如果这些最佳证明的长度 F中的命题的长度随着n的平方而增长，而它们的 G中最好的证明在n中呈指数增长，那么看起来 F是一个比G更强大的系统。 巴斯已经找到了 这种性质的问题的复杂性类的算术 这些功能已经被计算机科学家研究过了。

The research of Samuel Buss deals with formal systems of mathematical logic and with low-level complexity and the interrelationships between these subjects. The logical systems to be studied include fragments of arithmetic, especially bounded arithmetic, and pure first-order logic and propositional logic. The low-level complexity classes to be studied include alternating log time and the polynomial time hierarchy. He is particularly concerned with developing new and fruitful connections between computational complexity and the proof theory of formal systems. Past research has already established intimate connections between these areas. This project concerns primarily (1) formal theories with proof-theoretic strength closely related to various computational complexity classes and (2) the structure of first- order and propositional proofs, especially, the lengths of proofs. Proof theory is concerned with such properties of proofs as their length, correctness being understood and taken for granted. Thus a typical result might assert that the proposition P is a deeper result than the proposition Q in the sense that any proof of P (in a specific formal system) is longer than some known proof of Q (in the same system). A slightly more complicated type of result considers a sequence of propositions P1, P2, P3, ..., Pn, ..., all provable both in the formal system F and in the formal system G. If, for example, the lengths of the best proofs of these propositions in F grow in length as the square of n, while their best proofs in G grow exponentially in n, then it would seem that F is a more powerful system than G. Buss has found ways to relate questions of this nature to complexity classes of arithmetic functions that have already been studied by computer scientists.