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