Proof-Based Synthesis of Sorting Algorithms Using Multisets in Theorema

We present a comprehensive case study in the automated synth esis of list sorting algorithms: two main proofs produce the most popular sorting algorithms (min-so rt, quick-sort, insert-sort, merge-sort) and trigger all the proofs necessary for producing the needed au xiliary functions for inserting, splitting, and merging. This is a continuation of our work on exploring in pa rallel the theories of multisets, lists, and binary trees, for the purpose of developing proof method s for the synthesis of algorithms on these domains. In one related paper [12] we already investigated a lgorithms for deletion from lists and binary trees using multisets. We follow the proof-based approach to automated synthesis: first one proves automatically a synthesis conjecture which is based on the specification (input and output conditions) of the desired function, then the algorithm is extracted automatically from the proo f, in form of conditional rewrite rules. The theoretical basis and the correctness of this scheme is well -known [6] and we used earlier in [11, 15].