POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS - Abajyan, A.G. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2011)
In this paper the notion of quasi-hard determinative formulas is introduced and the proof complexities of such formulas are investigated. For some class of quasi-hard determinative formulas the same order lower and upper bounds for the length of proofs are obtained in several proof systems, basing on disjunctive normal forms (conjunctive normal forms).
Keywords: proof complexity; Split Tree; resolution system; resolution over linear equations; determinative conjunct; quasi-hard determinative formula