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

TL;DR

This paper introduces an inductive inference system that automates a significant portion of proof efforts in equational theories by combining advanced reasoning techniques and contextual rewriting, applicable modulo various axioms.

Contribution

It presents a new inductive inference system with 20 rules, 11 of which are automatable, integrating multiple advanced equational reasoning techniques for improved proof automation.

Findings

Most inference rules are implemented in Maude's NuITP prover.

The system effectively automates proof steps in order-sorted equational theories.

Techniques work modulo axioms like associativity, commutativity, and identity.

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.