Correctness of Logic Program Transformations Based on Existential Termination
Kung-kiu Lau, Mario Ornaghi, Alberto Pettorossi, Maurizio Proietti · The MIT Press eBooks · 1995
We study the relationships between the correctness of logic program transformation and program termination. We consider definite programs and we identify some `invariants' of the program transformation process. The validity of these invariants ensures the preservation of the success set semantics, provided that the existential termination of the initial program implies the existential termination of the final program. We also identify invariants for the preservation of the finite failure set semantics. We consider four very general transformation rules: definition introduction, definition elimination, iff-replacement, and finite failure. Many versions of the transformation rules proposed in the literature, including unfolding, folding, and goal replacement, are instances of the iff-replacement rule. By using our proposed invariants which are based on Clark completion, we prove, for our transformation rules, various results concerning the preservation of both the success set and finite ...