О разрешимости проблемы разложимости для конечных теорий

Рассматривается проблема разложимости элементарных теорий – алгоритмическая проблема нетривиального представления теории в виде объединения двух (или более) теорий дизъюнктных сигнатур. Доказаны $\Sigma^0_1$-полнота и, как следствие, алгоритмическая неразрешимость проблемы разложимости конечных хорновых универсальных теорий, а также разрешимость проблемы разложимости для конечных теорий в сигнатуре, содержащей только одноместные предикаты и символы констант.