Bounded Rewriting Induction for LCSTRSs
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911356480913408 |
|---|---|
| author | Hagens, Kasper Kop, Cynthia |
| author_facet | Hagens, Kasper Kop, Cynthia |
| contents | Rewriting Induction (RI) is a method to prove inductive theorems, originating from equational reasoning. By using Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate language, rewriting induction becomes a tool for program verification, with inductive theorems taking the role of equivalence predicates. Soundness of RI depends on well-founded induction, and one of the core obstacles for obtaining a practically useful proof system is to find suitable well-founded orderings automatically. Using naive approaches, all induction hypotheses must be oriented within the well-founded ordering, which leads to very strong termination requirements. This, in turn, severely limits the proof capacity of RI. Here, we introduce Bounded RI: an adaption of RI for LCSTRSs where such termination requirements are minimized. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_02803 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Bounded Rewriting Induction for LCSTRSs Hagens, Kasper Kop, Cynthia Logic in Computer Science Rewriting Induction (RI) is a method to prove inductive theorems, originating from equational reasoning. By using Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate language, rewriting induction becomes a tool for program verification, with inductive theorems taking the role of equivalence predicates. Soundness of RI depends on well-founded induction, and one of the core obstacles for obtaining a practically useful proof system is to find suitable well-founded orderings automatically. Using naive approaches, all induction hypotheses must be oriented within the well-founded ordering, which leads to very strong termination requirements. This, in turn, severely limits the proof capacity of RI. Here, we introduce Bounded RI: an adaption of RI for LCSTRSs where such termination requirements are minimized. |
| title | Bounded Rewriting Induction for LCSTRSs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2601.02803 |