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

Abstract

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.