Software — free catalog

Hypatheon-Searchable Database Capability for Formalized Mathematics

A NASA software catalog entry available for reuse or request.

Find it in the NASA software catalog Open project or source

About this technology

Overview

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.