Proofs by Program Transformations
Abhik Roychoudhury, I. V. Ramakrishnan · 1999
this paper, we examine how unfolding, folding and goal replacement transformations can be used towards automating the construction of such induction proofs. In [20] we proposed an abstract unfold/fold transformation framework for definite logic programs. We also constructed SCOUT,