Abstract: In this paper the proof complexities of some classes of quasi-hard determinable (Tsgf n ) and hard determinable (ψ n ) formulas are investigated in some refutation propositional systems. It is proved that 1) the number of proof steps of Tsgf n in R(lin) (Resolution over linear equations) and GCNF'+ permutation (cutfree Gentzen type with permutation) systems are bounded by p( 2 Tsgf n 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 SYSTEMS1

Ashot Abajyan, Anahit Chubaryan

http://www.foibg.com/ijita/vol17/ijita17-3-p07.pdf