Specification and proof in membership equational logic

This paper is part of a long-term effort to increase expressiv eness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, wherethey have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both ordersorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification. Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.