首页    期刊浏览 2024年12月05日 星期四
登录注册

文章基本信息

  • 标题:A Decidable Fragment of Second Order Logic With Applications to Synthesis
  • 本地全文:下载
  • 作者:P. Madhusudan ; Umang Mathur ; Shambwaditya Saha
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:119
  • 页码:1-19
  • DOI:10.4230/LIPIcs.CSL.2018.31
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:second order logic; synthesis; decidable fragment
国家哲学社会科学文献中心版权所有