Self-Learned Formula Synthesis in Set Theory

One of the most difficult tasks in higher-order theorem proving is the instantiation of set variables [ 2, 3 ]. An important class of theorem proving problems requiring instantia tion of a set variable are those requiring induction [ 5 ]. Instantiating a set variable often requires synthesizing a formula satisfying some properties. In our work we apply machine le arning to the task of synthesizing formulas satisfying a collection of semantic properties . Previous work applying machine learning to induction theorem proving can be found in [ 7 ].