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.

翻译：本文提出了一种归纳推理系统，用于验证有序排序方程理论 $\mathcal{E}$ 的初始代数 $T_{\mathcal{E}}$ 中公式的有效性。该系统包含20条推理规则，但其中只有9条需要用户交互，其余11条可作为简化规则自动执行。通过这种方式，可以自动化大部分证明工作。这些推理规则基于先进的等式推理技术，包括：等式定义的相等谓词、窄化、构造子变元统一、变元可满足性、有序排序同余闭包、上下文重写、有序重写和递归路径序。所有技术均在公理 $B$ 模下工作，其中 $B$ 是结合性和/或交换性和/或恒等公理的任意组合。这些推理规则中的大多数已在 Maude 的 NuITP 归纳定理证明器中实现。