NSF Young Investigator: Logic and Complexity Theory

对证明系统复杂性的研究是逻辑的基础，在计算机科学中也有广泛的应用。首先，任何演绎系统的效率都与逻辑推理的速度有关(例如，Prolog、Datalog和人工智能中的许多推理系统)。其次，命题证明系统的复杂性与复杂性理论中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.