Soundness of Rewriting Induction Based on an Abstract Principle

Citations Over TimeTop 15% of 2008 papers

Abstract

Rewriting induction (Reddy, 1990) is a method to prove inductive theorems of term rewriting systems automatically. Koike and Toyama(2000) extracted an abstract principle of rewriting induction in terms of abstract reduction systems. Based on their principle, the soundness of the original rewriting induction system can be proved. It is not known, however, whether such an approach can be adapted also for more powerful rewriting induction systems. In this paper, we give a new abstract principle that extends Koike and Toyama's abstract principle. Using this principle, we show the soundness of a rewriting induction system extended with an inference rule of simplification by conjectures. Inference rules of simplification by conjectures have been used in many rewriting induction systems. Replacement of the underlying rewriting mechanism with ordered rewriting is an important refinement of rewriting induction — with this refinement, rewriting induction can handle non-orientable equations. It is shown that, based on the introduced abstract principle, a variant of our rewriting induction system based on ordered rewriting is sound, provided that its base order is ground-total. In our system based on ordered rewriting, the simplification rule extends those of the equational fragment of some major systems from the literature.

Related Papers

• → Development closed critical pairs(1996)18 cited
• → Checking Overlaps of Nominal Rewriting Rules(2016)9 cited
• → Proving and disproving confluence of context-sensitive rewriting(2022)3 cited
• → Completion of Globally Finite Term Rewriting Systems for Inductive Proofs(1986)6 cited
• → Confluence of Right Ground Term Rewriting Systems Is Decidable(2005)4 cited