Specification and proof in membership equational logic

This paper is part of a long-term effort to increase expressiveness of alge braic specification languages while at the same time having a simple semant ic foundation on which efficient execution by rewriting and powerful theore m-proving tools can be based. In particular, our rewriting techniques provi de semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. This effort started in the late 1970s, led b y the ADJ group, who promoted equational logic and universal algebra as the semantic basis of program specification languages. An important later mile stone was the work around order-sorted algebras and the OBJ family of langu ages developed at SRI-International in the 1980s. This effort has been subs tantially advanced in the mid-1990s with the development of Maude, a langua ge based on membership equational logic. Membership equational logic is qui te simple, and yet quite powerful. Its atomic formulae are equations and so rt membership assertions, and its sentences are Horn clauses. It extends in a conservative way both (a version of) order-sorted equational logic and p artial algebra approaches, while Horn logic with equality can be very easil y encoded. After introducing the basic concepts of the logic, we give condi tions and proof rules with which efficient equational deduction by rewritin g can be achieved. We also give completion techniques to transform a specif ication into one meeting these conditions. We address the important issue o f proving that a specification protects a subspecification, a property gene ralizing the usual notion of sufficient completeness. Using tree-automata t echniques, we develop a test-set-based approach for proving inductive theor ems about a parameterized specification. We briefly discuss a number of ext ensions of our techniques, including rewriting module axioms such as associ ativity and commutativity, having extra variables in conditions, and solvin g goals by narrowing. Finally, we discuss the generality of our approach an d how it extends several previous approaches. (C) 2000 Elsevier Science B.V . All rights reserved.