Bounded Rewriting Induction for LCSTRSs
Kasper Hagens, Cynthia Kop
原文摘要
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.
cs.LO