1 Search Results for "Saha, Shambwaditya"


Document
A Decidable Fragment of Second Order Logic With Applications to Synthesis

Authors: P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)


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.

Cite as

P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan. A Decidable Fragment of Second Order Logic With Applications to Synthesis. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{madhusudan_et_al:LIPIcs.CSL.2018.31,
  author =	{Madhusudan, P. and Mathur, Umang and Saha, Shambwaditya and Viswanathan, Mahesh},
  title =	{{A Decidable Fragment of Second Order Logic With Applications to Synthesis}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.31},
  URN =		{urn:nbn:de:0030-drops-96987},
  doi =		{10.4230/LIPIcs.CSL.2018.31},
  annote =	{Keywords: second order logic, synthesis, decidable fragment}
}
  • Refine by Author
  • 1 Madhusudan, P.
  • 1 Mathur, Umang
  • 1 Saha, Shambwaditya
  • 1 Viswanathan, Mahesh

  • Refine by Classification
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 decidable fragment
  • 1 second order logic
  • 1 synthesis

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail