A decidable fragment of second order logic with applications to synthesis

We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an ∃∗∀∗ quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the ∃∗∀∗ FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of ∃∗∀∗ formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting ∃∗∀∗ reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT ) reasoning.