Proof Theory and Computational Complexity

证明理论和计算复杂性

• 批准号: 0100589
• 负责人: Samuel Buss
• 金额: $ 23.85万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-07-01 至 2005-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0100589&HistoricalAwards=false
• 关键词: Proof; Theory; Computational; Complexity

This project focuses on some of the unexpectedly fruitful connections between proof theory and important open questions in computational complexity. In mathematical logic, Buss investigates proof theory and proof complexity, especially weak proof systems with close connections to open problems in computational complexity. He investigates aspects of theoretical computer science related to open questions such as the "P versus NP" problem and related problems in complexity including open problems in the mathematical foundations of cryptography. Buss studies the proof complexity of propositional systems such as Frege systems, cutting planes systems, Nullstellensatz proof systems, counting axioms, the polynomial calculus, and intuitionistic proof systems. He plans to extend previous work on bounded arithmetic and its relationships with proof complexity, computational complexity and cryptographic conjectures. The goals of this research are firstly to give bounds on proof size and on proof search algorithms, and to determine what kinds of computational content can be extracted from formal proofs; and secondly to investigate open problems in computational complexity from the viewpoint of mathematical logic.The work of this project is motivated by the desire to obtain a better understanding of open problems in computational complexity. These open problems include the "P versus NP" problem regarding the difficulty of solving a large range of combinatorial problems including scheduling and optimization; they also include establishing the possibility of mathematically secure cryptographic systems. It is commonly believed that many of the computational problems in NP and in cryptography are intractible, and it important for many applications that they be intractible. However, mathematical proofs of intractibility have not been obtained yet, in spite of extensive efforts. Buss works on aspect of these problems in the setting of mathematical logic and proof theory. His work addresses the logical and computational complexity of formal, symbolic proofs; this includes the analysis of proofs in a variety of proof systems corresponding to feasible computation, and the possibility of extracting computational information from proofs. This project will be supported by the Foundations program of the Division of Mathematical Sciences and the Theory of Computing program of the Division of Computer and Communications Research.

这个项目的重点是证明理论和计算复杂性中的重要开放问题之间的一些意想不到的富有成效的联系。在数理逻辑中，巴斯研究证明理论和证明复杂性，特别是与计算复杂性中的开放问题密切相关的弱证明系统。 他研究了与开放性问题相关的理论计算机科学方面，如“P对NP”问题和复杂性中的相关问题，包括密码学数学基础中的开放性问题。巴斯研究命题系统的证明复杂性，如弗雷格系统，切割平面系统，零星证明系统，计数公理，多项式演算和直觉证明系统。他计划扩展以前在有界算术及其与证明复杂性、计算复杂性和密码学结构之间的关系方面的工作。 本研究的目标是首先给出证明大小和证明搜索算法的界限，并确定可以从形式证明中提取什么样的计算内容;其次从数理逻辑的角度研究计算复杂性中的开放问题。 这些开放问题包括“P对NP”问题，涉及解决大量组合问题（包括调度和优化）的难度;它们还包括建立数学安全密码系统的可能性。 人们普遍认为，NP和密码学中的许多计算问题是难解的，并且对于许多应用来说，它们是难解的是很重要的。 然而，数学证明的intractibility尚未获得，尽管广泛的努力。巴斯在数理逻辑和证明论的背景下对这些问题进行了研究。 他的工作解决了逻辑和计算复杂性的正式，符号证明;这包括分析证明在各种证明系统对应可行的计算，并提取计算信息的可能性证明。该项目将得到数学科学部基础计划和计算机与通信研究部计算理论计划的支持。