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 Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

Abstract: In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints ($\mathcal{L}_{\lvert\cdot\rvert}$) to a decision procedure for $\mathcal{L}_{\lvert\cdot\rvert}$ extended with set terms denoting finite integer intervals ($\mathcal{L}_{[\,]}$). In $\mathcal{L}_{[\,]}$ interval limits can be integer linear terms including \emph{unbounded variables}. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for $\mathcal{L}_{[\,]}$ it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the $\{log\}$ tool. The paper includes a case study based on the elevator algorithm showing that $\{log\}$ can automatically discharge all its invariance lemmas some of which involve intervals.
Comments: arXiv admin note: text overlap with arXiv:2102.05422
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Cite as: arXiv:2105.03005 [cs.LO]
  (or arXiv:2105.03005v1 [cs.LO] for this version)

Submission history

From: Maximiliano Cristia [view email]
[v1] Thu, 6 May 2021 23:35:41 GMT (49kb)

Link back to: arXiv, form interface, contact.