Geodesic
Polynomial length proofs for some class of Tseitin formulas
Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 3 (2011), pp. 3-8

Voir la notice de l'article provenant de la source Math-Net.Ru

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. 
@article{UZERU_2011_3_a0,
     author = {A. G. Abajian},
     title = {Polynomial length proofs for some class of {Tseitin} formulas},
     journal = {Proceedings of the Yerevan State University. Physical and mathematical sciences},
     pages = {3--8},
     publisher = {mathdoc},
     number = {3},
     year = {2011},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/UZERU_2011_3_a0/}
}
TY  - JOUR
AU  - A. G. Abajian
TI  - Polynomial length proofs for some class of Tseitin formulas
JO  - Proceedings of the Yerevan State University. Physical and mathematical sciences
PY  - 2011
SP  - 3
EP  - 8
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/UZERU_2011_3_a0/
LA  - en
ID  - UZERU_2011_3_a0
ER  - 
%0 Journal Article
%A A. G. Abajian
%T Polynomial length proofs for some class of Tseitin formulas
%J Proceedings of the Yerevan State University. Physical and mathematical sciences
%D 2011
%P 3-8
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/UZERU_2011_3_a0/
%G en
%F UZERU_2011_3_a0
A. G. Abajian. Polynomial length proofs for some class of Tseitin formulas. Proceedings of the Yerevan State University. Physical and mathematical sciences, no. 3 (2011), pp. 3-8. http://geodesic.mathdoc.fr/item/UZERU_2011_3_a0/