Get started

You will be proposed to look at a simple propositional PVS theory, and re-play a recorded proof scenario for a simple formula of propositional calculus.

The goal is to make you familiar with PVS Emacs interface.