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

TL;DR

The paper addresses inductive proving for equational specifications by formulating a 20-rule inference system that unifies automated simplification with interactive induction under a background theory modulo $B$, including AC/ACU and unit axioms. It introduces advanced techniques—equationally defined equality predicates, narrowing, constructor-variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting, and background-aware ordered rewriting—in a Maude-based framework (NuITP) to automate substantial portions of inductive proofs. Four novel rules (Narrowing Induction ${\bf NI}$, Narrowing Simplification ${\bf NS}$, equality ${\bf Eq}$, and cut ${\bf Cut}$) expand inductive reasoning, while formalizing Skolemization semantics and proving soundness; the system handles quantified formulas via Skolem witnesses and a meta-level rewrite approach. The work demonstrates significant automation for inductive validity checks, supports integration as a backend for other tools, and highlights practical applications (e.g., in Maude NuITP and DM-Check) and future directions toward proof certification and strategy development.

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.