Transformational Synthesis of Prolog Programs

In order to give a rough feel for transformational synthesis of logic programs, we first present the pioneering mechanism in some detail. Then, we cite the achievements of some of the more recent mechanisms. 

Some of the early efforts were conducted at Imperial College of Science and Technology in Lx)ndon (UK). The developed synthesis mechanisms, called symbolic execution, were inspired by the foundational work on LISP program transformation of [Burstall and Darlington 77]. 

A similar approach was taken by [Hogger 78, 81, 84], though with slight differences. Unfolding is referred to as resolution, which is perfectly adequate and underlines the operational flavor of symbolic execution. More importantly, the induction on some parameter is only introduced as the need arises, and this by strengthening an implicant with a form-identifying atom, such as L = [//IT]. 

Example 2-6 The synthesis of a logic program for membetil goes as follows. As a reminder, the top-level specification is (for convenience, we omit quantifiers)  

Suppose now that parameter L is chosen as the induction parameter. It is a list, so let s perform a symbolic execution for the mutually exclusive symbolic values [] and [//IT]. Let s start with the base case, and apply the substitution L/[] to (1)  

---