RUS  ENG
Полная версия
ЖУРНАЛЫ // Труды Математического института имени В. А. Стеклова // Архив

Труды МИАН, 2003, том 242, страницы 136–140 (Mi tm411)

Эта публикация цитируется в 1 статье

Note on a Translation to Characterize Constructivity

M. Baaz

Vienna University of Technology

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

УДК: 510.6

Поступило в октябре 2002 г.

Язык публикации: английский


 Англоязычная версия: Proceedings of the Steklov Institute of Mathematics, 2003, 242, 125–129

Реферативные базы данных:


© МИАН, 2025