论文部分内容阅读
区间逻辑在许多领域如人工智能，形式化方法中都有成功应用。其中，区间时序逻辑及其各种扩充近年来越来越多地受到人们的重视，由于区间时序逻辑具有较强的表达能力，这也使得该逻辑的定理证明变得相当困难，该文提出了区间时序逻辑的一个标记相继式演算，并给出其可靠性和相对完备性结论。该演算应用于机器辅助定理证明工具中，可以有效地提高证明的自动化程度，在高阶逻辑证明了工具ＰＶＳ中，作者尝试性地实现了这一演算，获得了