  An inductive inference system for proving validity of formulas in the initial
algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is
presented. It has 20 inference rules, but only 9 of them require user
interaction; the remaining 11 can be automated as simplification rules. In this
way, a substantial fraction of the proof effort can be automated. The inference
rules are based on advanced equational reasoning techniques, including:
equationally defined equality predicates, narrowing, constructor variant
unification, variant satisfiability, order-sorted congruence closure,
contextual rewriting, ordered rewriting, and recursive path orderings. All
these techniques work modulo axioms $B$, for $B$ any combination of
associativity and/or commutativity and/or identity axioms. Most of these
inference rules have already been implemented in Maude's NuITP inductive
theorem prover.
