Specification and Proof in Membership Equational Logic

The goal of this paper is to study in depth a first-order many-kinded Horn language based on equality and unary membership predicates. The language being Horn, the model theory is algebraic, and the axioms can be regarded as rewrite or membership rules which can be fired via pattern matching for the functional subset, and unification for the full language. We investigate a variety of questions relating to the use of the framework as an executable specification language, among which an algebraic semantics validating our deduction rules, the treatment of errors, Church-Rosser properties and completion, sufficient completeness and parameterization. We make an important connection between membership equational signatures and bottom up tree automata with equational constraints. This relationship is exploited for building efficient inductive theorem proving tools. We also show how membership equational logic generalizes many-sorted and order-sorted logic, and that it is indeed Horn complete. We emphasize its conceptual elegance, therefore advocating for membership equational logic as the ultimate algebraic specification language.