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/

[1] S.A. Cook, A.R. Reckhow, “The Relative Efficiency of Propositional Proof Systems”, J. Symbolic Logic, 44 (1979), 36–50 | DOI | MR | Zbl

[2] G. S. Tseitin, “On the disjunctive rank of formulas of constructive arithmetic”, Studies in constructive mathematics and mathematical logic. Part II, Zap. Nauchn. Sem. LOMI, 8, “Nauka”, Leningrad. Otdel., Leningrad, 1968, 260–271 (in Russian) | MR | Zbl

[3] Siberian Math. J., 50:2 (2009), 193–198 | DOI | MR | Zbl

[4] J. Soviet Math., 22:3 (1983), 1293–1305 | DOI | MR | Zbl | Zbl

[5] R. Ran, Tz. Iddo, “Resolution over linear equations and multilinear proofs”, Ann. Pure Appl. Logic, 155:3 (2008), 194–224 | DOI | MR | Zbl

[6] P. Pudak, “Lengths of Proofs”, Handbook of Proof Theory, North-Holland, 1998, 547–637 | DOI | MR