ABSTRACT
This chapter discusses propositional and first-order temporal logic of programs with time corresponding to integers. The logic contains past and future temporal operators. We concentrate mainly on the formal verification of temporal properties. A variety of proof systems is presented in both Hilbert and Gentzen styles. Various notions of soundness and completeness are investigated. We also discuss applications of the logic in the formal specification and verification of properties of algorithms and data structures.
