Proof Theory and Computational Complexity

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

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.