A Decidable Fragment of Second Order Logic With Applications to Synthesis

P. Madhusudan, Umang Mathur, Shambwaditya Saha +1

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 $\exis…