The Complexity of Propositional Proofs
The Complexity of Propositional Proofs
复制标题
命题证明的复杂性
DOI：
10.2307/421131
复制
发表时间：
1995
影响因子：
0.6
通讯作者：
A. Urquhart
中科院分区：
文献类型：
--
作者：
A. Urquhart
§1。介绍。经典的命题演算在逻辑学家中被认为是微不足道的，这是不应有的声誉。我希望能使读者相信，它提出了现代逻辑中一些最具挑战性和最有趣的问题。虽然命题证明的复杂性是一个很自然的问题，但直到20世纪60年代末才开始系统地研究它。对这个问题的兴趣来自与计算机相关的两个领域，自动定理证明和计算复杂性理论。该学科最早的论文是tseittin发表的一篇开创性的文章[62]，这是1966年在列宁格勒研讨会上发表的一篇演讲的出版版本。在那次谈话之后的三十年里，在确定证明系统的相对复杂性和证明某些限制性证明系统的强下界方面取得了实质性进展。然而，主要问题仍然挑战着研究人员。本文提供了该领域的概况，以及一些在推导证明复杂性下界方面已被证明成功的技术。这里只涉及的一个主要领域是有界算术的证明理论及其与命题证明复杂性的关系。读者可以参考Buss[10]的书来了解有界算术的背景知识。Krajíček[40]即将出版的书也很好地介绍了有界算术，并涵盖了命题证明复杂性的大多数基本结果。
§1. Introduction. The classical propositional calculus has an undeserved reputation among logicians as being essentially trivial. I hope to convince the reader that it presents some of the most challenging and intriguing problems in modern logic. Although the problem of the complexity of propositional proofs is very natural, it has been investigated systematically only since the late 1960s. Interest in the problem arose from two fields connected with computers, automated theorem proving and computational complexity theory. The earliest paper in the subject is a ground-breaking article by Tseitin [62], the published version of a talk given in 1966 at a Leningrad seminar. In the three decades since that talk, substantial progress has been made in determining the relative complexity of proof systems, and in proving strong lower bounds for some restricted proof systems. However, major problems remain to challenge researchers. The present paper provides a survey of the field, and of some of the techniques that have proved successful in deriving lower bounds on the complexity of proofs. A major area only touched upon here is the proof theory of bounded arithmetic and its relation to the complexity of propositional proofs. The reader is referred to the book by Buss [10] for background in bounded arithmetic. The forthcoming book by Krajíček [40] also gives a good introduction to bounded arithmetic, as well as covering most of the basic results in complexity of propositional proofs.