Geodesic
Weak constructive second order arithmetic with extracting polynomial time computable algorithms
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VIII, Tome 304 (2003), pp. 7-12

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

A family of weak constructive theories is built in this work. The theories contain arithmetic and a theory of natural valued functions with natural arguments. These functions are polynomially bounded and are computable in a time polynomially bounded in values of their arguments. Theory languages contain functional constants for addition, and multiplication and equality predicate. Other functional constants also may be used if their functions satisfy the polynomial boundedness conditions above. Polynomial time computable (in numeric values of the arguments) witness functions for proved formulas can be algorithmically extracted from the proofs of these theories. If one of the arguments of witness is a function, then this function is used in the witness algorithm as an oracle. 
@article{ZNSL_2003_304_a1,
     author = {A. P. Beltiukov},
     title = {Weak constructive second order arithmetic with extracting polynomial time computable algorithms},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {7--12},
     publisher = {mathdoc},
     volume = {304},
     year = {2003},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a1/}
}
TY  - JOUR
AU  - A. P. Beltiukov
TI  - Weak constructive second order arithmetic with extracting polynomial time computable algorithms
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2003
SP  - 7
EP  - 12
VL  - 304
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a1/
LA  - ru
ID  - ZNSL_2003_304_a1
ER  - 
%0 Journal Article
%A A. P. Beltiukov
%T Weak constructive second order arithmetic with extracting polynomial time computable algorithms
%J Zapiski Nauchnykh Seminarov POMI
%D 2003
%P 7-12
%V 304
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a1/
%G ru
%F ZNSL_2003_304_a1
A. P. Beltiukov. Weak constructive second order arithmetic with extracting polynomial time computable algorithms. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part VIII, Tome 304 (2003), pp. 7-12. http://geodesic.mathdoc.fr/item/ZNSL_2003_304_a1/