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

2022/08/06 by Maximiliano Cristiá, Cristiá, Maximiliano, Gianfranco Rossi +1
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Engineering (cs.SE)

paper · pdf · doi:10.48550/arxiv.2208.03518

openalex publication_date 2022/08/06 · openalex created_date 2022/10/04 · openalex updated_date 2026/07/28

Abstract

Let L_X be the language of first-order, decidable theory X. Consider the language, L_RQ(X), that extends L_X 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, L_RQ(X) admits nested restricted quantifiers. In this paper we present a decision procedure for L_RQ(X) based on the decision procedure already defined for the Boolean algebra of finite sets extended with restricted intensional sets (L_RIS). 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.

Related

• Automated Reasoning with Restricted Intensional Sets
• A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
• Solving Set Constraints with Comprehensions and Bounded Quantifiers
• On the Syntax of Logic and Set Theory
• Level Two of the Quantifier Alternation Hierarchy over Infinite Words