Decidability of Term Algebras Extending Partial Algebras

  • Bakhadyr Khoussainov
  • Sasha Rubin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


Let \({\cal A}\) be a partial algebra on a finite signature. We say that \({\cal A}\) has decidable query evaluation problem if there exists an algorithm that given a first order formula \(\phi(\bar{x})\) and a tuple \(\bar{a}\) from the domain of \({\cal A}\) decides whether or not \(\phi(\bar{a})\) holds in \({\cal A}\). Denote by \(E({\cal A})\) the total algebra freely generated by \({\cal A}\). We prove that if \({\cal A}\) has a decidable query evaluation problem then so does \(E({\cal A})\). In particular, the first order theory of \(E({\cal A})\) is decidable. In addition, if \({\cal A}\) has elimination of quantifiers then so does \(E({\cal A})\) extended by finitely many definable selector functions and tester predicates. Our proof is a refinement of the quantifier elimination procedure for free term algebras. As an application we show that any finitely presented term algebra has a decidable query evaluation problem. This extends the known result that the word problem for finitely presented term algebras is decidable.


Word Problem Order Theory Disjunctive Normal Form Ground Term Partial Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: Casl: The Common Algebraic Specification Language. Theoretical Computer Science 286(2), 153–196 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Blumensath, A., Gradel, E.: Automatic structures. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 51–62 (2000)Google Scholar
  3. 3.
    Comon, H.: Complete axiomatization of some quotient term algebras. Theoretical Computer Science 122(1-2), 165–200 (1993)MathSciNetGoogle Scholar
  4. 4.
    Compton, K., Henson, C.: A uniform method for proving lower bounds on computational complexity of logical theories. Annals of Pure and Applied Logic 48, 1–79 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Hodges, W.: Model theory. Cambridge University Press, Cambridge (1993)zbMATHCrossRefGoogle Scholar
  6. 6.
    Khoussainov, B., Rubin, S., Stephan, F.: Automatic Linear Orders and Trees. In: Kolaitis, P.G. (ed.) Transactions on Computational Logic (TOCL) special issue (selected papers from the LICS 2003 conference) (2003) (accepted)Google Scholar
  7. 7.
    Khoussainov, B., Nerode, A.: Automatic Presentations of Structures. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 367–393. Springer, Heidelberg (1995)Google Scholar
  8. 8.
    Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebra with the Knuth-Bendix ordering. In: Proceedings IEEE Conference on Logic in Computer Science, pp. 291–302 (2000)Google Scholar
  9. 9.
    Grätzer, G.: Universal Algebra. D. Van Nostrand Co., Inc., Princeton, N.J.-Toronto, Ont.-London (1968) Google Scholar
  10. 10.
    Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the 9th ACM symposium on theory of computing, pp. 164–177 (1977)Google Scholar
  11. 11.
    Kozen, D.: Partial automata and finitely generated congruences: an extension of Nerode’s theorem. In: Crossley, J., Remmel, J., Shore, R., Sweedler, M. (eds.) Logical methods: in honour of Anil Nerode’s Siztieth Birthday, Birkhauser, pp. 490–511 (1993)Google Scholar
  12. 12.
    Kuncak, V., Rinard, M.C.: Structural sybtyping of non-recursive types is decidable. In: Proceedings IEEE Conference on Logic in Computer Science, pp. 96–107 (2003)Google Scholar
  13. 13.
    Lohrey, M.: Automatic structures of bounded degree. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 346–360. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Maher, M.: A CLP view of logic programming. In: Algebraic and Logic Programming, pp. 364–383 (1992)Google Scholar
  15. 15.
    A. Mal’cev: Axiomatizable classes of locally free algebras of various types. In The Metamathimatics of Algebraic Systems. Anatoliĭ Ivanovic̆ Mal’cev. Collected papers: 1936-1967, B. Wells III, Ed. Vol. 66. North Holland. Chapter 23, 262–281 (1971) Google Scholar
  16. 16.
    Zhang, T., Sipma, H., Manna, Z.: Term algebras with length function and bounded quantifier alternation. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 321–336. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Rybina, T., Voronkov, A.: A Decision procedure for term algebras with queues. ACM Transaction on Computational Logic 2(2), 155–181 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Vorobyov, S.: An improved lower bound for the elementary theories of trees. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 275–287. Springer, Heidelberg (1996)Google Scholar
  19. 19.
    Walukiewicz, I.: Monadic second order logic on tree-like structures. Theoretical computer science 275(1-2), 311–346 (2002)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Bakhadyr Khoussainov
    • 1
  • Sasha Rubin
    • 1
  1. 1.Department of Computer ScienceUniversity of AucklandNew Zealand

Personalised recommendations