Back to Search
Start Over
A Decidable Fragment of Second Order Logic With Applications to Synthesis
- Source :
- 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), http://drops.dagstuhl.de/opus/volltexte/2018/9698
- Publication Year :
- 2017
-
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 $\exists^*\forall^*$ 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 $\exists^*\forall^*$ FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of $\exists^*\forall^*$ formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting $\exists^*\forall^*$ 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.
Details
- Database :
- arXiv
- Journal :
- 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), http://drops.dagstuhl.de/opus/volltexte/2018/9698
- Publication Type :
- Report
- Accession number :
- edsarx.1712.05513
- Document Type :
- Working Paper
- Full Text :
- https://doi.org/10.4230/LIPIcs.CSL.2018.31