PVS Theorem Proving Enhancements.
Natarajan Shankar · 1997
Abstract : The goal of the project was to augment PVS with features that simplified the construction and management of proofs, and to document the PVS functions needed for writing proof strategies. The extensions to PVS developed in this project include: (1) Multiple-proof maintenance, (2) Comments in proofs, (3) Labeling and accessing sequent formulas, (4) Rerunning proofs with checkpoints, (5) Deconstructing EXPAND, and (6) Saved SKIP command.