Application of Notational Methods in dy/dx

by Stuart F. Allen
1997-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.

Application of Notational Methods in dy/dx

by Stuart F. Allen 1997-1998

by Stuart F. Allen
1997-1998