Восстановление типов в рефлексивной комбинаторной логике

Рассматривается задача типизации термов средствами предложенной С. Н. Артемовым рефлексивной комбинаторной логики $\mathrm{RCL}_\to$. Доказана единственность восстановления типов, что обосновывает корректность синтаксиса $\mathrm{RCL}_\to$. Доказано, что задачи проверки типизации, полного восстановления типов и распознавания правильно построенных формул для $\mathrm{RCL}_\to$, разрешимы за полиномиальное время.
Библиогр. 4.