On generic representation of implicit induction procedures
Dimitri Naidich · Data Archiving and Networked Services (DANS) · 1996
We develop a generic representation of implicit induction proof procedures within the cover set induction framework. Our work further develops the approach of cover set induction on propositional orderings. We show that in order to represent a substantially wide range of implicit induction procedures it is necessary to generalize the induction on formulas (propositions) to the induction on formula instances. We present a generic induction procedure which captures virtually all the existing implicit induction procedures developed from the inductive completion framework. We establish the formal relationship between the generic induction procedure and the cover set induction scheme. We also demonstrate that the developed generic framework allows for easy generalization/modification of the existing procedures. CR Subject Classification (1991): I.2.3, I.1.3. Keywords & Phrases: automated induction, algebraic specifications, term rewriting. Note: The author was supported by the N...