Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
<|reference_start|>Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification: 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.<|reference_end|>
@article{meseguer2024inductive,
    title={Inductive Reasoning with Equality Predicates, Contextual Rewriting and
  Variant-Based Simplification},
    author={Jose Meseguer},
    journal={arXiv preprint arXiv:2405.02420},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.02420},
    primaryClass={cs.LO}
}