Inferences Citing Lemmas

There is a subtlety here. In Proof Organization we have given reasons of efficiency to make inference objects independent of the proofs they are part of, based on the assumption that inference checking dominates cost over proof organization, and we assumed inference step certification to be independent of proof certification. But when an inference cites one or more lemmas, then justifying the inference depends on justifying the entire proofs for those lemmas, so in order to maintain the economy of independent inference step certification we must allow inference step certification to fall short of full justification to the extent that lemmas are cited. We modify proof certification to require certification of lemmas cited by an inference just as it requires certification for proofs of children of an inference.

But how is the FDL process supposed to determine which lemmas are cited by an inference? Different Inference Engines supplied by FDL clients might treat lemmas rather differently. A fine grained solution is possible if the inference engine reports which lemmas it depends on for a step; in that case the certification procedure invoking the engine can store in the certificate the list of lemmas as reported by the engine. If, on the other hand, the possible lemmas were to be supplied by the FDL process to the inference engine as part of certification, then again these can be listed as part of the certificate. A coarser solution would be to assume that any proof referred to by the justification part of the inference content might be cited as a lemma and so must be certified in the course of certifying the citing proof.

A second subtlety is implicit in the proof certification procedure extended to lemma citation as described above. Although with "normal" proof methods, one expects the cited lemmas to be proved by the same methods, some systems of proof may not be "uniform", i.e. they may require that certain lemmas cited in certain inferences be proved by a more restrictive method. This means that in order for the FDL process to certify a proof citing lemmas, one must know how to certify the lemma, which in turn means that along with each lemma cited in an inference step certificate, one may need to indicate the certification criteria to be used for the lemma. Of course, the default is just to use the same criterion as for the citing proof.

This same mechanism can be adapted for combining proof methods that are not compatible at the level of individual inference, and so could not participate together in the sort of hybrid proof mentioned in Proof Organization.

Another interesting distribution of verification involves shifting some lemma certification dependencies into the records of how the inference engine was built. It could be practical to create certain inference engines containing a specification of a large ground set of lemmas that were certified by the time the engine was created; this would obviate the need, when the engine is applied, to check those lemmas explicitly (or to mention them in the inference certificate) because: the certification of the inference refers to a process identity certificate for the engine, which in turn refers to the certifications of its base set of lemmas; consequently the whole chain of certificates from that inference down to each base lemma can be assumed to remain intact. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html