Syntacticness, Cycle-Syntacticness and Shallow Theories

An equational theory is shallow if it can be generated by a finite set of equations whose variables occur at depth at most one. Such a set of equational axioms is called a shallow presentation of the equational theory. We show that shallow theories admit syntactic shallow presentations. Using these presentations, we then design a set of transformation rules for first order formulas over the single predicate symbol = which decides whether such a formula is satisfiable in the Herbrand universe by computing a solved form. The set of rules is shown to be sound, complete, and terminating. Hence, the first order theory of the quotient of the set of finite trees by a shallow theory is decidable when the set of function symbols is finite. This shows in particular that unification in shallow theories is finitary and that there is a uniform unification algorithm finding complete sets of most general unifiers. We think that shallow theories form the largest such subclass of syntactic theories.
full paper