One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus. The purpose of the present paper is to study a question related to the complexity of decision procedures for the propositional calculus; namely, the complexity of proof systems for the propositional calculus. The fundamental issue here is whether there exists any proof system, and a polynomial p(n) such that every valid formula has a proof of length not exceeding p(n), where n is the length of the formula. Theorem 1 below helps establish the importance of this question. For the purposes of this theorem, we give the following definitions.

article Free Access Share on Corrections for "On the lengths of proofs in the propositional calculus preliminary version" Authors: Stephen Cook View Profile , Robert Reckhow View Profile Authors Info & Claims ACM SIGACT NewsVolume 6Issue 3July 1974 pp 15–22https://doi.org/10.1145/1008311.1008313Online:01 July 1974Publication History 12citation167DownloadsMetricsTotal Citations12Total Downloads167Last 12 Months2Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

The RAM, an abstract model for a random access computer, is introduced. A unique feature of the model is that the execution time of an instruction is defined in terms of l(n), a function of the size of the numbers manipulated by the instruction. This model has a fixed program, but it is shown that the computing speeds of this model and a stored-program model can differ by no more than a constant factor. It is proved that a T(n) time-bounded Turing machine can be simulated by an O(T(n).l(T(n))) timebounded RAM, and that a T(n) time-bounded RAM can be simulated by a Turing machine whose execution time is bounded by (T(n))^3 if l(n) is constant, or (T(n))^2 if l(n) is logarithmic. The main result states that if T"2(n) is a function such that there is a RAM that computes T"2(n) in time O(T"2(n)), and if T"1(n) is any function such that liminfn->~T"1(n)T"2(n)=0, then there is a set S that can be recognized by some RAM in time O(T"2(n)), but no RAM recognizes S in time O(T"1(n)). This is a sharper diagonal result than has been obtained for Turing machines. The proofs of most of the above results are constructive and are aided by the introduction of an ALGOL-like programming language for RMA's.

In this paper we introduce a formal model for random access computers and argue that the model is a good one to use in the theory of computational complexity. Results are proved which compare run times for recognizing sets using this model (which has a fixed program) with a stored program model and with Turing machines. The main result, theorem 3, shows the existence of a time complexity hierarchy which is finer than that of any standard abstract computer model. An Algol-like programming language is introduced which facilitates proofs of the theorems.