Skip to main content
SpringerLink
Log in

An improved lower bound for the elementary theories of trees

  • Session 4A
  • Conference paper
  • First Online:
Automated Deduction — Cade-13 (CADE 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1104))

Included in the following conference series:

Abstract

The first-order theories of finite and rational, constructor and feature trees possess complete axiomatizations and are decidable by quantifier elimination [15, 13, 14, 5, 10, 3, 20, 4, 2]. By using the uniform inseparability lower bounds techniques due to Compton and Henson [6], based on representing large binary relations by means of short formulas manipulating with high trees, we prove that all the above theories, as well as all their subtheories, are non-elementary in the sense of Kalmar, i.e., cannot be decided within time bounded by a k-story exponential function exp k (n) for any fixed k. Moreover, for some constant d>0 these decision problems require nondeterministic time exceeding exp∞ (⌊dn⌋) infinitely often.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Aït-Kaci, A. Podelski, and G. Smolka. A feature constraint system for logic programming with entailment. Theor. Comput. Sci., 122:263–283, 1994. Preliminary version: 5th Intern. Conf. Fifth Generation Computer Systems, June 1992.

    Article  Google Scholar 

  2. R. Backofen. A complete axiomatization of a theory with feature and arity constraints. J. Logic Programming, 24:37–71, 1995.

    Article  Google Scholar 

  3. R. Backofen and G. Smolka. A complete and recursive feature theory. Theor. Comput. Sci., 146:243–268, 1995. Also: Report DFKI-RR-92-30, 1992.

    Article  Google Scholar 

  4. R. Backofen and R. Treinen. How to win a game with features. In Constraints in Computational Logics'94, volume 845 of Lect. Notes Comput. Sci., pages 320–335. Springer-Verlag, 1994.

    Google Scholar 

  5. H. Comon and P. Lescanne. Equational problems and disunification. J. Symb. Computation, 7:371–425, 1989.

    Google Scholar 

  6. K. J. Compton and C. W. Henson. A uniform method for proving lower bounds on the computational complexity of logical. theories. Annals Pure Appl. Logic, 48:1–79, 1990.

    Article  Google Scholar 

  7. Yu. L. Ershov, I. A. Lavrov, A. D. Taimanov, and M. A. Taitslin. Elementary theories. Russian Math. Surveys, 20:35–105, 1965.

    Google Scholar 

  8. J. Ferrante and C. W. Rackoff. The computational complexity of logical theories, volume 718 of Lect. Notes Math. Springer-Verlag, 1979.

    Google Scholar 

  9. M. J. Fisher and M. O. Rabin. Super-exponential complexity of Presburger arithmetic. In SIAM-AMS Proceedings, volume 7, pages 27–41, 1974.

    Google Scholar 

  10. W. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and its Applications. Cambridge Univ. Press, 1993.

    Google Scholar 

  11. J. Jaffar and M. J. Maher. Constraint logic programming: A survey. J. Logic Programming, 19 & 20:503–581, 1994.

    Article  Google Scholar 

  12. K. Kunen. Answer sets and negation as failure. In J.-L. Lassez, editor, 4th International Conference on Logic Programming, volume 1, pages 219–228. MIT Press, 1987.

    Google Scholar 

  13. K. Kunen. Negation in logic programming. J. Logic Programming, 4:289–308, 1987.

    Article  Google Scholar 

  14. M. J. Maher. Complete axiomatizations of the algebras of finite, rational, and infinite trees. In 3rd Annual IEEE Symp. on Logic in Computer Science LICS'88), pages 348–357, 1988.

    Google Scholar 

  15. A. I. Malcev. Axiomatizable classes of locally free algebras. In B. F. Wells, editor, The Metamathematics of Algebraic Systems (Collected Papers: 1936–1967), volume 66 of Studies in Logic and the Foundations of Mathematics, chapter 23, pages 262–281. North-Holland Pub. Co., 1971.

    Google Scholar 

  16. A. R. Meyer. Weak monadic second-order theory of successor is not elementaryrecursive. In R. Parikh, editor, Logic Colloquium: Symposium on Logic Held at Boston, 1972–1973, volume 453 of Lect. Notes Math., pages 132–154. Springer-Verlag, 1975.

    Google Scholar 

  17. P. Odifreddi. Classical recursion theory, volume 125 of Studies in Logic and the Foundations of Mathematics. North-Holland Pub. Co., 1989. Second Edition, 1992.

    Google Scholar 

  18. J. I. Seiferas, M. J. Fisher, and A. R. Meyer. Separating nondeterministic time complexity classes. J. ACM, 25(1):146–167, 1978.

    Article  Google Scholar 

  19. G. Smolka. Feature constraint logics for unification grammars. J. Logic Programming, 12:51–87, 1992.

    Article  Google Scholar 

  20. G. Smolka and R. Treinen. Records for logic programming. J. Logic Programming, 18:229–258, 1994. Also: Report DFKI-RR-92-23, 1992.

    Article  Google Scholar 

  21. R. M. Smullyan. Theory of Formal Systems. Princeton University Press, revised edition, 1961.

    Google Scholar 

  22. L. J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, MIT Lab for Computer Science, 1974. (Also /MIT/LCS Tech Rep 133).

    Google Scholar 

  23. L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time: preliminary report. In 5th Symp. on Theory of Computing, pages 1–9, 1973.

    Google Scholar 

  24. S. Vorobyov. Theory of finite trees revisited: Application of model-theoretic algebra. Technical Report CRIN-94-R-135, Centre de Recherche en Informatique de Nancy, October 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, D-66123, Saarbrücken, Germany

    Sergei Vorobyov

Authors
  1. Sergei Vorobyov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vorobyov, S. (1996). An improved lower bound for the elementary theories of trees. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_91

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_91

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61511-8

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation