Proof Theory and Computational Complexity

巴斯的研究涉及计算复杂性和逻辑的数学方面，特别是计算复杂性和电路复杂性以及数学逻辑的形式系统和证明复杂性之间的关系。要研究的逻辑系统包括算术片段、命题逻辑、一阶逻辑和二阶逻辑。要研究的计算类包括多项式时间、交替对数时间、低级电路类和加密协议。提出的研究旨在证明证明复杂性和计算复杂性的新上界和下界，以及这两个问题之间相互作用的发展。过去的研究已经发展了形式证明系统和形式计算模型之间的密切联系。Buss对证明理论的研究包括从最优证明的大小和证明搜索的难度两方面对证明系统的效率进行调查。这些问题与计算复杂性中一些最重要的开放问题密切相关，例如，P对NP问题和密码学的数学基础。这些开放问题对可计算性理论至关重要，因为在它们得到解决之前，不可能从数学上证明计算复杂性的良好下界；例如，如果不解决这些悬而未决的问题，就不可能从数学上证明加密系统的安全性。Buss等人先前的研究已经在可计算性的基础上建立了证明复杂性和这些问题之间的直接联系。该基金支持的主要研究重点是研究证明复杂性和证明搜索，以及证明复杂性与计算/电路复杂性之间的关系。

The research of Buss deals with the mathematical aspects of computational complexity and logic, especially the relationships between computational complexity and circuit complexity and formal systems of mathematical logic and proof complexity. The logical systems to be investigated include fragments of arithmetic, propositional logics, first-order logics, and second-order logics. The computational classes to be investigated include polynomial time, alternating logarithmic time, low-level circuit classes, and cryptographic protocols. The proposed research is aimed at proving new upper and lower bounds on the complexity of proofs and the complexity of computations, and the development of interactions between these two problems.Past research has developed intimate connections between formal proof systems and formal models of computation. Buss's research on proof theory includes investigations into the efficiency of proof systems, both in terms of the size of optimal proofs and in terms of the difficulty of proof search. These problems are closely related to some of the most important open problems in computational complexity, e.g., to the P versus NP question and to the mathematical foundations of cryptography. These open problems are of fundamental importance to computability theory since, until they are resolved, it will be impossible to mathematically prove good lower bounds on computational complexity; for instance, it will be impossible to mathematically prove the security of cryptographic systems without resolving some of these open questions. Prior research of Buss and others has established direct links between proof complexity and these problems in the foundations of computability. The main thrust of the research supported by this grant is the investigation of proof complexity and proof search, and the relationship between proof complexity and computational/circuit complexity.