Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-21T23:59:51.919Z Has data issue: false hasContentIssue false
  • English
  • Français

The relative efficiency of propositional proof systems

Published online by Cambridge University Press:  12 March 2014

Stephen A. Cook  and
Robert A. Reckhow
Stephen A. Cook
Affiliation:
Department of Computer Science, University of Toronto, Toronto, CanadaM5S 1A7
Robert A. Reckhow
Affiliation:
Department of Computing Science, University of Alberta, Edmonton, CanadaT6G 2E1
Get access Rights & Permissions [Opens in a new window]

Extract

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.

In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 44 , Issue 1 , March 1979 , pp. 36 - 50
Copyright
Copyright © Association for Symbolic Logic 1979

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Cook, S. A. and Reckhow, R. A., On the lengths of proofs in the propositional calculus, Preliminary version, Proceedings of the Sixth Annual ACM Symposium on the Theory of Computing, May 1974, pp. 135–148. (See also corrections for the above in SIGACT News, vol. 6(1974), pp. 15–22.)Google Scholar
[2]Reckhow, R. A., On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976.Google Scholar
[3]Cook, S. A., The complexity of theorem proving procedures, Proceedings of the Third Annual ACM Symposium on the Theory of Computing, May 1971, pp. 151–158.Google Scholar
[4]Karp, R. M., Reducibility among combinatorial problems, Complexity of computer computations (Miller, R. E. and Thatcher, J. W., Editors), Plenum Press, NY, 1972, pp. 85–103.CrossRefGoogle Scholar
[5]Aho, A. V., Hopcroft, J.E. and Ullman, J. D., The design and analysis of computer algorithms, Addison-Wesiey, Reading, Massachusetts, 1974.Google Scholar
[6]Frege, G., Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle, 1879. English translation in From Frege to Godel, a source book in mathematical logic (van Heijenoort, J., Editor), Harvard University Press, Cambridge, 1967, pp. 1–82.Google Scholar
[7]Prawitz, D., Natural deduction. A proof-theoretic study, Stockholm, 1965.Google Scholar
[8]Tseitin, G. S., On the complexity of derivations in propositional calculus, Studies in mathematics and mathematical logic, Part II (Slisenko, A. O., editor), 1968, pp. 115–125. (Translated from Russian)Google Scholar
[9]Cook, S. A., Rackoff, C. W.et al, Lecture notes for CSC2429F, “Topics in the theory of computation”, a course presented by the Department of Computer Science, University of Toronto during the fall, 1976.Google Scholar
[10]Statman, R., Complexity of derivations from quantifier-free horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems, Proceedings of Logic Colloquium '76 (Gandy, and Hyland, , Editors), Studies in Logic and Foundations of Mathematics, vol. 87(1977), North-Holland, Amsterdam.Google Scholar
[11]Cook, S. A., Feasibly constructive proofs and the propositional calculus, Proceedings of the Saventh Annual ACM Conference on the Theory of Computing, May 1976, pp. 83–97.Google Scholar
[12]Church, A., Introduction to mathematical logic, vol. I, Princeton University Press, Princeton, 1956.Google Scholar
[13]von Neumann, J., Zur Hilbertschen Beweistheorie, Mathematische Zeitschrift, vol. 26 (1927), pp. 1–46.CrossRefGoogle Scholar