Interactive Theorem Proving with Temporal Logic

ISSN： 0747-7171

Source： Journal of Symbolic Computation, Vol.23, Iss.4, 1997-04, pp. : 367-397

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

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 of proof by pointing and point and shoot for 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.