A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers

Abstract

Let ${\mathcal{L}}_{\mathcal{X}}$ be the language of first-order, decidable theory $\mathcal{X}$. Consider the language, ${\mathcal{L}}_{\mathcal{R}\mathcal{Q}}(\mathcal{X})$, that extends ${\mathcal{L}}_{\mathcal{X}}$ with formulas of the form $\forall x\in A:\varphi$ (restricted universal quantifier, RUQ) and $\exists x\in A:\varphi$ (restricted existential quantifier, REQ), where $A$ is a finite set and $\varphi$ is a formula made of $\mathcal{X}$-formulas, RUQ and REQ. That is, ${\mathcal{L}}_{\mathcal{R}\mathcal{Q}}(\mathcal{X})$ admits nested restricted quantifiers. In this paper we present a decision procedure for ${\mathcal{L}}_{\mathcal{R}\mathcal{Q}}(\mathcal{X})$ based on the decision procedure already defined for the Boolean algebra of finite sets extended with restricted intensional sets (${\mathcal{L}}_{\mathcal{R}\mathcal{I}\mathcal{S}}$). The implementation of the decision procedure as part of the $\{log\}$ (`setlog') tool is also introduced. The usefulness of the approach is shown through a number of examples drawn from several real-world case studies.