Complexity of proofs, proof search, and algorithmic complexity

该项目支持Buss教授和他的研究生在逻辑和计算复杂性方面的研究，特别是在计算复杂性，命题证明复杂性，有界算术，随机性和近似以及算法设计方面。中心研究课题涉及命题证明复杂性及其与计算复杂性和一阶算术的相互作用。命题证明复杂性构成了几乎所有支持逻辑推理和推断的形式系统的基础。证明复杂性和一阶算术的弱理论的许多方面都与计算复杂性中的开放问题有关，包括P对NP问题，计数和去随机化问题，以及关于伪随机数生成器的开放密码学问题。PI将致力于扩展可满足性和其他困难问题的确定性算法的下限。他的研究将探索证明搜索的数学基础。他将开发和测试命题证明搜索的新算法。他将致力于有界算术片段的新见证算法，例如对应于多项式空间推理的逻辑。他将致力于证明新的独立性结果和分离结果的弱证明系统。他将致力于复杂性下界，特别是空间受限的计算。证明论，逻辑和算法的数学研究的目标是提高我们对可行可计算性，可行可证明性和密码算法的数学安全性的基本限制的理解。该项目支持PI及其学生对证明和算法复杂性的数学方面的研究，特别强调建立证明和计算所需的复杂性。PI还将开发和评估新的可满足性算法。这些算法是大多数目前部署的软件和硬件验证系统的逻辑核心，并且是产生可验证正确的软件和硬件的几个主要研究工作的重要部分。该项目支持数学和计算机科学的教育和学生研究培训，特别是计算复杂性和数理逻辑的方法和理论。

This project supports research by Professor Buss and his graduate students in logic and computational complexity, particularly in computational complexity, propositional proof complexity, bounded arithmetic, randomness and approximation, and algorithm design. The central research topics concern propositional proof complexity and its interplay with computational complexity and first-order arithmetic. Propositional proof complexity forms a basis for nearly all formal systems that support logical reasoning and inference. Many aspects of proof complexity and weak theories of first-order arithmetic connect to open problems in computational complexity, including the P versus NP problem, questions about counting and derandomization, and open cryptographic questions about pseudorandom number generators. The PI will work to extend lower bounds on deterministic algorithms for satisfiability and other hard problems. His research will explore the mathematical foundations of proof search. He will develop and test new algorithms for propositional proof search. He will work on new witnessing algorithms for fragments of bounded arithmetic, such as logics that correspond to polynomial space reasoning. He will work to prove new independence results and separation results for weak proof systems. He will work on complexity lower bounds, especially for space-restricted computation.Mathematical research on proof theory, logic, and algorithms has the goal of improving our understanding of fundamental limitations of feasible computability, feasible provability, and the mathematical security of cryptographic algorithms. The project supports the research of the PI and his students on these mathematical aspects of complexity of proofs and algorithms, with particular emphasis on establishing the complexity required for proofs and computations. The PI will also develop and evaluate new algorithms for satisfiability. These algorithms are the logical core of most presently deployed systems for software and hardware verification, and are an important part of several major research efforts to produce verifiably correct software and hardware. The project supports education and student research training in mathematics and computer science, especially in the methods and theory of computational complexity and mathematical logic.