PRL Seminars
Application of Notational Methods in dy/dx
Stuart Allen
March 31, 1998
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.
This work was made into a conference paper From dy/dx to [ ]P: a matter of notation.