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 \( \sum _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.
Similar content being viewed by others
References
Amir E. and McIlraith S., “Partition-based logical reasoning for first-order and propositional theories” Artificial Intelligence, 162, No. 1–2, 49–88 (2005).
Cuenca Grau B., Horrocks I., Kazakov Y., and Sattler U., “Modular reuse of ontologies: theory and practice” J. Artificial Intelligence Res., 31, 273–318 (2008).
Cuenca Grau B., Horrocks I., Kazakov Y., and Sattler U., Extracting Modules from Ontologies: Theory and Practice, Technical Report, University of Manchester (2007). Available from http://www.cs.man.ac.uk/?ykazakov/publications/abstracts/
Konev B., Lutz C., Walther D., and Wolter F., “Formal properties of modularization” in: H. Stuckenschmidt, C. Parent, and S. Spaccapietra, LNCS Volume on Ontology Modularization, Springer-Verlag, 2008.
Lutz C., Walther D., and Wolter F., “Conservative extensions in expressive description logics” in: Proc. of IJCAI, 2007, pp. 453–458.
Ponomaryov D., “A decomposability criterion for elementary theories” Siberian Math. J., 49, No. 1, 152–154 (2008).
Ponomaryov D., “On decomposability in logical calculi” Bull. Novosibirsk Computing Center, IIS Special Issue 28, 111–120 (2008).
Rogers H., Theory of Recursive Functions and Effective Computability, McGraw-Hill Book Comp., New York, St. Louis, San Francisco, Toronto, London, and Sydney (1972).
Shoenfield J. R., Mathematical Logic, Addison-Wesley, Reading (1967).
Ershov Yu. L. and Palyutin E. A., Mathematical Logic [in Russian], Nauka, Moscow (1987).
Lloyd J. W., Foundations of Logic Programming, Springer-Verlag, New York (1987).
Cohen D. E., Computability and Logic, Ellis Horwood Limited, Chichester (1987).
Chang C. C. and Keisler H. J., Model Theory, North-Holland, Amsterdam etc. (1973).
Ershov Yu. L., Decidability Problems and Constructive Models [in Russian], Nauka, Moscow (1980).
Author information
Authors and Affiliations
Corresponding author
Additional information
Original Russian Text Copyright © 2010 Morozov A. S. and Ponomaryov D. K.
The authors were supported by the Russian Foundation for Basic Research (Grant 05-01-04003-NNIO_a) and DFG project COMO, GZ: 436 RUS 113/829/0-1.
Novosibirsk. Translated from Sibirskiĭ Matematicheskiĭ Zhurnal, Vol. 51, No. 4, pp. 838–847, July–August, 2010.
Rights and permissions
About this article
Cite this article
Morozov, A.S., Ponomaryov, D.K. On decidability of the decomposability problem for finite theories. Sib Math J 51, 667–674 (2010). https://doi.org/10.1007/s11202-010-0068-6
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11202-010-0068-6