← 研踪 PaperTrailarXiv:2601.02803 · v2
Bounded Rewriting Induction for LCSTRSs
首次提交 2026-01-06 16:26
版本更新 2026-11-05 20:24
雷达观测 2026-11-06 12:09
摘要
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. Traditionally, RI can be used not only to prove equivalence, but also to establish ground confluence. Moreover, for ground confluent TRSs, RI can be extended to a system for disproving inductive theorems. We will show that this is also possible with Bounded RI.
作者备注：57 pages, 4 figures, submitted to LMCS
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-05 20:24 · 最新观测版本
Bounded Rewriting Induction for LCSTRSs
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. Traditionally, RI can be used not only to prove equivalence, but also to establish ground confluence. Moreover, for ground confluent TRSs, RI can be extended to a system for disproving inductive theorems. We will show that this is also possible with Bounded RI.
查看此版本解读 →查看此版本原文 ↗