Stepwise, Schema-Guided Logic Algorithm Synthesis

3 Stepwise, Schema-Guided Logic Algorithm Synthesis 

Let s reconsider the strategies of stepwise synthesis of logic algorithms, seen in Section 7.3. An interesting idea, especially with non-incremental stepwise strategies, is then to establish a mapping between steps and the variables of a schema each step synthesizes instance(s) of some predicate- or schema-variable(s) of a given schema. 

Example 8-8 Given Schema 8-3, a possible stepwise strategy would be the following fixed sequence of steps [Rener and Deville 92,93ab]  

Step 2 Synthesis of Minimal mdiNonMinimah Step 3 Synthesis of Decompose,  

We thus advocate a more disciplined approach to algorithm synthesis rather than use a uniform method for instantiating all variables of a given schema (possibly without any awareness of such a schema), one should deploy for each variable the best-suited method. We thus propose to view research on program synthesis as (1) the search for adequate schemas (2) the development of useful methods of predicate-variable instantiation and (3) the discovery of interesting mappings between these methods and the variables of these schemas. 

---