Hypatheon Database Search          Version 1.0        4 Dec 2012


1. Copyright Notice

The following copyright notice applies to the software released in
this package:

  Copyright (c) 2012 United States Government as represented by
  the National Aeronautics and Space Administration.  No copyright
  is claimed in the United States under Title 17, U.S.Code.  All Other
  Rights Reserved.


2. License Agreement

The software in this package has been released as open-source software
under the NASA Open Source Agreement.  See the accompanying file
NASA_Open_Source_Agreement.pdf for a full description of the terms.

As stipulated in the Agreement under clause 3.F, users of the software
are requested to notify the NASA Point of Contact, Ben Di Vito
(b.divito@nasa.gov), providing name, e-mail address and affiliation.
This data is collected for statistical purposes only.  Also requested
is information about any modifications or improvements created by
recipients that are likely to benefit other users.


3. Introduction

Welcome to Hypatheon Database Search.  Hypatheon provides a capability
for indexing PVS theories and making them searchable via a GUI client.
It renders proof-side assistance by finding suitable lemmas within PVS
libraries.  It also can retrieve other declarations and allows you to
view the full theories that contain them.  Detailed descriptions of
features and operation can be found via the Help menu on the client.

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


4. Software Dependencies

Besides PVS itself, Hypatheon requires a standard Python suite in the
version 2 series (version 2.5.x or later), a contemporary SQLite
distribution (version 3.x or later), and the Tcl/Tk GUI toolkit
(version 8.4.x or later).  Recent versions of Linux include suitable
implementations of these as standard software.  OS X 10.4 and later
should have these components as well.


5. Installation Procedure

See the file INSTALL.


6. 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.


7. Conclusion

We hope you find Hypatheon useful and enjoyable.  User feedback is
always welcome.  Further improvements are planned for future releases.
Experience reports and problem reports are encouraged.


Ben Di Vito

b.divito@nasa.gov

 4 Dec 2012