We show how interval-based temporal separation on the extension of Moszkowski's discrete time interval temporal logic (Moszkowski, 1986) by the neighbourhood modalities (ITL-NL) and a lemma which is key in establishing this form of separation in (Guelev and Moszkowski, 2022) can be used to obtain concise proofs of an interval-based form of the reactivity normal form as known from (Manna and Pnueli, 1990), the inverse of the temporal projection operator from (Halpern, Manna and Moszkowski, 1983), the elimination of propositional quantification in ITL-NL and, consequently, uniform Craig interpolation and Beth definability for ITL-NL.

翻译：我们展示了如何在Moszkowski离散时间区间时序逻辑（Moszkowski, 1986）的扩展——即通过邻域模态增强的区间时序逻辑（ITL-NL）——上应用基于区间的时间分离方法，并结合（Guelev and Moszkowski, 2022）中确立该分离形式的关键引理，以简洁地证明以下结果：源自（Manna and Pnueli, 1990）的基于区间的反应性范式形式、（Halpern, Manna and Moszkowski, 1983）中时间投影算子的逆、ITL-NL中命题量词的消除，以及由此导出的ITL-NL的一致Craig插值定理和Beth可定义性定理。