Mathematical Sciences: Proof Theory and Computational Complexity

数学科学：证明理论和计算复杂性

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

9503247 Buss Buss will investigate axiomatics and conditional separations of bounded arithmetic theories; relative proof complexity of propositional proof systems including Frege, extended Frege, constant-depth Frege, Hilbert Nullstellensatz and cutting plane proof systems; problems in designing computerized theorem provers based on extensions of the sequent calculus; and various problems in low-level computational complexity. Buss' research concerns (i) formal systems of mathematical logic and the complexity of proofs in such systems and (ii) computational complexity and feasible complexity. A central goal for this research is to relate the strength of proof systems to the complexity or difficulty of computations. Buss' work centers on proof systems corresponding to functions which are feasibly computable, especially on proof systems for polynomial time computation. Buss will also investigate the relative effectiveness of various proof systems for propositional and first-order logic. This research is fundamental to understanding the power of computation in mathematics. ***

小行星9503247 巴斯将调查公理和有界算术理论的条件分离;命题的相对证明复杂性 证明系统包括弗雷格，扩展弗雷格，恒定深度弗雷格， 希尔伯特零空间和割平面证明系统;基于扩展的计算机定理证明器设计中的问题 以及低级计算中的各种问题 复杂性 巴斯的研究涉及（i）数学逻辑的形式系统和在这种系统中证明的复杂性，以及（ii）计算 复杂性和可行复杂性。 这项研究的中心目标是 将证据系统的强度与以下问题的复杂性或难度联系起来： 计算。 巴斯的工作集中在证明系统上， 函数是可行的计算，特别是在证明系统， 多项式时间计算 巴斯还将调查这位亲戚 命题和一阶逻辑的各种证明系统的有效性 逻辑 这项研究对于理解 数学中的计算 ***