区间时序逻辑的标记相继式演算

A LABELED SEQUENT CALCULUS FOR INTERVAL TEMPORAL LOGIC

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

Interval logics have already been seen many successful applications in the fields of the artificial intelligence, formal specification and verification, and so on. Among them, real time Interval Temporal Logic and its various extensions have been given more and more attention recently. Due to their strong expressiveness, theorem proving in these logics is usually not so easy. In this paper, a labeled sequent calculus for Interval Temporal Logic is proposed. Its soundness and relative completeness results are also given. A tool supporting this calculus is implemented in a higher order logic proof checker called PVS. The experiments show that this calculus is very suitable for computer aided theorem prover and can efficiently automate many proof steps.