Gloss of "Certificate"

As the name suggests, a certificate attests that certain FDL actions were taken at a certain time; they are the basis for logical accounting. A certificate will be realized as an Object which can then be referenced and accessed like other objects save for certain constraints. A certificate cannot be created or modified except by the FDL process following a procedure specific to the "kind" of certificate in question. See Certificates.

Although certificate contents are expected to often be rather compact, largely consisting of Object references, they will often also be rather expensive to establish. By realizing certificates as objects the FDL can build certificates that depend on others whose correctness is independently established. Thus one process of certification can contribute to many other certifications without having to be redone.

The paradigmatic certificates are those created to validate proofs. An Inference Step certificate is built by applying a specified Inference Engine to an inference, and including in the certificate the references to the inference step as well as to the instructions for building or deploying the inference engine; the certificate attests to the fact that such an engine accepted that inference. A Proof is a rooted dag of inference steps. A proof certificate is created only when there is an inference certificate for the root inference and there are already proof certificates for all the proofs of the premises of the root inference. See Proof Organization.

A certificate will be reconsidered either by explicit demand or automatically when any Object it refers to is modified. See Altering Certificates. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html