基于区间的时间分离的应用：反应性范式、逆 $\Pi$、Craig 插值与 Beth 可定义性
计算机科学中的逻辑
2026-02-12 v3
摘要
我们展示了 Moszkowski 离散时间区间时序逻辑（Moszkowski, 1986）的扩展上的基于区间的时间分离（通过邻域模态 ITL-NL）以及在 (Guelev and Moszkowski, 2022) 中建立这种分离形式的关键引理，如何被用于获得简洁证明：(1) 区间形式的反应性范式，如 (Manna and Pnueli, 1990) 所知；(2) 一个新的 ITL 公式范式，该范式给定状态公式 ，刻画了满足给定公式的区间的最大 -子区间和非 -子区间所需满足的条件；(3) (Halpern, Manna and Moszkowski, 1983) 中时间投影算子的逆的可表达性；(4) ITL-NL 中命题量化的消除；以及 (5) ITL-NL 的一致 Craig 插值和 Beth 可定义性。
引用
@article{arxiv.2512.08640,
title = {Applications of Interval-based Temporal Separation: the Reactivity Normal Form, Inverse $\Pi$, Craig Interpolation and Beth Definability},
author = {Dimitar P. Guelev},
journal= {arXiv preprint arXiv:2512.08640},
year = {2026}
}