Abstract:
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 $\Sigma _1^0$-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.
Keywords:
decomposable theory, decomposition of a theory, Horn theory, logic programming, monadic logic.
Citation:
A. S. Morozov, D. K. Ponomaryov, “On decidability of the decomposability problem for finite theories”, Sibirsk. Mat. Zh., 51:4 (2010), 838–847; Siberian Math. J., 51:4 (2010), 667–674
\Bibitem{MorPon10}
\by A.~S.~Morozov, D.~K.~Ponomaryov
\paper On decidability of the decomposability problem for finite theories
\jour Sibirsk. Mat. Zh.
\yr 2010
\vol 51
\issue 4
\pages 838--847
\mathnet{http://mi.mathnet.ru/smj2129}
\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=2732302}
\transl
\jour Siberian Math. J.
\yr 2010
\vol 51
\issue 4
\pages 667--674
\crossref{https://doi.org/10.1007/s11202-010-0068-6}
\isi{https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=Publons&SrcAuth=Publons_CEL&DestLinkType=FullRecord&DestApp=WOS_CPL&KeyUT=000281763300010}
\scopus{https://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-77956293008}
Linking options:
https://www.mathnet.ru/eng/smj2129
https://www.mathnet.ru/eng/smj/v51/i4/p838
This publication is cited in the following 5 articles:
Ponomaryov D., “On the Relationship Between the Complexity of Decidability and Decomposability of First-Order Theories”, Lobachevskii J. Math., 42:12 (2021), 2905–2912
Emelyanov P., Ponomaryov D., “the Complexity of and-Decomposition of Boolean Functions”, Discret Appl. Math., 280 (2020), 113–132
Ponomaryov D., Soutchanski M., “Progression of Decomposed Local-Effect Action Theories”, ACM Trans. Comput. Log., 18:2 (2017), 16
Emelyanov P.G., Ponomaryov D.K., “Algorithmic Issues of and-Decomposition of Boolean Formulas”, Program. Comput. Softw., 41:3 (2015), 162–169
Emelyanov P., Ponomaryov D., “on Tractability of Disjoint and-Decomposition of Boolean Formulas”, Perspectives of System Informatics, Psi 2014, Lecture Notes in Computer Science, 8974, eds. Voronkov A., Virbitskaite I., Springer-Verlag Berlin, 2015, 92–101