Sciweavers

Share
ICLP
2007
Springer

Automatic Correctness Proofs for Logic Program Transformations

11 years 6 months ago
Automatic Correctness Proofs for Logic Program Transformations
Abstract. The many approaches which have been proposed in the literature for proving the correctness of unfold/fold program transformations, consist in associating suitable well-founded orderings with the proof trees of the atoms belonging to the least Herbrand models of the programs. In practice, these orderings are given by ‘clause measures’, that is, measures associated with the clauses of the programs to be transformed. In the unfold/fold transformation systems proposed so far, clause measures are fixed in advance, independently of the transformations to be proved correct. In this paper we propose a method for the automatic generation of the clause measures which, instead, takes into account the particular program transformation at hand. During the transformation process we construct a system of linear equations and inequations whose unknowns are the clause measures to be found, and the correctness of the transformation is guaranteed by the satisfiability of that system. Thro...
Alberto Pettorossi, Maurizio Proietti, Valerio Sen
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where ICLP
Authors Alberto Pettorossi, Maurizio Proietti, Valerio Senni
Comments (0)
books