A Decidable Fragment of Second Order Logic With Applications to Synthesis
Abstract
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. Errata: We have modified the transformation step-2 (page 9) to correct for a slight error. Also, the description above Theorem 10 is different from the published version.
Cite
@article{arxiv.1712.05513,
title = {A Decidable Fragment of Second Order Logic With Applications to Synthesis},
author = {P. Madhusudan and Umang Mathur and Shambwaditya Saha and Mahesh Viswanathan},
journal= {arXiv preprint arXiv:1712.05513},
year = {2018}
}