On the lengths of proofs in the propositional calculus (Preliminary Version)

ABSTRACT

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.

REFERENCES

• 1: A note on disjunctive form tautologies, by Bauer, Brand, Fischer, Meyer, and Paterson. SIGACT NEWS, April, 1973.
• 2: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 3: Examples for the Davis-Putnam Procedure, by S.A. Cook. Unpublished manuscript, June, 1971.
• 4: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 5: Theorem testing by computer, by B. Dunham and J.H. North. Proceedings of the Symposium on Mathematical Theory of Automata, Jerome Fox, Editor, pp. 173-177.
• 6: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, by G. Frege, Halle, 1879.
• 7: Principles of Mathematical Logic, by D. Hilbert and W. Ackermann, New York (Chelsea Pub. Co.).
• 8: Reducibility among combinatorial problems, by R.M. Karp, Complexity of Computer Computations, R.E. Miller and J.W. Thatcher, ed., New York (Plenum Press), pp. 85-103.
• 9: Semantic trees in automatic theorem proving, by R. Kowalski and P. Hayes. Machine Intelligence, Vol. 4 (B. Meltzer and D. Michie, eds.), New York, pp. 87-101.
• 10: Introduction to Metamathematics, by S.C. Kleene, (D. Van Nostrand, Inc.).
• 11: Mathematical Logic, by S.C. Kleene, (Wylie).
• 12: Introduction to Mathematical Logic, by Elliott Mendelson, (Van Nostrand).
• 13: A way to simplify truth functions, by W.V. Quine, American Mathematical Monthly, Vol. 62, pp. 627-631.
• 14: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 15: The generalized resolution principle, by J.A. Robinson. Machine Intelligence, Vol. 3 (D. Michie, ed.), American Elsevier, New York, pp. 77-94.
• 16: On the time required by the Davis-Putnam tautology recognition algorithm, by Imre Simon, Research Report CSRR-2050, Department of Applied Analysis and Computer Science, University of Waterloo, Waterloo, Ontario, Canada, June, 1971.
• 17: First order logic, by Raymond M. Smullyan, Springer-Verlag New York Inc.
• 18: On the complexity of derivation in propositional calculus, by G.S. Tseitin, Studies in Constructive Mathematics and Mathematical Logic, Part II, A.O. Slisenko, ed.
• 19: Toward Mechanical Mathematics, by Hao Wong. IBM Journal, Jan. 1960, pp. 2-22.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Theory