NSF Young Investigator: Logic and Complexity Theory

证明系统复杂性的研究是逻辑学的基础，在计算机科学中也有广泛的应用。 首先，任何演绎系统的效率都与逻辑推理的速度有关（例如，Prolog、Datasheet和人工智能中的许多推理系统）。 其次，命题证明系统的复杂性与复杂性理论中的中心问题NP是否等于coNP密切相关。 最后，在特定的命题证明系统、算术系统和复杂性类之间存在联系。 利用这些联系，人们可以应用一系列全新的工具，从逻辑到解决困难的复杂性问题（如P = NP）。 命题逻辑中要考虑的基本问题是：作为重言式大小的函数，一个命题重言式的证明需要多长时间？ 所有已知的证明系统的最佳上界是指数的重言式的大小，它是一个类似的下界举行。 这个问题等价于NP是否= coNP，虽然在过去的25年里已经被广泛研究，但仍然远远没有解决。 命题证明系统可以被划分为直接对应于复杂性类的类。 证明NP = coNP的一种方法是为越来越大的证明强度的特定证明系统建立超多项式下界。 这项研究的大部分目的是解决这个难题。 另一条研究路线涉及可行算术（也称为有界算术）及其与 命题证明和复杂性理论。 可行的概念 在过去的十年里，证据一直是许多研究的主题。

The study of the complexity of proof systems is fundamental to logic and has a broad range of applications in computer science as well. First, the efficiency of any deduction system is tied to the speed of logical reasoning (e.g., Prolog, Datalog, and many inferencing systems in artificial intelligence). Secondly, the complexity of propositional proof systems is intimately connected to the central question in complexity theory of whether NP equal coNP. Finally, there are links between particular propositional proof systems, systems of arithmetic, and complexity classes. Exploiting these connections, one can apply a whole new range of tools from logic to attack difficult complexity questions (such as P = NP). The basic question in propositional logic to be considered is: How long does a proof of a propositional tautology have to be, as a function of the size of the tautology? The best upper bound for all known proof systems is exponential in the size of the tautology and it is conjectured that a similar lower bound holds. This question is equivalent to whether or not NP = coNP, and while it has been studied extensively for the last 25 years, it is still far from solved. Propositional proof systems can be divided into classes that correspond directly to complexity classes. An approach toward proving NP = coNP is to establish superpolynomial lower bounds for specific proof systems of greater and greater proof strength. Much of this research is aimed at attacking this difficult problem. Another line of research concerns feasible arithmetic (also known as bounded arithmetic) and its connections to propositional proofs and complexity theory. The concept of a feasible proof has been the subject of much research in the last ten years.