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