Mathematical Sciences: Proof Theory and Computational Complexity

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

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

The research of Samuel Buss deals with formal systems of mathematical logic and with low-level complexity and the interrelationships between these subjects. The logical systems to be studied include fragments of arithmetic, especially bounded arithmetic, and pure first-order logic and propositional logic. The low-level complexity classes to be studied include alternating log time and the polynomial time hierarchy. He is particularly concerned with developing new and fruitful connections between computational complexity and the proof theory of formal systems. Past research has already established intimate connections between these areas. This project concerns primarily (1) formal theories with proof-theoretic strength closely related to various computational complexity classes and (2) the structure of first- order and propositional proofs, especially, the lengths of proofs. Proof theory is concerned with such properties of proofs as their length, correctness being understood and taken for granted. Thus a typical result might assert that the proposition P is a deeper result than the proposition Q in the sense that any proof of P (in a specific formal system) is longer than some known proof of Q (in the same system). A slightly more complicated type of result considers a sequence of propositions P1, P2, P3, ..., Pn, ..., all provable both in the formal system F and in the formal system G. If, for example, the lengths of the best proofs of these propositions in F grow in length as the square of n, while their best proofs in G grow exponentially in n, then it would seem that F is a more powerful system than G. Buss has found ways to relate questions of this nature to complexity classes of arithmetic functions that have already been studied by computer scientists.

塞缪尔·巴斯的研究涉及数理逻辑的形式系统，以及低层次的复杂性和这些学科之间的相互关系。要研究的逻辑系统包括算术片段，特别是有界算术，以及纯一阶逻辑和命题逻辑。要研究的低级复杂性类包括交错对数时间和多项式时间层次。他特别关注在计算复杂性和形式系统的证明理论之间发展新的和富有成效的联系。过去的研究已经在这些区域之间建立了密切的联系。这个项目主要涉及(1)具有与各种计算复杂性类密切相关的证明论强度的形式理论和(2)一阶和命题证明的结构，特别是证明的长度。证明论关注的是证明的性质，如它们的长度、正确性被理解和视为理所当然。因此，一个典型的结果可能断言，命题P是比命题Q更深的结果，因为P的任何证明(在特定的形式系统中)都比Q的某些已知证明(在同一系统中)要长。稍微复杂一点的结果类型考虑在形式系统F和形式系统G中都可证明的命题序列P1、P2、P3、…、Pn、……。例如，如果F中这些命题的最佳证明的长度以n的平方增长，而它们在G中的最佳证明在n中指数增长，那么，似乎F是一个比G.Buss找到了将这种性质的问题与计算机科学家已经研究过的复杂算术函数类联系起来的方法更强大的系统。