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