Back to Search
Start Over
A Decidable Fragment of Second Order Logic With Applications to Synthesis
- Publisher :
- Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
-
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.
- Subjects :
- 060201 languages & linguistics
000 Computer science, knowledge, general works
0602 languages and literature
Computer Science
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
06 humanities and the arts
02 engineering and technology
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Accession number :
- edsair.doi...........5d9ccd96f7d99c9a2ea359f76ff1afe8