Geodesic
Note on a~Translation to Characterize Constructivity
Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 136-140.

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

This note describes a straightforward translation $\mathcal C^{(1)}$ such that $T\vdash A(t)$ for some term $t$ $\Leftrightarrow$ $\mathcal C^{(1)}(T)\vdash \mathcal C^{(1)}(\exists xA(x))$ for universal $T$ and purely existential $\exists xA(x)$. The correspondence is based on the properties of resolution calculus. 
@article{TRSPY_2003_242_a10,
     author = {M. Baaz},
     title = {Note on {a~Translation} to {Characterize} {Constructivity}},
     journal = {Informatics and Automation},
     pages = {136--140},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a10/}
}
TY  - JOUR
AU  - M. Baaz
TI  - Note on a~Translation to Characterize Constructivity
JO  - Informatics and Automation
PY  - 2003
SP  - 136
EP  - 140
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a10/
LA  - en
ID  - TRSPY_2003_242_a10
ER  - 
%0 Journal Article
%A M. Baaz
%T Note on a~Translation to Characterize Constructivity
%J Informatics and Automation
%D 2003
%P 136-140
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a10/
%G en
%F TRSPY_2003_242_a10
M. Baaz. Note on a~Translation to Characterize Constructivity. Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 136-140. http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a10/

[1] Takeuti G., Proof theory, North-Holland, Amsterdam, 1987 | MR | Zbl

[2] Troelstra A., van Dalen D., Constructivism in mathematics. An introduction, v. 1, North-Holland, Amsterdam, 1988

[3] Leitsch A., The resolution calculus, Texts Theor. Comput. Sci., Springer, Berlin, 1997 | MR