在逻辑约束重写中为存在量词方程重写归纳
Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
AI总结：
本文提出在逻辑约束重写中扩展重写归纳方法，以处理存在量词方程，通过引入存在量词到方程和规则中，实现对约束方程的归纳证明。
摘要：
重写归纳（RI）是一种原则，用于证明一个关于术语的方程是重写系统的归纳定理，即任何该方程的实例都是重写系统的定理。RI已被适应到几种不同的重写系统，并且RI在约束重写系统中已被扩展到不等式。在本文中，我们扩展RI到约束方程中的存在量词方程。为此，我们首先通过在约束方程的方程部分引入存在量词来扩展约束方程。然后，在应用约束重写规则到此类扩展的约束方程时，我们引入存在量词到应用规则的额外变量中。最后，利用扩展的约束重写规则应用，我们将RI扩展到存在量词方程。
英文摘要：
Rewriting Induction (RI) is a principle to prove that an equation over terms is an inductive theorem of a rewrite system, i.e., that any ground instance of the equation is a theorem of the rewrite system. RI has been adapted to several kinds of rewrite systems, and RI for constrained rewrite systems has been extended to inequalities. In this paper, we extend RI for constrained equations to existentially quantified equations in logically constrained rewriting. To this end, we first extend constrained equations by introducing existential quantification to the equation part of constrained equations. Then, in applying a constrained rewrite rule to such extended constrained equations, we introduce existential quantification to extra variables of the applied rule. Finally, using the extended application of constrained rewrite rules, we extend RI for constrained equations to existentially quantified equations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
