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

Abstract Let LX be the language of first-order, decidable theory X. Consider the language, LRQ(X), that extends LX with formulas of the form ∀ x ∈ A : ϕ (restricted universal quantifier, RUQ) and ∃ x ∈ A : ϕ (restricted existential quantifier, REQ), where A is a finite set and ϕ is a formula made of X-formulas, RUQ and REQ. That is, LRQ(X) admits nested restricted quantifiers. In this paper we present a decision procedure for LRQ(X) based on the decision procedure already defined for the Boolean algebra of finite sets extended with restricted intensional sets (LRIS). 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.