to be fairly strong systems. Unlike, say, resolution, there are no known superlinear lower bounds on the number of lines in Frege proofs, and the best known lower bounds on the size of the proofs are quadratic. The minimal number of rounds in the prover-adversary game needed to prove a tautology is proportional to the logarithm of the minimal number of steps in a Frege proof of . Extended Frege system An important extension of a Frege system, the so called Extended Frege, is defined by taking a Frege system F and adding an extra derivation rule which allows to derive formula , where abbreviates its definition in the language of the particular F and the atom does not occur in previously derived formulas including axioms and in the formula . The purpose of the new derivation rule is to introduce 'names' or shortcuts for arbitrary formulas. It allows to interpret proofs in Extended Frege as Frege proofs operating with circuits instead of formulas. Cook's correspondence allows to interpret Extended Frege as a nonuniform equivalent of Cook's theory PV and Buss's theory formalizing feasible (polynomial-time) reasoning. References Krajíček, Jan (1995). "Bounded Arithmetic, Propositional Logic, and Complexity Theory", Cambridge University Press. Buss, S. R. (1987). "Polynomial size proofs of the propositional pigeonhole principle", Journal of Symbolic Logic 52, pp. 916–927. Pudlák, P., Buss, S. R. (1995). "How to lie without being (easily) convicted and the lengths of proofs in propositional calculus", in: Computer Science Logic'94 (Pacholski and Tiuryn eds.), Springer LNCS 933, 1995, pp. 151–162. Propositional calculus Logic in computer science