A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909008354344960 |
|---|---|
| author | Cristiá, Maximiliano Rossi, Gianfranco |
| author_facet | Cristiá, Maximiliano Rossi, Gianfranco |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2105_03005 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals Cristiá, Maximiliano Rossi, Gianfranco Logic in Computer Science Software Engineering 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. |
| title | A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2105.03005 |