Some remarks on lengths of propositional proofs. (English) Zbl 0841.03030
Summary: We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depth \(d\) Frege proofs of \(m\) lines can be transformed into depth \(d\) proofs of \(O( m^{d+ 1})\) symbols. We show that renaming Frege proof systems are \(p\)-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed.
Keywords:
survey; lower bounds; Frege proofs; sequent calculus proofs; number of distinct subformulas; propositional proof length; logical flow graphsReferences:
| [1] | Bonet, M.L.: Number of symbols in Frege proofs with and without the deduction rule. In: Clote, P., Krajíček, J. (eds.) Arithmetic, Proof Theory and Computational Complexity, pp. 61–95. Oxford: Oxford University Press 1993 · Zbl 0806.03038 |
| [2] | Bonet, M.L., Buss, S.R.: The deduction rule and linear and near-linear proof simulations. J. Symb. Logic58, 688–709 (1993) · Zbl 0848.03028 · doi:10.2307/2275228 |
| [3] | Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Logic52, 916–927 (1987) · Zbl 0636.03053 · doi:10.2307/2273826 |
| [4] | Buss, S.R.: The undecidability ofk-provability. Ann. Pure Appl. Logic53, 75–102 (1991) · Zbl 0749.03039 · doi:10.1016/0168-0072(91)90059-U |
| [5] | Buss, S.R.: On Gödel’s theorems on lengths of proofs II: Lower bounds for recognizingk symbol provability. In: Clote, P., Remmel, J. (eds.) Feasible Mathematics vol. II, pp. 57–90 Boston: Birkhäuser 1995 · Zbl 0829.03034 |
| [6] | Buss, S.R., et al.: Weak formal systems and connections to computational complexity. Student-written Lecture Notes for a Topics Course at U.C. Berkeley, January–May (1988) |
| [7] | Cejtin, G., Čubarjan, A.: On some bounds to the lengths of logical proofs in classical propositional calculus (Russian). Trudy Vyčisl. Centra AN ArmSSR i Erevan. Univ.8, 57–64 (1975) |
| [8] | Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic44, 36–50 (1979) · Zbl 0408.03044 · doi:10.2307/2273702 |
| [9] | Dowd, M.: Model-theoretic aspects ofP P. Typewritten manuscript (1985) |
| [10] | Krajíček, J.: On the number of steps in proofs. Ann. Pure Appl. Logic41, 153–178 (1989) · Zbl 0672.03042 · doi:10.1016/0168-0072(89)90012-2 |
| [11] | Krajíček, J.: Speed-up for propositional Frege systems via generalizations of proofs. Commentationes Mathematicae Universitatis Carolinae30, 137–140 (1989) · Zbl 0675.03034 |
| [12] | Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first-order theories and the complexity of computations, J. Symb. Logic54, 1063–1079 (1989) · Zbl 0696.03029 · doi:10.2307/2274765 |
| [13] | Krajíček, J., Pudlák, P., Woods, A.: Exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Struct. Algorithms (to appear) · Zbl 0843.03032 |
| [14] | Pitassi, T., Beame, P., Impagliazzo, R.: Exponential lower bounds for the pigeonhole principle. Comput. Complex.3, 97–140 (1993) · Zbl 0784.03034 · doi:10.1007/BF01200117 |
| [15] | Reckhow, R.A.: On the lengths of proofs in the propositional calculus. PhD thesis, Department of Computer Science, University of Toronto, Technical Report #87 (1976) · Zbl 0375.02004 |
| [16] | Statman, R.: Complexity of derivations from quantifier-free Horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems. In: Logic Colloquium ’76, pp. 505–517. Amsterdam: North Holland 1977 · Zbl 0441.03021 |
| [17] | Takeuti, G.: Proof Theory, 2nd edn. Amsterdam: North-Holland 1987 · Zbl 0609.03019 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
