Аннотация:
В данной работе исследуются алгоритмические свойства унаров с разнозначной функцией. Мы доказываем, что теория любого такого унара допускает элиминацию кванторов при подходящем обогащении сигнатуры счётным множеством предикатных символов. Устанавливаются необходимые и достаточные условия для того, чтобы элиминация кванторов была эффективной, и формулируется критерий разрешимости теорий таких унаров. С помощью полученного критерия приводится пример такого унара с разрешимой теорией, что теория унара его подмножеств неразрешима.
Список цитирования
