Some remarks on lengths of propositional proofs

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

Bonet, M.L., Buss, S.R.: The deduction rule and linear and near-linear proof simulations. J. Symb. Logic58, 688–709 (1993)

Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Logic52, 916–927 (1987)

Buss, S.R.: The undecidability ofk-provability. Ann. Pure Appl. Logic53, 75–102 (1991)

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

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)

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)

Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic44, 36–50 (1979)

Dowd, M.: Model-theoretic aspects ofP ≠NP. Typewritten manuscript (1985)

Krajíček, J.: On the number of steps in proofs. Ann. Pure Appl. Logic41, 153–178 (1989)

Krajíček, J.: Speed-up for propositional Frege systems via generalizations of proofs. Commentationes Mathematicae Universitatis Carolinae30, 137–140 (1989)

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)

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)

Pitassi, T., Beame, P., Impagliazzo, R.: Exponential lower bounds for the pigeonhole principle. Comput. Complex.3, 97–140 (1993)

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)

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

Takeuti, G.: Proof Theory, 2nd edn. Amsterdam: North-Holland 1987