PROSPER Theory Management Subsystem:Discussion and Proposal

This document discusses Task T3.4, which is described in the project proposal as follows:

    ... In Task T3.4 we will add in new theory management facilities to
    suppport the sharing of proof-related data among the CAD/CASE tools,
    the plug-ins, and the core proof engine. The core prover API will
    ... be upgraded, ... so that it supports the theory-related
    requirements of the client tools and the plug-ins. This upgrade
    requires concomitant changes and improvements to the current theory
    management scheme used in HOL, which is slanted towards interactive
    use. In particular, we aim to track dependency relationships between
    proofs and between theories, so that theory revision can be
    automated. Also we envision that multiple and simultaneous theory
    contexts are needed to support the requirements of the CAD/CASE
    tools.

    The result of this task will be a theory management subsystem that
    will support the flow of large quantities of theory-related data
    among the CAD/CASE tools, the plug-ins, and the core proof
    system. Also, it will support the tracking and maintenance of
    theory-related information for the client tools.

(Internal PROSPER document)