Skip to main content
Log in

On decidability of the decomposability problem for finite theories

  • Published:
Siberian Mathematical Journal Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Amir E. and McIlraith S., “Partition-based logical reasoning for first-order and propositional theories” Artificial Intelligence, 162, No. 1–2, 49–88 (2005).

    Article  MATH  MathSciNet  Google Scholar 

  2. 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).

    MATH  MathSciNet  Google Scholar 

  3. 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/

  4. 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.

  5. Lutz C., Walther D., and Wolter F., “Conservative extensions in expressive description logics” in: Proc. of IJCAI, 2007, pp. 453–458.

  6. Ponomaryov D., “A decomposability criterion for elementary theories” Siberian Math. J., 49, No. 1, 152–154 (2008).

    Article  Google Scholar 

  7. Ponomaryov D., “On decomposability in logical calculi” Bull. Novosibirsk Computing Center, IIS Special Issue 28, 111–120 (2008).

    Google Scholar 

  8. Rogers H., Theory of Recursive Functions and Effective Computability, McGraw-Hill Book Comp., New York, St. Louis, San Francisco, Toronto, London, and Sydney (1972).

    MATH  Google Scholar 

  9. Shoenfield J. R., Mathematical Logic, Addison-Wesley, Reading (1967).

    MATH  Google Scholar 

  10. Ershov Yu. L. and Palyutin E. A., Mathematical Logic [in Russian], Nauka, Moscow (1987).

    MATH  Google Scholar 

  11. Lloyd J. W., Foundations of Logic Programming, Springer-Verlag, New York (1987).

    MATH  Google Scholar 

  12. Cohen D. E., Computability and Logic, Ellis Horwood Limited, Chichester (1987).

    MATH  Google Scholar 

  13. Chang C. C. and Keisler H. J., Model Theory, North-Holland, Amsterdam etc. (1973).

    MATH  Google Scholar 

  14. Ershov Yu. L., Decidability Problems and Constructive Models [in Russian], Nauka, Moscow (1980).

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Andrey S. Morozov.

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

Reprints 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

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11202-010-0068-6

Keywords

Navigation