Аннотация:
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.