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), a new normal form for ITL formulas which, given a state formula w, features the conditions that the maximal w- and non w-subintervals of an interval satisfying the given formula need to satisfy, the expressibility of 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）的基于区间的反应性范式；一种新的ITL公式范式，该范式在给定状态公式w时，刻画了满足给定公式的区间中最大w子区间与非w子区间所需满足的条件；（Halpern, Manna and Moszkowski, 1983）中时序投影算子逆的表达性；ITL-NL中命题量词的消去；以及由此导出的ITL-NL的一致Craig插值与Beth可定义性。