Totally Correct Logic Program Transformations Via Well-Founded Annotations (Articolo in rivista)

Type
Label
  • Totally Correct Logic Program Transformations Via Well-Founded Annotations (Articolo in rivista) (literal)
Anno
  • 2008-01-01T00:00:00+01:00 (literal)
Alternative label
  • Pettorossi, A.; Proietti, M. (2008)
    Totally Correct Logic Program Transformations Via Well-Founded Annotations
    in Higher-order and symbolic computation (Print)
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Pettorossi, A.; Proietti, M. (literal)
Pagina inizio
  • 193 (literal)
Pagina fine
  • 235 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#numeroVolume
  • 21 (literal)
Rivista
Note
  • SCImago (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • Pettorossi, A. DISP, Università Tor Vergata, Roma (literal)
Titolo
  • Totally Correct Logic Program Transformations Via Well-Founded Annotations (literal)
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 G1 of clauses occurring in P by a new set G2 of clauses, provided that G1 and G2 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. (literal)
Prodotto di
Autore CNR

Incoming links:


Autore CNR di
Prodotto
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#rivistaDi
data.CNR.it