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.

翻译：本文将对带基数约束的有限集合布尔代数($\mathcal{L}_{\lvert\cdot\rvert}$)的判定过程进行扩展，得到$\mathcal{L}_{\lvert\cdot\rvert}$经添加表示有限整数区间的集合项($\mathcal{L}_{[\,]}$)后的扩展版本的判定过程。在$\mathcal{L}_{[\,]}$中，区间边界可以是包含\emph{无界变量}的整数线性项。这些区间是一种有用的扩展，因为它们允许在无量词逻辑中表达非平凡集合算子，例如集合的最小值和最大值。因此，通过为$\mathcal{L}_{[\,]}$提供判定过程，可以自动推理一类新的无量词公式。该判定过程已作为$\{log\}$工具的一部分实现。本文包含一个基于电梯算法的案例研究，表明$\{log\}$能够自动验证所有涉及区间的不变性引理。