Strategic Issues in Rewriting Induction


The rewriting induction (RI) is a method for inductive theorem proving
proposed by Reddy. We present some strategic issues in obtaining
successful proofs in RI. We also present a variant of RI procedure, which
is suitable for trying various strategies in parallel, and discuss the
effectiveness of the procedure with experimental results.