带有限整数区间的有限集理论的判定过程

在本文中，我们将带有基数约束的有限集布尔代数（$\mathcal{L}_{\lvert\cdot\rvert}$）的判定过程扩展为对扩展了表示有限整数区间的集合项（$\mathcal{L}_{[\,]}$）的 $\mathcal{L}_{\lvert\cdot\rvert}$ 的判定过程。在 $\mathcal{L}_{[\,]}$ 中，区间端点可以是包含\emph{无界变量}的整数线性项。这些区间是一种有用的扩展，因为它们允许表达诸如集合的最小值和最大值等非平凡集合算子，且仍保持在无量词逻辑中。因此，通过为 $\mathcal{L}_{[\,]}$ 提供判定过程，可以自动推理一类新的无量词公式。该判定过程作为 $\{log\}$ 工具的一部分实现。本文包含一个基于电梯算法的案例研究，表明 $\{log\}$ 可以自动证明所有其不变性引理，其中一些涉及区间。