Equational Formulae with Membership Constraints

Abstract

We propose a set of transformation rules for first order formulae whose atoms are either equations between terms or "membership constraints" of the form "t in s". s can be interpreted as a regular tree language (s 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 Mal'cev (1962), Maher (1988), Comon and Lescanne (1989). we also show how to apply our results to automatic inductive proofs in equational theories.

paper (.ps version)