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.
draft