POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS

A.G. Abajyan

doi:10.46991/PYSU:A/2011.45.3.003

POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS

Authors

A.G. Abajyan Chair of Discrete Mathematics and Theoretical Informatics, YSU, Armenia

DOI:

https://doi.org/10.46991/PYSU:A/2011.45.3.003

Keywords:

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

Abstract

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

Downloads

Published

2011-10-17

How to Cite

Abajyan, A. (2011). POLYNOMIAL LENGTH PROOFS FOR SOME CLASS OF TSEITIN FORMULAS. Proceedings of the YSU A: Physical and Mathematical Sciences, 45(3 (226), 3–8. https://doi.org/10.46991/PYSU:A/2011.45.3.003