The first public release of Hypatheon is now available. Hypatheon is a database capability for indexing PVS
theories and declarations with the goal of making interactive theorem proving more productive. Included is a search engine for finding and selecting desired lemmas along with the ability to invoke them in a proof. The search engine takes the form of a GUI application that runs alongside PVS. It also can run in stand-alone mode without a PVS connection.
The files can be retrieved from this page:
After the upcoming release of PVS 6.0, Hypatheon will be bundled as part of NASA Langley's PVS library distribution. Prospective users who already use the NASA libraries might prefer to wait until then as the setup will be easier. In the meantime, users who would like to try Hypatheon now may download the software and pre-built database files.
Ben Di Vito
NASA Langley Research Center