Membership algebra as a logical framework for equational specification

This paper proposes membership equational logic—a Horn logic in which the basic predicates are equations t = t′ and membership assertions t : s stating that a term t belongs to a sort s—as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.