直到的历史
A History of Until
摘要：
直到是一个非常困难的时间算子，因为它同时是存在的和泛的：A直到B在当前时刻w成立当且仅当B在w成立，或者在未来存在一个时刻w'，B在该时刻成立，并且使得A在当前时刻和w'之间的所有时刻成立。这种“矛盾”的性质在试图为until提供演绎规则时构成了一个重大挑战。相反，在本文中，我们通过引入一个新的时间算子来明确直到的这种对偶性，从而为线性时间逻辑提供表现良好的自然演绎规则，该算子允许我们形式化直到的“历史”，即，在当前1和w '之间的时刻上的“内部”通用量化。这种方法提供了形式化的推理系统的时间逻辑赋予直到运营商的基础。为了具体起见，我们在这里给出了一个标记的自然演绎系统的线性时间逻辑赋予新的运营商，并表明，通过适当的翻译，这样的系统也是健全的和完整的线性时间逻辑LTL与直到。
英文摘要：
Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A until B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and w'. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until to provide well-behaved natural deduction rules for linear-time logics by introducing a new temporal operator that allows us to formalize the "history" of until, i.e., the "internal" universal quantification over the time instants between the current one and w'. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
