Target Scenarios for SYNAPSE

We now list a few synthesis scenarios that SYNAPSE is targeted to reproduce. Pending the future extensions of the current prototype, these scenarios may not all already be obtained, but the synthesis mechanism is powerful enough to handle these problems. The used problems range from easy plateaulT) to moderately difficult (efface/3) to intricate (sort/2). All the given syntheses are in quiet and manual mode. 

Example 14-4 The synthesis dialogue for the plateau/3 problem proceeds as follows (the actual dialogue is printed in the Courier font synthesizer output precedes colons, whereas user input follows colons the default answers to questions are between curly braces comments on the synthesis are printed in the Times font)  

This ends the specification acquisition. Synthesis now starts with the expansion phase 

The specifier accepts all the default selections. Synthesis now goes fully automatically through the reduction phase (Steps 5 to 7), and yields  

This logic algorithm is totally correct wrt the intended relation. Quite a few atoms can be simplified away (the last two, for instance).  

---