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. 457  (Previous    Next)  

Alberto Pettorossi, Maurizio Proietti

Synthesis and transformation of logic programs using unfold/fold proofs

ABSTRACT
We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfold/fold transformation rules. Given a program P and two goals (that is, conjunctions of atoms)..... and ............, where ...... and .......... are pairwise disjoint vectors of variables, the unfold/fold proof method can be used to show that the equivalence formula ........................................................ holds in the least Herbrand model of P. Equivalence formulas of that form can be used to justify goal replacement steps, which allow us to transform logic programs by replacing old goals, such as ............. by equivalent new goals, such as ............ These goal replacements preserve the least Herbrand model semantics if we find non-ascending unfold/fold proofs of the corresponding equivalence formulas, that is, unfold/fold proofs which ensure suitable well-founded orderings between the successful SLD-derivations of ............ and .................., respectively. We also present a method for program synthesis from implicit definitions. It can be used to derive a definite logic program for the predicate newp implicitly defined by an equivalence formula of the form ................................................................................, such that the predicates occurring in the goals ............. and ............... are defined in a given program P, and newp is a predicate symbol not occurring in P. The set of clauses defining newp, say Eureka, allows us to prove that the above equivalence formula holds in the least Herbrand model of PEureka using an unfold/fold proof. Thus, the correctness of our synthesis method derives from the one of the unfold/fold proof method. We finally illustrate our synthesis method through some examples of program specialization, program synthesis, and program transformation, which can all be viewed as program syntheses from implicit definitions. This paper is an improved version of "Synthesis of Programs from Unfold/Fold Proofs". In: Yves Deville (ed.) Logic Program Synthesis and Transformation, LoPSTr '93, Louvain-la-Neuve, Belgium, Springer-Verlag, Workshops in Computing Series, 1994, 141-158.
back
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -