POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS

Author(s)

POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS Ashot Abajian

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).

DOI: 10.46991/PYSUA.2011.45.3.003 Physical and Mathematical Sciences, 45(3 (226) 3-8

Download PDF

Keywords

proof complexity, Split Tree, resolution system, resolution over linear equations, determinative conjunct, quasi-hard determinative formula

Check for updates

Share

Contact admin with any questions, comments or concerns

admin@thegufo.com