NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

    • Hypatheon: A Database Capability for PVS Theories

    Theories and libraries for PVS have grown considerably over the last few years. While these theories are helpful, their growth has created the problem of locating and selecting suitable declarations from the thousands available. In response, we have developed a database capability called Hypatheon to index PVS theories and declarations.

    Hypatheon's aim is to make interactive theorem proving in PVS 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.

    Development has been conducted at NASA Langley Research Center. The software is released under the terms of the NASA Open Source Agreement (included with the distribution). Feedback of any kind is encouraged so that it might be improved.

    Hypatheon was named for Hypatia and her father Theon, early mathematicians who were the last scholars to preside over the ancient Library of Alexandria.

    A Note on Library Terminology

    For various reasons, the term “PVS library” has undergone some evolution. The original meaning is a named collection of related PVS theories all residing within a single directory. Recent usage refers to the “NASA PVS Library” as a “collection of formal developments,” where each “formal development” is realized by a collection of theories. This newer usage places “Library” at a higher level. Hypatheon, though, was developed with the original library meaning and has retained that terminology. Please be mindful that two variants of the term exist. In the following, we distinguish the newer usage using capitalization. Elsewhere, context should suffice to discern which meaning applies.

    Obtaining Hypatheon

    Users of PVS 6.0 (and later) and NASA Langley's PVS libraries, known more formally as the NASA PVS Library, can find the Hypatheon software and a pre-built database file as part of the Library distribution. Stable Library releases are distributed as tar files. Once the full 'nasalib' distribution has been downloaded and unpacked, see the file INSTALL.txt in the Hypatheon subdirectory for further instructions. NOTE: a stable Library version with Hypatheon 1.2 has not been released yet; only version 1.1 is available in this form.

    Users of the GitHub repository for the development version of the NASA PVS Library * can also find the Hypatheon software as part of the GitHub Library distribution. This repository is normally cloned into a user directory called 'nasalib'. After issuing a git clone command or updating with a pull command, see the file INSTALL.txt in the Hypatheon subdirectory for further instructions. A script for retrieving the latest pre-built database file is included in the repository. Run this script (fetch-hypatheon-db) to download the database file into the nasalib directory. Hypatheon 1.2 is available from the GitHub repository.

    For other users, the software distribution and database files for versions 5.0 and 6.0 of PVS can be retrieved separately using the links below.

    Current Status

    Screenshots

    Software Files

    NOTE: those who are using a recent nasalib distribution will already have the Hypatheon software files.

    Current Version

    Previous Versions

    Database Files

    Pre-built database files for the core PVS theories and the NASA Langley libraries are available from the links below. By placing these files in a directory listed in PVS_LIBRARY_PATH, they will be found and loaded automatically by Hypatheon. NOTE: those who are using a recent nasalib distribution will already have a matching database file.

    The database files work for all supported platforms (OS X, Linux). There is no need to uncompress the files; Hypatheon will take care of it. Note that Hypatheon can be run without any of these database files if your intention is to do your own library indexing.

    For non-PVS Users

    Hypatheon also can be run in search-only mode without the need for a PVS installation or a copy of the NASA libraries. This might be of interest to users of other theorem provers or those who have an interest in formalized mathematical knowledge. A single distribution file includes the Hypatheon software and the nasalib database in a ready-to-run configuration (no installation required). This might also be helpful to PVS users who would like to search for declarations and theories in their domains of interest before deciding whether to proceed with the full setup.

    Unpack this self-contained tar file configured for search-only mode (48 MB) into a directory of your choice using this command: 

        tar xfz Hypatheon-1.2-nasalib-2mar16.tgz
    This creates the subdirectory <path>/Hypatheon-1.2 (229 MB). The Hypatheon application can be started (from any location) using this command: 
        <path>/Hypatheon-1.2/bin/launch_client
    You may now issue queries as desired. If any problems are encountered, see the instructions near the beginning of the INSTALL.txt file for more information.

    Acknowledgements

    Although the current architecture was scaled down from the original, the concepts and techniques for Hypatheon grew out of a research project on mathematical database development during 2003 and 2004. Summer visitors during those years contributed to the early designs and prototypes. Ideas from two people in particular were especially helpful: Robert Marmorstein and David Johnson. Also helpful was interaction with other team members David Troiano, Matt Klinger, Kristin Rozier, Chris Connett, Golar Newby, Neil Nguyen and Joe Pohl.

    The current version of Hypatheon retains code contributions (in modified form) from Robert Marmorstein, Dave Johnson and Chris Connett. Their contributions to this software are being released, with their permission, in accordance with the NASA Open Source Agreement.

    The tag [*] identifies links that are outside the NASA domain

    usa gov logo

    + Freedom of Information Act
    + NASA Web Privacy Policy and Important Notices
    + USA.gov

    small NASA Logo

    NASA Official: César Muñoz
    + Contact NASA Langley
    + Contact NASA
     Last Updated: January 14, 2013