Морозов А. С., Пономарев Д. К.
О разрешимости проблемы разложимости для конечных теорий

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

Morozov A. S., Ponomaryov D. K.
On decidability of the decomposability problem for finite theories

We consider the decomposability problem for elementary theories, i.e. the problem of deciding whether a theory has a nontrivial representation as a union of two (or several) theories in disjoint signatures. For finite universal Horn theories, we prove that the decomposability problem is Σ₁⁰-complete and, thus, undecidable. We also demonstrate that the decomposability problem is decidable for finite theories in signatures consisting only of monadic predicates and constants.

Полный текст статьи / Full texts:

• PDF file (510 KB)
• PostScript file (950 KB)