rely solely on depth 1 formulas). Examples of propositional proof systems Some examples of propositional proof systems studied are: Propositional Resolution and various restrictions and extensions of it like DPLL algorithm Natural deduction Sequent calculus Frege system Extended Frege system Polynomial calculus Nullstellensatz system Cutting-plane method Semantic tableau References Further reading Samuel Buss (1998), "An introduction to proof theory", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier (1998). P. Pudlák (1998), "The lengths of proofs", in: Handbook of Proof Theory (ed. S.R.Buss), Elsevier, (1998). P. Beame and T. Pitassi (1998). Propositional proof complexity: past, present and future. Technical Report TR98-067, Electronic Colloquium on Computational Complexity. Nathan Segerlind (2007) "The Complexity of Propositional Proofs", Bulletin of Symbolic Logic 13(4): 417–481 J. Krajíček (1995), Bounded Arithmetic, Propositional Logic, and Complexity Theory, Cambridge University Press. J. Krajíček, Proof complexity, in: Proc. 4th European Congress of Mathematics (ed. A. Laptev), EMS, Zurich, pp. 221–231, (2005). J. Krajíček, Propositional proof complexity I. and Proof complexity and arithmetic. Stephen Cook and Phuong Nguyen, Logical Foundations of Proof Complexity, Cambridge University Press, 2010 (draft from 2008) Robert Reckhow, On the Lengths of Proofs in the Propositional Calculus, PhD Thesis, 1975. External links Proof Complexity Computational complexity theory Logic in computer science Automated theorem proving Propositional calculus Systems of formal logic