Mathematical Sciences: Proof Theory and Computational Complexity

[8902480] Buss这个研究项目处理低复杂度和算术和数理逻辑的弱形式系统之间的关系。低复杂度涉及可行的计算模型，如多项式时间计算、对数空间可计算性和交替对数时间。过去的研究已经显示了低复杂度和非常弱的逻辑系统之间的密切联系。拟研究的领域包括研究命题和一阶证明的长度，有界算术的公理化，直觉有界算术，以及获得与交替对数时间和不确定对数空间等计算类具有证明理论强度的形式理论。

8902480 Buss This research project deals with the relationship between low-level complexity and weak formal systems of arithmetic and mathematical logic. Low-level complexity concerns feasible computational models such as polynomial time computation, logarithmic space computability and alternating logarithmic time. Past research has already shown intimate connections between low-level complexity and very weak logical systems. The intended areas for research include research on lengths of propositional and first-order proofs, on axiomatizations of Bounded Arithmetic, on intutionistic Bounded Arithemetic, and on obtaining formal theories which have proof-theoretic strength equivalent to computational classes such as alternating logarithmic time and nondeterministic logarithmic space.