Subject: Fragments

Keywords: ::overview

Title: Fragments Overview

--------------------------------------------------
Proofs as data.

Separate refinement. 
 Each Nuprl theorem includes an index to a reference environment. A reference environment
defines the resources which can be accessed during a refinement. This allows a refiner
to refine arbitrary proof steps in any order. This provides the ability to
programmatically manipulate proof fragments.
For example, we have a tool which will compute a minimal set of
hypotheses needed for a fragment to run.
This is done by iteratively removing hypotheses, adjusting
the hypothesis index arguments, and testing the refinement.
This combination of separate refinement and
semantically structured arguments provides a powerful capability for programming proof 
analysis and exploration.

The most interesting attribute of a proof fragment is that the proof author entered the source
expression when presented with a proof subgoal. A fragment represents the smallest creative
act of the proof author. Probably the most insightful act is to assert a new hypothesis.
We can query the fragment database and collect all assert fragments. 
Using algorithms like
matching and unification, we may be able to find patterns for how assertions are constructed
from the context in which they are used.  
The fragment database provides an opportunity to apply the power of machine learning
to proof synthesis.

⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home