Publications of Maurizio Proietti

This page shows all publications that appeared in the IASI annual research reports. Authors currently affiliated with the Institute are always listed with the full name.

You can browse through them using either the links of the following line or those associated with author names.

Show all publications of the year  ALL, with author Proietti M., in the category IASI Research Reports (or show them all):


IASI Research Report n. 639  (Previous    Next)  

Alberto Pettorossi, Maurizio Proietti

Totally Correct Logic Program Transformations Via Well-Founded Annotations

ABSTRACT
We address the problem of proving the total correctness of transformations of definite logic programs. We consider a general transformation rule, called clause replacement, which consists in transforming a program P into a new program Q by replacing a set ..... of clauses occurring in P by a new set ...... of clauses, provided that ..... and ...... are equivalent in the least Herbrand model M(P) of the program P. We propose a general method for proving that transformations based on clause replacement are totally correct, that is, M(P) = M(Q). Our method consists in showing that the transformation of P into Q can be performed by: (i) adding extra arguments to predicates, thereby deriving from the given program P an annotated program P, (ii) applying a variant of the clause replacement rule and transforming the annotated program P into a terminating annotated program Q, and (iii) erasing the annotations from Q, thereby getting Q. Our method does not require that either P or Q are terminating and it is parametric with respect to the annotations. By providing different annotations we can easily prove the total correctness of program transformations based on various versions of the popular unfolding, folding, and goal replacement rules, which can all be viewed as particular cases of our clause replacement rule. Key words: Program transformation rules, logic programming, partial and total correctness, well-founded orderings.
back
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -