IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Continued from
Proof Sentinels
Use and Structure of Proof Sentinels
A sentinel expression is used to direct certification of inferences and assembly of proofs from inference steps, and occurs in records identifying inferences and proofs as having been certified accordingly. In its role as identifying a way to certify an inference, a sentinel expression must identify a method for finding or creating a suitable Inference Engine and it must provide any data (such as pointers to primitive inference rules) to be supplied to the inference engine in addition to the content of the Inference Step. These are specified as programs in a Native Language of the FDL.
In Proof Sentinels we supposed for the sake of explanation that all inference steps of a proof dag were certified according to some given sentinel; we now drop that supposition. In anticipation of the practice of extending a logic, we stipulate that a sentinel expression X determines which other sentinel expressions shall be accepted in assembling proofs according X, i.e. X inherits all the inferences passed by those other sentinels. A search for certificates according to a sentinel X should normally also find those certificates whose sentinels are inherited by X. Again, this can be specified by a program of the FDL's Native Language.
Typical motives for stipulating sentinel inheritance would be: implementation of an inference engine which is believed to be equivalent to an extant implementation; supplying an inference engine with more primitive resources (such as inference rules); the desire to explicitly unite distinct inference methods, simply inheriting them both, and specifying an order to try them when trying to create new certifications according to the union.
When an inference step is certified, the sentinel expression according to which it was certified is stored as a distinguished component of the inference certificate. When a proof is certified, either passively or actively, the sentinel expression determines whether the certificate for a step may be incorporated into the certificate for the whole proof.
Because of the external significance attributed to a sentinel expression by a person, persons will normally work with familiar sentinels, which means they need to be sufficiently small as to make it possible for a person to become familiar with those they understand, and not to mistake one for another. By allowing liberal use of packaging complex material into objects then referred to by object ids, and by allowing liberal use of Native Language macros, a suitable degree of abbreviation should be easily achieved.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html