Subject: FormalContent

Keywords: ::fragments
          ::proof

Title: Proofs as Data

--------------------------------------------------
Traditionally a proof assistant constructs proofs from a proof script.
To construct a proof, the script is evaluated. While there is syntactic
information in the script, in many cases there is little semantic
information. For example an integer literal in a proof script may mean
a hypothesis number, a step count for computation and more.

In Nuprl we construct a tree of inference steps. Each inference step
is stored as an INF object. A proof is a tree of INF objects. Each INF
object contains a Reference Environment, goal, a Tactic Expression,
and the subgoals produce by applying the tactic to the goal in the 
context constructed from the Reference Environment.


See also : 
 How proofs are stored in the libary.
 Separate Refinement
 Tactic Expressions
 Tactic Data
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home