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

Let \(\mathcal {L}_\mathcal {X}\) ${\mathcal{L}}_{\mathcal{X}}$ be the language of a first-order, decidable, quantifier-free theory \(\mathcal {X}\) $\mathcal{X}$ . Consider the language, \(\mathcal {L}_\mathcal{R}\mathcal{Q}(\mathcal {X})\) ${\mathcal{L}}_{\mathcal{R}}\mathcal{Q}(\mathcal{X})$ , that extends \(\mathcal {L}_\mathcal {X}\) ${\mathcal{L}}_{\mathcal{X}}$ with formulas of the form \(\forall x \in A: \phi \) $\forall x\in A:\varphi$ (restricted universal quantifier, RUQ) and \(\exists x \in A: \phi \) $\exists x\in A:\varphi$ (restricted existential quantifier, REQ), where A is a finite set and \(\phi \) $\varphi$ is a formula made of \(\mathcal {X}\) $\mathcal{X}$ -formulas, RUQ and REQ. That is, \(\mathcal {L}_\mathcal{R}\mathcal{Q}(\mathcal {X})\) ${\mathcal{L}}_{\mathcal{R}}\mathcal{Q}(\mathcal{X})$ admits nested restricted quantifiers. In this paper we present a decision procedure for some expressive fragments of \(\mathcal {L}_\mathcal{R}\mathcal{Q}(\mathcal {X})\) ${\mathcal{L}}_{\mathcal{R}}\mathcal{Q}(\mathcal{X})$ and its implementation as part of the \(\{log\}\) $\{log\}$ (‘setlog’) tool. The usefulness of the approach is shown by reporting on three real-world case studies.