Interactive Theorem Proving with Temporal Logic

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 eoeectiveness of user interaction in such systems. In particular, we extend the techniques of proof by pointing and point and shoot for mouse-driven proof construction in ørst-order logic to temporal logic. In addition, we show how to generate text from proofs by extending a previously given translation for ørst-order logic to the temporal operators. Our theorem prover implements an inference system for temporal logic that we have deøned. 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. 1. Introductio