Re: [isabelle] Proof by analogy and proof stability in Isabelle



Tobias Nipkow schrieb:
This is the killer, I believe:

"Moreover, if the proofs of intermediate lemmas will also be unpacked,
this proof would remain correct even if some intermediate lemmas
disappear in the new version!"

Otherwise replaying proofs is uncritical.

A possibility would also be to include the concept of lemma that can be referenced into the unpacked proof certificate, and include the proofs of required lemmas only once. This would make this certificate format slightly more complex, but avoid explosion of the certificate
by preserving the modularity of the original proof.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.