Order-sorted equality enrichments modulo axioms ?
We make the addition of equationally defined equality predicates effective and automatic by means of a transformation. The transformation is constructive and valid for a wide class of equational specifications. All the expected good properties of the input theory are preserved by the transformation. The transformation is implemented in Maude and integrated into Maude formal tools.
equality predicate maude order-sorted equational logic modulo axioms algebraic specifications initial algebra semantics