2026-07-31T03:34:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9698 2024-03-06T10:44:51Z ddc:004 open_access

A Decidable Fragment of Second Order Logic With Applications to Synthesis Madhusudan, P. Mathur, Umang Saha, Shambwaditya Viswanathan, Mahesh second order logic synthesis decidable fragment 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik P. Madhusudan and Umang Mathur and Shambwaditya Saha and Mahesh Viswanathan 2018 Is Part Of LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2018.31 urn:nbn:de:0030-drops-96987 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.31 eng https://creativecommons.org/licenses/by/3.0/legalcode