The Prototyping Verification System (PVS) developed by Stanford Research Institute (SRI), is an interactive theorem prover for typed higher order logic. PVS is a system for writing specifications and constructing proofs. PVS provides an integrated environment for the development and analysis of formal specifications, and supports a wide range of activities involved in creating, analyzing and documenting theories and proofs.
The aim of this project is to describe the PVS system and re-implement it in Java