[ NOTE: This is being resent because the underlying link in the original message had an extra segment in the path, although the displayed form of the URL was correct. Sorry for any inconvenience. ]
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.
For those who don't use PVS but might be interested in browsing PVS theories, Hypatheon has an operating mode that works without the installation of PVS and its libraries. See the description at the web page above.
Ben Di Vito
NASA Langley Research Center