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

Authors: Hubert Comon-Lundh Marianne Haberstrau Jean-Pierre Jouannaud

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{ComonLundhHaberstra-Decidableproblemsin,
    author = 	 {Hubert Comon-Lundh and Marianne Haberstrau and Jean-Pierre Jouannaud},
    title = 	 {Decidable problems in shallow equational theories},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {255--265},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }