Proof Complexities of some Propositional Formulae Classes in Different Refutation Systems

摘要

In this paper the proof complexities of some classes of quasi-hard determinable ( n Tsgf ) and harddeterminable ( n ? ) formulas are investigated in some refutation propositional systems. It is proved that 1) thenumber of proof steps of Tsgfn in R(lin) (Resolution over linear equations) and GCNF'? permutation (cutfreeGentzen type with permutation) systems are bounded by p( n Tsgf 2 log ) for some polynomial p(), 2) theformulas n ? require exponential size proofs in GCNF'? permutation.It is also shown that Frege systems polynomially simulate GCNF'? permutation and any Frege system hasexponential speed-up over the GCNF'? permutation.