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

Keywords: determinative conjunct, hard determinable formula, quasi-hard determinable formula, proof complexity, refutation system, polynomial simulation.

ACM Classification Keywords: F.4.1 Mathematical Logic and Formal Languages, Mathematical Logic, Proof theory

Link:

PROOF COMPLEXITIES OF SOME PROPOSITIONAL FORMULAE CLASSES IN DIFFERENT REFUTATION SYSTEMS

Ashot Abajyan, Anahit Chubaryan

http://www.foibg.com/ijita/vol19/ijita19-4-p06.pdf