Proof complexity, computation, and algorithms

证明复杂性、计算和算法

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

This project supports research by Buss and his graduate students oncomputational complexity, proof complexity, algorithms, andnumerical methods. Buss investigates proof theory and proofcomplexity, especially aspects that are closely connected to openproblems in computational complexity including the P versus NPproblem. The relevant proof systems include bounded arithmetics,which are first-order theories tailored to have logical strengthrelated to feasible computability, and propositional proof systems,which have rich connections to bounded arithmetic and circuitcomplexity. Buss will work to establish lower bounds on proofcomplexity based on complexity assumptions such as the existence ofprovably secure cryptographic systems. He will work to prove newindependence results and separation results for weak proof systems.He will investigate what kinds of computational content can beextracted from proofs. Buss will investigate the proof complexity ofpropositional systems such as Frege systems, cutting planes systems,Nullstellensatz proof systems, counting axioms, the polynomialcalculus, and intuitionistic proof systems. Buss also works onnumerical and geometric algorithms arising from computer graphics.He will work on simulation methods for rigid multibodies usinghigher-order approximation methods over manifolds, on symplecticalgorithms and other energy-conserving algorithms for physicalsimulations, and on collision response algorithms.The project supports research by Buss and his students on problemsthat le at the interface between mathematics and computer science,as motivated by open questions concerning the fundamental limits ofcomputation. These open questions include the P versus NP problem,the mathematical feasibility of secure cryptographic coding, and theoptimality of particular algorithms and circuits for solvingcombinatorial problems. Busss addresses these questions byinvestigating computational complexity and proof complexity. Theproject studies questions about the tradeoffs between the strengthof a formal proof system and the size of optimal proofs. Good boundson proof complexity are closely related to upper and lower bounds onthe hardness of computation, as well as to the mathematicalunderpinnings of cryptography. The project also supports Buss'swork on algorithms for simulation of dynamical systems

该项目支持巴斯和他的研究生在计算复杂性、证明复杂性、算法和数值方法方面的研究。Bus研究了证明理论和证明复杂性，特别是在计算复杂性方面与公开问题密切相关的方面，包括P与NP问题。相关的证明系统包括有界算术和命题证明系统，有界算术是一阶理论，被定制为具有与可行可计算性相关的逻辑强度，命题证明系统与有界算术和电路复杂性具有丰富的联系。BUS将致力于基于复杂性假设建立证明复杂性的下限，例如存在可证明安全的密码系统。他将致力于证明弱证明系统的新相依结果和分离结果。他将研究从证明中可以提取哪些计算内容。BUS将研究命题系统的证明复杂性，如Frege系统、割平面系统、Nullstellensz证明系统、计数公理、多项式演算和直觉证明系统。巴斯还致力于计算机图形学产生的数值和几何算法。他将致力于使用流形上的高阶近似方法来模拟刚体多体的方法，物理模拟的辛算法和其他能量守恒算法，以及碰撞响应算法。该项目支持巴斯和他的学生对数学和计算机科学交界处的问题的研究，这些问题的动机是关于计算的基本极限的公开问题。这些悬而未决的问题包括P与NP问题，安全密码编码的数学可行性，以及解决组合问题的特定算法和电路的最优性。巴斯通过调查计算复杂性和证明复杂性来解决这些问题。该项目研究了形式证明系统的强度和最佳证明的大小之间的权衡问题。良好的边界证明复杂性与计算难度的上下界以及密码学的数学基础密切相关。该项目还支持BUS在动态系统仿真算法方面的工作