Report Number: CS-TR-86-1109
Institution: Stanford University, Department of Computer Science
Title: A proof editor for propositional temporal logic
Author: Casley, Ross
Date: May 1986
Abstract: This report describes PTL, a program to assist in constructing proofs in propositional logic extended by the operators $\Box$ ("always"), $\Diamond$ ("eventually") and $\bigcirc$ ("at the next step"). This is called propositional temporal logic and is one of two systems of logic presented by Abadi and Manna in [1].
http://i.stanford.edu/pub/cstr/reports/cs/tr/86/1109/CS-TR-86-1109.pdf