A decidable fragment of second order logic with applications to synthesis

P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Science Logic 2018, CSL 2018
EditorsDan R. Ghica, Achim Jung
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Print)9783959770880
DOIs
StatePublished - Aug 1 2018
Event27th Annual EACSL Conference Computer Science Logic, CSL 2018 - Birmingham, United Kingdom
Duration: Sep 4 2018Sep 7 2018

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume119
ISSN (Print)1868-8969

Other

Other27th Annual EACSL Conference Computer Science Logic, CSL 2018
CountryUnited Kingdom
CityBirmingham
Period9/4/189/7/18

Keywords

  • Decidable fragment
  • Second order logic
  • Synthesis

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'A decidable fragment of second order logic with applications to synthesis'. Together they form a unique fingerprint.

  • Cite this

    Madhusudan, P., Mathur, U., Saha, S., & Viswanathan, M. (2018). A decidable fragment of second order logic with applications to synthesis. In D. R. Ghica, & A. Jung (Eds.), Computer Science Logic 2018, CSL 2018 [31] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 119). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2018.31