Application of Notational Methods in dy/dx
by Stuart F. Allen
Stuart Allen will discuss how to apply notational methods familiar from differential calculus, in "dy/dx", to give a simple and natural variant of Kripke-style semantics for modal logic and for first-order temporal logic of programs (Kroeger87).
Modal (temporal) operators are defined, and the the modal (temporal) formulas are identified simply as a subclass of all the expressions.
The notational methods are implemented in Nuprl.