Hypatheon-Searchable Database Capability for Formalized Mathematics(LAR-18232-1)

The Hypatheon suite of software tools provide a searchable database capability for the specialized domain of formalized mathematics. The technology is designed to be a companion to a specific tool called PVS, which supports an emerging type of advanced software verification intended for safety-critical systems. Hypatheon aims to enhance PVS users' productivity by first indexing the mathematical theories rendered in the PVS specification language, then making their contents searchable by an interactive software tool.