Rewriting Induction
Term rewriting can be used in proving theorems by induction. The use of
term rewriting techniques to prove theorems by induction has been known
as "inductionless induction" and "rewriting induction". This node points
to some slides that I made after reading a paper
in CADE-10 by
Uday Reddy .
Reddy's paper describes rewriting induction in a manner that makes the relation to
classical induction clear. My slides give some inference rules that are implicitly present
in Reddy's paper. Reddy's rules are forward chaining. My slides also give a set
of backward chaining rules. A version of these slides were written for Alan Bundy's first induction
workshop (I believe it was at CADE-11 in the summer of 1992).
the slides
David McAllester, March, 1995