Abstract: | We propose an extension to the rippling technique of [Bundy et al. 93], to improve its suitability for reasoning about theorems specified in terms of relations. The extension broadens the notion of rippling to control proofs by induction over datatypes specified by arbitrary relations. In particular, it will allow synthesis of logic programs from logic-program-like specifications, broadening the possibilities for automated synthesis and transformation of logic programs discussed in [Wiggins 92].
|