An Equational Deductive System for Linear Temporal Logic (Student) David Vega

This paper presents an equational deductive system for linear temporal logic. It differs from previous developments of temporal logic in several respects. First, the proofs are given in the equational logic developed by Dijkstra and Scholten as opposed to the older Hilbert-style logics. Second, it presents several new and interesting linear temporal theorems, including the associative properties of the until operator. Third, although space limitations preclude giving a proof of every theorem in this paper, every theorem has been proved with equational logic. The summary of equational logic is minimal, and the paper can serve as an introduction to linear temporal logic for those already familiar with equational logic.