基于等式谓词、上下文重写与变体化简的归纳推理
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
AI总结：
本文提出一个基于等式谓词、上下文重写和变体化简的归纳推理系统，20条规则中仅9条需用户交互，其余11条可自动执行，大部分已在Maude的NuITP中实现。
摘要：
本文提出了一个归纳推理系统，用于证明有序分类等式理论 $\mathcal{E}$ 的初始代数 $T_{\mathcal{E}}$ 中公式的有效性。该系统包含20条推理规则，但其中只有9条需要用户交互，其余11条可以作为化简规则自动执行。通过这种方式，证明工作的相当大一部分可以自动化完成。这些推理规则基于先进的等式推理技术，包括：等式定义的等式谓词、窄化、构造子变体合一、变体可满足性、有序分类同余闭包、上下文重写、有序重写以及递归路径序。所有这些技术都在公理 $B$ 模下工作，其中 $B$ 可以是结合性和/或交换性和/或单位元公理的任意组合。这些推理规则中的大多数已经在 Maude 的 NuITP 归纳定理证明器中实现。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
