Interactive Theorem Proving with Temporal Logic

In this paper, we present a theorem prover for linear temporal logic. Our goal is to extend the capabilities of existing interactive and automatic systems for verifying temporal properties of software and hardware systems. We focus on increasing the effectiveness of user interaction in such systems. In particular, we extend the techniques ofproof by pointingandpoint and shootfor mouse-driven proof construction in first-order logic to temporal logic. In addition, we show how to generate text from proofs by extending a previously given translation for first-order logic to the temporal operators. Our theorem prover implements an inference system for temporal logic that we have defined. The inference rules of this system are more intuitive than the rules commonly given for temporal logics and thus they are better suited to our goals. We present this inference system and prove that it is sound and complete with respect to a known system.