A Decidable Fragment of Second Order Logic With Applications to Synthesis

TL;DR

This paper introduces EQSMT, a decidable fragment of second-order logic with an  prefix, enabling effective reasoning for synthesis problems through reduction to SMT solving.

Contribution

The paper defines EQSMT, a new decidable second-order logic fragment suitable for synthesis, and provides a decision procedure leveraging existing SMT solvers for  fragments.

Findings

Decidability of EQSMT satisfiability established.

Reduction of EQSMT to SMT  queries demonstrated.

Applicable to background theories like linear arithmetic.

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. Errata: We have modified the transformation step-2 (page 9) to correct for a slight error. Also, the description above Theorem 10 is different from the published version.