Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914331896053760 |
|---|---|
| author | Nishida, Naoki Nishie, Kazushi Kojima, Misaki |
| author_facet | Nishida, Naoki Nishie, Kazushi Kojima, Misaki |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_14636 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version) Nishida, Naoki Nishie, Kazushi Kojima, Misaki Logic in Computer Science 68Q42 F.4.2 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. |
| title | Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version) |
| topic | Logic in Computer Science 68Q42 F.4.2 |
| url | https://arxiv.org/abs/2602.14636 |