Equational Formulas with Membership Constraints

AbstractWe propose a set of transformation rules for first order formulae whose atoms are either equations between terms or "membership constraints" t∈ζ. ζ can be interpreted as a regular tree language (ζ is called a sort in the algebraic specification community) or as a tree language in any class of languages which satisfies some adequate closure and decidability properties. This set of rules is proved to be correct, terminating, and complete. This provides a quantifier elimination procedure: for every regular tree language L, the first order theory of some structure defining L is decidable. This extends the results of several previously published results. We also show how to apply our results to automatic inductive proofs in equational theories