IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Proof Organization and Certification - independence of inference steps
Different organizations of Inference Steps into proof structures and certifications are possible. We shall assume that the inference steps of a proof are organized into a dag. For convenience of discussion we assume the dag has a single root, i.e., a node having no parents, and that the proof purports to justify the conclusion of the root from the premises of the leaf nodes, i.e. the conclusion of the proof is the conclusion of the root inference and the premises of the proof are the premises of the leaf inferences; more generally any dag could also be construed as the collection its rooted subdags. An extreme form of proof organization would be to represent a proof as a rooted dag of certificates each certificate comprising the conclusion of the inference, references to the root certificates of the proofs of the premises of the inference, and an indication of a justification (such as an inference schema or Tactic code) of the conclusion from the premises. The principle drawback of this simplest organization of proofs would be that it does not anticipate the potential costs of justifying an inference.
In a realistic proof system one can expect the cost of inference to dominate, whereas the organization of inferences into a rooted dag is cheap. There are reasons to certify individual inferences independently of other inferences in the larger proof, so let us assume that each inference will be represented as the content of an Inference Step object (a non-certificate), comprising the conclusion and premise Propositions, and a Justification, which is simply an expression used by an Inference Engine to help recognize the inference.
By making the inference step content external to certification content it becomes possible to have multiple certifications by different engines for the same inference. By making the proof structure external to the inference step content, i.e. by
not having the inference step point to proofs of its premises, we make it possible for the same inference to be used in multiple proofs without recertification. While one might imagine having two otherwise unrelated proofs sharing an inference step, the main sharing would be across time among intermediate partial proofs being developed toward a single large proof, or across versions of a proof. Observe that if certifying an inference step in a proof required certifying the proofs of the premises as well, building a proof top down, i.e. by progressive arguments for premises, one would either require repeated certification of inferences as the subproofs were built or one would have to forestall certification of each inference until the whole proof was finished, both of which would be absurd. Another interesting potential of this proof organization is the development of hybrid proofs, in which different kinds of inferences can be performed by distinct inference engines on the various steps in a certified proof.
Continued at
Proof Certification
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html