[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Information and Media Technologies
Online ISSN : 1881-0896
ISSN-L : 1881-0896
Computing
Soundness of Rewriting Induction Based on an Abstract Principle
Takahito Aoto
Author information
JOURNAL FREE ACCESS

2008 Volume 3 Issue 2 Pages 225-235

Details
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.

Content from these authors
© 2008 by Information Processing Society of Japan
Previous article Next article
feedback
Top