One way to improve software reliability is to use formal methods, which emphasize the design and implementation of provably correct programs and algorithms. However, tackling real applications requires powerful environments that assist programmers in this somewhat tedious proving process. Proof by pointing and point-and-shoot are interactive techniques that use mouse-driven inputs on graphic representations of expressions to conduct such proofs.

This paper shows how such techniques, previously introduced for a simpler first-order intuitionistic logic, can be used in the formal framework of temporal logic. As a proof of concept, a theorem prover for the S4.3 temporal logic, with its two standard operators always and eventually, has been implemented on top of the Centaur graphic environment, using the higher-order logic programming language &lgr;Prolog as the core prover. Both a sequent calculus and a natural deduction system for S4.3 are introduced; they are then mixed together to provide the logic that will eventually be used in the system. A couple of proof examples are provided, in both mathematical and automatically generated “pseudo-English” notations.

Even though this paper is a rather simple extension of the proof by pointing and point-and-shoot techniques, I found it quite interesting (the more involved equivalence proofs are left in an appendix). I recommend it to researchers interested in temporal logic and automatic proof systems.