Chapter 4
Deduction
The past is certain, the future obscure.
—Thales of Miletus.
In this Chapter, we will:
- [INTRODUCTION] examine the idea of deciding on the truth of temporal formulae using formal rules and procedures (Section 4.1);
- [TECHNIQUE] introduce the clausal temporal resolution method for proof in PTL (Section 4.2);
- [SYSTEM] describe the TSPASS system which is one of those implementing the clausal temporal resolution approach (Section 4.3); and
- [ADVANCED] highlight a selection of more advanced work including alternative methods and tools (Section 4.4).
Although fewer in number than in previous chapters, exercises will again be interspersed throughout the chapter with solutions provided in Appendix B.
4.1 Temporal Proof
As we saw in the last chapter, we often want to check whether one temporal formula implies another. For example, if we have specified a system using the temporal formula, ψ, then we can check whether a certain temporal property, say φ, follows from the specification of the system by establishing that φ is implied by ψ, that is, whether 
ψ ⇒ φ. This can be achieved by proving that one temporal formula implies another.
There are a variety of mechanisms for deciding proof problems in temporal logic, some of which we will mention in this chapter. However, our main technique will be a variety of clausal resolution for PTL. Before proceeding, it is appropriate ...
