Logic in Computer Science (LICS 1992)

Paper: Decidable problems in shallow equational theories (at LICS 1992)

Authors: Comon, H. Haberstrau, M. Jouannaud, J.-P.

Abstract

Results for syntactic theories are generalized to shallow theories. The main technique used is the computation by ordered completion techniques of conservative extensions of the starting shallow presentation which are, respectively, ground convergent, syntactic, and cycle-syntactic. In all cases, the property that variables occur at depth at most one appears to be crucial. shallow theories thus emerge as a fundamental nontrivial, union-closed subclass of equational theories for which all important questions are decidable

BibTeX

  @InProceedings{ComonHaberstrauJoua-Decidableproblemsin,
    author = 	 {Comon, H. and Haberstrau, M. and Jouannaud, J.-P.},
    title = 	 {Decidable problems in shallow equational theories},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {255--265},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }