A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
share
Let ℒ_𝒳 be the language of first-order, decidable theory 𝒳. Consider the language, ℒ_ℛ𝒬(𝒳), that extends ℒ_𝒳 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 𝒳-formulas, RUQ and REQ. That is, ℒ_ℛ𝒬(𝒳) admits nested restricted quantifiers. In this paper we present a decision procedure for ℒ_ℛ𝒬(𝒳) based on the decision procedure already defined for the Boolean algebra of finite sets extended with restricted intensional sets (ℒ_ℛℐ𝒮). 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.
READ FULL TEXT
