Cut for resolution method
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XII, Tome 407 (2012), pp. 111-128
Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

The aim of this talk is to extended Resolution Method by new rule, which simulate cut. We also will obtain upper and lower bounds on the complexity of refutation with and without this rule.
@article{ZNSL_2012_407_a5,
     author = {V. P. Orevkov},
     title = {Cut for resolution method},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {111--128},
     year = {2012},
     volume = {407},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a5/}
}
TY  - JOUR
AU  - V. P. Orevkov
TI  - Cut for resolution method
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2012
SP  - 111
EP  - 128
VL  - 407
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a5/
LA  - ru
ID  - ZNSL_2012_407_a5
ER  - 
%0 Journal Article
%A V. P. Orevkov
%T Cut for resolution method
%J Zapiski Nauchnykh Seminarov POMI
%D 2012
%P 111-128
%V 407
%U http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a5/
%G ru
%F ZNSL_2012_407_a5
V. P. Orevkov. Cut for resolution method. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XII, Tome 407 (2012), pp. 111-128. http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a5/

[1] V. P. Orevkov, Complexity of proofs and their transformations in axiomatic theories, Amer. Math. Soc., 1993 | MR | Zbl

[2] S. K. Klini, Vvedenie v metamatematiku, IL, M., 1957

[3] Ch. Chen, R. Li, Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem, Nauka, M., 1983 | MR