Inductive Reasoning with Equality Predicates, Contextual Rewriting, and Variant-Based Simplification

This paper presents an inductive inference system that combines automated and explicit-induction theorem proving techniques to prove validity of formulas in the initial algebra of an order-sorted equational theory. The system uses advanced equational reasoning techniques, including equationally defined equality predicates, narrowing, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting, and ordered rewriting, all working modulo axioms.