We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: 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{RQ}}(\mathcal{X})$, that extends $\mathcal{L}_{\mathcal{X}}$ with formulas of the form $\forall x \in A: \phi$ (restricted universal quantifier, RUQ) and $\exists x \in A: \phi$ (restricted existential quantifier, REQ), where $A$ is a finite set and $\phi$ is a formula made of $\mathcal{X}$-formulas, RUQ and REQ. That is, $\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ admits nested restricted quantifiers. In this paper we present a decision procedure for $\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ based on the decision procedure already defined for the Boolean algebra of finite sets extended with restricted intensional sets ($\mathcal{L}_\mathcal{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.
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Cite as: arXiv:2208.03518 [cs.LO]
  (or arXiv:2208.03518v1 [cs.LO] for this version)

Submission history

From: Maximiliano Cristia [view email]
[v1] Sat, 6 Aug 2022 13:44:31 GMT (44kb)

Link back to: arXiv, form interface, contact.