Automated Synthesis of Some Algorithms on Finite Sets

We start from the set theory axioms and we represent sets by monotone lists (sorted lists without duplications). For this, we define a representation function R and its reverse S and we want to synthesize the implementation of the essential corresponding predicates and functions over sets. Each synthesis starts as an inductive constructive proof which applies specific strategies and inference rules. We synthesize (by extracting from proofs) five algorithms among which two predicates: membership and inclusion, and three functions: union, intersection, and difference. In the process of proving we use properties from the theory of sets and we also add other necessary properties in the knowledge base. In this way we explore the theory of sets (represented as monotone lists). The program synthesis and the corresponding theory exploration are carried out in the frame of the Theorem a system. One of the major advantages of our approach is that the algorithms for operating on sets represented as monotone lists are more efficient than the ones for operating on sets represented as non-sorted lists.